contracts.coffee

Simple Contracts

In addition to the Num contract that checks for numbers, we also have Str, Bool, Null, Undefined, Nat, Pos, Neg, Any (everything is ok), and None (nothing is ok).

Functions

Basic functions:

f :: (Num) -> Num
f = (x) -> x

Multiple arguments:

f :: (Num, Str, Bool) -> Num
f = (n, s, b) -> # ...

Optional arguments:

f :: (Num, Str, Bool?) -> Num
f = (n, s, b) -> # ...

All optional arguments must come at the end of the arguments list.

Higher order functions:

f :: ((Num) -> Bool, Num) -> Bool
f = (g, n) -> # ...

Functions that cannot be called with the new keyword:

f :: (Num) --> Num
f = (n) -> # ...
#...

g = f 42      # ok
g = new f 42  # error!

Functions that can only be called with the new keyword:

f :: (Num) ==> Num
f = (n) -> # ...
#...

g = f 42      # error!
g = new f 42  # ok

Dependent functions:

inc :: (Num) -> !(result, args) -> result > args[0]
inc = (n) -> n + 1

The variable args[0] is the first argument passed to the function (args[1] would be the second argument, args[2] the third, and so on). This allows us to compare the result of the function to its arguments. Note that the test is run after the function has completed so if any of the arguments were mutated during the function’s execution the test could give spurious results.

The this contract:

f :: (Str, @{name: Str}) -> Str
f = (s) -> #...

o = { name: "foo", f: f}
o.f()

Checks that this matches the given object contract.

Objects

Simple properties:

o ::
  a: Str
  b: Num
  f: (Num) -> Num
o =
  a: "foo"
  b: 42
  f: (x) -> x

Note: Putting an object contract on a primitive will always fail. This might seem obvious at first but since many primitives have methods, the following contract would seem reasonable:

f :: ({toString: (Any) -> Str}) -> Str
f = (s) -> s.toString()

f "a string"   # Contract violation
f {}           # ok

Even though “a string” has a toString method the contract will always signal a violation. This is because JavaScript proxies can wrap objects but not primitives.

In addition due to a limitation in the current JavaScript engines implementations of proxies, you cannot put a contract on the Date object. This is expected to be fixed in future implementations. See this issue to track progress on this.

Optional properties:

o ::
  a: Str
  b: Num?
  f: (Num) -> Num
o =
  a: "foo"
  f: (x) -> x

Nested objects:

o ::
  oo: { a: Str }
  b: Num
o =
  oo: { a: "foo" }
  b: 42

Recursive objects:

o ::
  a: Num
  b: Self
  c: (Num) -> Self
  inner: { y: Bool, z: Self }
o = #...

Self binds to the closest object contract. So in this example, Self in b and c points to o and Self in inner.z points to inner.

Objects with functions that have pre and post conditions:

o ::
  a: Num
  f: (Num) -> Num -|
      pre: (o) -> o.a > 10
      post: (o) -> o.a > 20
o =
  a: 12
  f: (x) -> @.a = @.a + x

The pre and post condition functions are called with the object that f is a member of. As their names imply, pre is called before the function f is invoked and post is called after.

Object invariants:

o ::
  a: Num
  f: (Num) -> Num -|
      pre: (o) -> o.a > 10
      post: (o) -> o.a > 20
  -| invariant: ->
    @.a > 0 and @.a < 100
o =
  a: 12
  f: (x) -> @.a = @.a + x

The invariant is checked at contract application and whenever there is a possibility of o mutating (on property sets and delete).

Arrays

Note: due to a proxy bug in all the current JavaScript engines, arrays are not currently being wrapped in a contract. This won’t cause code to fail, it just means that contracts will not be checked for arrays. See this github issue for more info.

Basic arrays:

a :: [Num, Str, [Bool, Num]]
a = [42, "foo", [true, 24]

This says the array must have three elements, the first being a Num, the second being a Str, and the third being another array.

Multiple elements:

a :: [...Num]
a = [42, 24, 432, 854, 21]

The ... operator says that the array will only contain Nums.

Mixing arrays

a :: [Bool, Str, ...Num]
a = [false, "foo", 432, 854, 21]

The ... operator can be mixed with single contracts. This says that the array’s first and second positions must pass the first two contracts and the remaining array positions must pass Num. The ... operator must be in the last position of the array contract.

o :: { a: Num or Str }
o = { a: 42 }

o :: { a: Num and Even }
o = { a: 42 }

f :: ((Num) -> Num, (Str) -> Str) -> Num
f = (g, h) -> g 42

str = (x) -> "string"
num = (x) -> 42

f str, num  # fails when g is called inside f
f num, num  # since h is never called it never fails
            # even though it would violate its contract

f :: (Num) -> {a: Str, b: Num}
f = (x) -> {a: "foo"}

# fails as soon as f returns since b is missing
f 42

g :: (Num) -> {a: Str, b: Num}
g = (x) -> {a: x, b: x}

o = g 42         # does not fail yet
console.log o.a  # now fails because o.a does not satisfy Str

NumId = ?(Num) -> Num

f :: NumId
f = (x) -> x

takesEvens :: (!(x) -> x % 2 is 0) -> Num
takesEvens = (x) -> x

Num = ?!(x) -> typeof x is 'number'
Str = ?!(x) -> typeof x is 'string'

Num = (x) -> typeof x is 'number'
Str = (x) -> typeof x is 'string'

f = (!Num) -> !Str

# A binary search tree is a binary tree 
# where each node is  greater than the 
# left child but less than the right child
BinarySearchTree = ?(Null or {
  node: Num
  left: Self or Null
  right: Self or Null
  -| invariant: ->
    (@.node > @.left.node) and (@.node < @.right.node)
})

# A red-black tree is a binary search tree 
# that keeps its balance
RedBlackTree = ?(Null or {
  node: Num
  color: Str
  left: Self or Null
  right: Self or Null
  -| invariant: ->
    (@.color is "red" or @.color is "black") and
    (if @.color is "red"
      (@.left.color is "black" and 
       @.right.color is "black") 
    else 
      true
    ) and
    (@.node >= @.left.node) and 
    (@.node >= @.right.node) and
})

takesBST :: (BinarySearchTree) -> Any
takesBST = (bst) -> ...

takesRedBlack :: (RedBlackTree) -> Any
takesRedBlack = (rbTree) -> ...

bst = makeBinarySearchTree()  
rb = makeRedBlackTree()

takesBST bst # works fine
takesBST rb  # works fine

takesRedBlack rb  # works fine
takesRedBlack bst # might fail if the full 
                  # red-black invariants don't hold!