►Pyret
►2 Language Concepts
▼2.1 Language Constructs
    contents    up   
2.1.9 Contracts

As part of its support for the systematic design of functions, Pyret allows developers to specify an annotation for a name, before that name is defined. The general grammar for standalone contracts is:

For example,

the-answer :: Number
the-answer = 42

double :: String -> String
fun double(s): s + s end

vals-to-string :: <T, S> (S, T -> String)
fun vals-to-string(val1, val2):
  to-string(val1) + ", " + to-string(val2)
end

In all of these cases, the definition itself (of the-answer, double, and vals-to-string) is preceded by a contract statement, asserting the signature of the definition to follow. Pyret treats these contracts specially, and weaves them in to the definitions: the previous examples are equivalent to

the-answer :: Number = 42

fun double(s :: String) -> String: s + s end

fun vals-to-string<T,S>(val1 :: T, val2 :: S) -> String:
  to-string(val1) + ", " + to-string(val2)
end

The grammar for these contracts looks nearly identical to that of ‹name-binding›s. Function annotations are given a slightly more relaxed treatment: the outermost set of parentheses are optional.

‹contract›: NAME :: ‹ty-params› ‹ann› | NAME :: ‹ty-params› ‹contract-arrow-ann› ‹contract-arrow-ann›: (‹ann› ,)* ‹ann› -> ‹ann› | ( (NAME :: ‹ann› ,)* NAME :: ‹ann› ) -> ‹ann›

When weaving function annotations onto functions, Pyret enforces a few restrictions:

  • For a standalone function, the contract must immediately precede the function definition, or must immediately precede an examples or check block that immediately precedes the function definition. (Whitespace or comments are not important; extraneous definitions are.)

    is-even :: Number -> Boolean

check:
  is-even(2) is true
end

fun is-even(n): num-modulo(n, 2) == 0 end
    is-even :: Number -> Boolean

something-irrelevant = 12345

fun is-even(n): num-modulo(n, 2) == 0 end

  • For mutually recursive functions, the contracts must be adjacent to the functions, and must precede them. 
    # Contracts
is-even :: Number -> Boolean
is-odd :: Number -> Boolean
# Implementations
fun is-even(n): if n == 0: true else: is-odd(n - 1) end end
fun is-odd(n): if n == 0: false else: is-even(n - 1) end end
    # Is even?
is-even :: Number -> Boolean
fun is-even(n): if n == 0: true else: is-odd(n - 1) end end
# Is odd?
is-odd :: Number -> Boolean
fun is-odd(n): if n == 0: false else: is-even(n - 1) end end
    is-odd :: Number -> Boolean
fun is-even(n): if n == 0: true else: is-odd(n - 1) end end
is-even :: Number -> Boolean  ## Does not precede definition of is-even
fun is-odd(n): if n == 0: false else: is-even(n - 1) end end

  • If a contract specifies argument names, then the names must match those used by the function. 
    is-even :: (n :: Number) -> Boolean
fun is-even(n): num-modulo(n, 2) == 0 end
    is-even :: (x :: Number) -> Boolean # name does not match
fun is-even(n): ... end

  • If a contract is used for a function, then the function must not itself be annotated. 
    is-even :: (n :: Number) -> Boolean
fun is-even(n): num-modulo(n, 2) == 0 end
    is-even :: (n :: Number) -> Boolean # Redundant argument annotation
fun is-even(n :: Number): ... end
    is-even :: (n :: Number) -> Boolean # Redundant return annotation
fun is-even(n) -> Boolean: ... end

Note that using a contract on a function is more expressive than using an annotated binding for a lambda. Annotated bindings do not enforce all the components of an arrow annotation; they merely ensure that the value being bound is in fact a function. By contrast, function contracts ensure the arguments and return values are annotated and checked.

    contents    up