Programming with contracts in Nickel

In a previous post, I gave a taste of Nickel, a configuration language we are developing at Tweag. One cool feature of Nickel is the ability to validate data and enforce program invariants using so-called contracts. In this post, I introduce the general concept of programming with contracts and illustrate it in Nickel.

Contracts are everywhere

You go to your favorite bakery and buy a croissant. Is there a contract binding you to the baker?

A long time ago, I was puzzled by this very first question of a law class exam. It looked really simple, yet I had absolutely no clue.

“Ehm..No?”

A contract should write down terms and conditions, and be signed by both parties. How could buying a croissant involve such a daunting liability?

Well, I have to confess that this exam didn’t go very well.

It turns out the sheer act of selling something implicitly and automatically establishes a legally binding contract between both parties (at least in France). For once, the programming world is not that different from the physical world: if I see a ConcurrentHashmap class in a Java library, given the context of Java’s naming conventions, I rightfully expect it to be a thread-safe implementation of a hashmap. This is a form of contract. If a programmer uses ConcurrentHashmap to name a class that implements a non-thread safe linked list, they should probably be sent to court.

Contracts may take multiple forms. A contract can be explicit, such as in a formal specification, or implicit, as in the ConcurrentHashMap example. They can be enforced or not, such as a type signature in a statically typed language versus an invariant written as a comment in a dynamically typed language. Here are a few examples:

As often, explicit is better than implicit: it leaves no room for misunderstanding. Enforced is better than not, because I would rather be protected by a proper legal system in case of contract violation.

Programming with Contracts

Until now, I’ve been using the word contract in a wide sense. It turns out contracts also refer to a particular programming paradigm which embodies the general notion pretty well. Such contracts are explicit and enforced, following our terminology. They are most notably used in Racket. From now on, I shall use contract in this more specific sense.

To first approximation, contracts are assertions. They check that a value satisfies some property at run-time. If the test passes, the execution can go on normally. Otherwise, an error is raised.

In Nickel, one can enforce a contract using the | operator:

let x = (1 + 1 | Num) in 2*x

Here, x is bound to a Num contract. When evaluating x, the following steps are performed:

1. evaluate 1 + 1
2. check that the result is a number
3. if it is, return the expression unchanged. Otherwise, raise an error that halts the program.

Let’s see it in action:

$nickel <<< '1 + 1 | Num'
Done: Num(2.0)

$nickel <<< 'false | Num'
error: Blame error: contract broken by a value.
  ┌─ :1:1
  │
1 │ Num
  │ --- expected type
  │
  ┌─ <stdin>:1:9
  │
1 │ false | Num
  │         ^^^ bound here

Contracts versus types

I’ve described contracts as assertions, but the above snippet suspiciously resembles a type annotation. How do contracts compare to types? First of all, contracts are checked at run-time, so they would correspond to dynamic typing rather than static typing. Secondly, contracts can check more than just the membership to a type:

let GreaterThan2 = fun label x =>
  if builtins.isNum x then
    if x > 2 then
      x
    else
      contracts.blame (contracts.tag "smaller or equals" label)
  else
    contracts.blame (contracts.tag "not a number" label)
in

(3 | #GreaterThan2) // Ok, evaluate to 3
(1 | #GreaterThan2) // Err, `smaller or equals`
("a" | #GreaterThan2) // Err, `not a number`

Here, we just built a custom contract. A custom contract is a function of two arguments:

• the label label, carrying information for error reporting.
• the value x to be tested.

If the value satisfies the condition, it is returned. Otherwise, a call to blame signals rejection with an optional error message attached via tag. When evaluating value | #Contract, the interpreter calls Contract with an appropriate label and value as arguments.

Such custom contracts can check arbitrary properties. Enforcing the property of being greater than two using static types is rather hard, requiring a fancy type system such as refinement types , while the role of dynamic types generally stops at distinguishing basic datatypes and functions.

Back to our first example 1 + 1 | Num, we could have written instead:

let MyNum = fun label x =>
  if builtins.isNum x then x else contracts.blame label in
(1 + 1 | #MyNum)

This is in fact pretty much what 1 + 1 | Num evaluates to. While a contract is not the same entity as a type, one can derive a contract from any type. Writing 1 + 1 | Num asks the interpreter to derive a contract from the type Num and to check 1 + 1 against it. This is just a convenient syntax to specify common contracts. The# character distinguishes contracts as types from contracts as functions (that is, custom contracts).

To sum up, contracts are just glorified assertions. Also, there is this incredibly convenient syntax that spares us a whole three characters by writing Num instead of #MyNum. So… is that all the fuss is about?

Function contracts

Until now, we have only considered what are called flat contracts, which operate on data. But Nickel is a functional programming language: so what about function contracts? They exist too!

let f | Str -> Num = fun x => if x == "a" then 0 else 1 in ...

Here again, we ask Nickel to derive a contract for us, from the type Str -> Num of functions sending strings to numbers. To find out how this contract could work, we must understand what is the defining property of a function of type Str -> Num that the contract should enforce.

A function of type Str -> Num has a duty: it must produce a number. But what if I call f on a boolean? That’s unfair, because the function has also a right: the argument must be a string. The full contract is thus: if you give me a string, I give you a number. If you give me something else, you broke the contract, so I can’t guarantee anything. Another way of viewing it is that the left side of the arrow represents preconditions on the input while the right side represents postconditions on the output.

More than flat contracts, function contracts show similarities with traditional legal contracts. We have two parties: the caller, f "b", and the callee, f. Both must meet conditions: the caller must provide a string while the callee must return a number.

In practice, inspecting the term f can tell us if it is a function at most. This is because a function is inert, waiting for an argument to hand back a result. In consequence, the contract is doomed to fire only when f is applied to an argument, in which case it checks that:

1. The argument satisfies the Str contract
2. The return value satisfies the Num contract

The interpreter performs additional bookkeeping to be able to correctly blame the offending code in case of a higher-order contract violation:

$nickel <<< 'let f | Str -> Num = fun x => if x == "a" then 0 else 1 in f "a"'
Done: Num(0.0)

$nickel <<< '... in f 0'
error: Blame error: contract broken by the caller.
  ┌─ :1:1
  │
1 │ Str -> Num
  │ --- expected type of the argument provided by the caller
  │
  ┌─ <stdin>:1:9
  │
1 │ let f | Str -> Num = fun x => if x == "a" then 0 else 1 in f 0
  │         ^^^^^^^^^^ bound here
[..]

$nickel <<< 'let f | Str -> Num = fun x => x in f "a"'
error: Blame error: contract broken by a function.
  ┌─ :1:8
  │
1 │ Str -> Num
  │        --- expected return type
  │
  ┌─ <stdin>:1:9
  │
1 │ let f | Str -> Num = fun x => x in f "a"
  │         ^^^^^^^^^^ bound here

These examples illustrate three possible situations:

1. The contract is honored by both parties.
2. The contract is broken by the caller, which provides a number instead of a string.
3. The contract is broken by the function (callee), which rightfully got a string but returned a string instead of a number.

Combined with custom contracts, function contracts make it possible to express succinctly non-trivial invariants:

let f | #GreaterThan2 -> #GreaterThan2 = fun x => x + 1 in ..

A warning about laziness

Nickel is a lazy programming language. This means that expressions, including contracts, are evaluated only if they are needed. If you are experimenting with contracts and some checks buried inside lists or records do not seem to trigger, you can use the deepSeq operator to recursively force the evaluation of all subterms, including contracts:

let exp = ..YOUR CODE WITH CONTRACTS.. in builtins.deepSeq exp exp

Conclusion

In this post, I introduced programming with contracts. Contracts offer a principled and ergonomic way of validating data and enforcing invariants with a good error reporting story. Contracts can express arbitrary properties that are hard to enforce statically, and they can handle higher-order functions.

Contracts also have a special relationship with static typing. While we compared them as competitors somehow, contracts and static types are actually complementary, reunited in the setting of gradual typing. Nickel has gradual types, which will be the subject of a coming post.

The examples here are illustrative, but we’ll see more specific and compelling usages of contracts in yet another coming post about Nickel’s meta-values, which, together with contracts, serve as a unified way to describe and validate configurations.