School of Computing

Practical Lazy Typed Contracts for Functional Programming

In programs contracts express properties of run-time values that the programmer expects to hold.

A simple example is asserting that an expression is a natural number, that is, a non-negative integer. A more complex example is asserting for a function that computes a clausal normal form of a formula in propositional logic that its input must be in conjunctive normal form and right-bracketed, and then its output will be a list of list of literals.

Contracts both document and enforce properties that are beyond the standard static type system (or would require awkward encoding in the type system). For functional values both pre- and post-conditions are given.

In a higher-order language contracts should also be higher-order, that is, express properties of higher-order functions that e.g. restrict arguments of a functional type. In a typed language contracts have to be typed and should be type directed, that is, for every type constructor there exists a corresponding contract combinator that has contracts for the type constructor arguments as arguments. The function type contract combinator which takes contracts for pre- and post-conditions as arguments is an example.

Adding contracts to a program leaves its meaning unchanged, unless a contract is violated and thus an exception raised. To ensure this meaning preservation in the presence of lazy evaluation, where expressions may be evaluted only partially, the expressiveness of contracts needs to be limited carefully. For algebraic data types contracts basically provide structural subtyping.

Contracts are similar to assertions. Additionally, contracts are explicitly made between several partners (at least a server, i.e., code providing some service, and a client, i.e., a user of the service) and if a contract is violated one of the partners is to blame.

The Contract library for Haskell

The library uses pure Haskell plus Template Haskell to derive data-type-dependent code and include source locations.

Some example uses: 

  • nat :: (Integral a, Flat a) => Contract a
nat = prop (>= 0)

nats :: (Integral a, Flat a) => Contract [a]
nats = list nat

t3 :: [Integer]
t3 = $assert nats [10,9..(-2)]
    Here contracts for natural numbers and lists of natural numbers are defined. The function $assert takes a contract and monitors it for its second argument. Evaluating t3 yields 
    [10,9,8,7,6,5,4,3,2,1,0,*** Exception: Contract at ContractTest.hs:22:6 failed at
..({-1}:_)..
The server is to blame.

    So the -1 in the list violates the contract. 

  • sqrtC :: Float -> Float
sqrtC = $attach sqrt (prop (>=0) >-> prop (>= 0))

t14 = sqrtC 4
t15 = sqrtC (-4)
    Note that $attach does the same as $assert, but has its two arguments in the opposite order. Here evaluating t14 just returns 2, but evaluating t15 yields 
    *** Exception: Contract at ContractTest.hs:56:9 failed at
({-4.0}->_)
The client is to blame.
  • We can express contracts for user-defined algebraic data types as follows. Here we define a type for propositional formulae and functions that use it. 
    data Formula =
  Imp Formula Formula | And Formula Formula |
  Or Formula Formula | Not Formula | Atom Char

$(deriveContracts ’’Formula)
    The last line derives contract combinators for all data constructors of the type Formula. 
    conjNF = pAnd conjNF conjNF |> disj
disj   = pOr  disj disj |> lit
lit    = pNot atom |> atom
atom   = pAtom true

right = pImp (right & pNotImp) right |>
        pAnd (right & pNotAnd) right |>
        pOr (right & pNotOr) right |>
        pNot right |> pAtom true
    Here several contracts have been defined that we use below. The contract definitions look similar to the definitions of algebraic data types, but also allow the use of conjunction. 
    clausalNF = $assert (conjNF&right >-> list (listlit)) clausalNF’

clausalNF’ :: Formula -> [[Formula]]
clausalNF’ (And f1 f2) = clause f1 : clausalNF’ f2
clausalNF’ f           = [clause f]

clause = $assert (disj&right >-> list lit) clause’

clause’ :: Formula -> [Formula]
clause’ (Or f1 f2) = f1 : clause’ f2
clause’ lit        = [lit]

Using the Contract library

Summary of the Contract library

  • The contract combinators have simple parametrically polymorphic types, such that adding a contract does not change the type of a function.
  • The library provides lazy contract combinators. Adding contracts leaves the semantics of a program unchanged, unless a contract fails.
  • The library is written in pure, portable Haskell, without any use of side-effecting primitives such as unsafePerformIO that could change the semantics of the programming language.
  • All data-type-dependent code is simple and thus easy to write by hand if necessary.
  • The contract combinators have a nice algebra of properties. Contract assertions are partial identities and we claim that they are idempotent too. Thus contracts are projections, like eager contracts.
  • If a contract is violated the raised exception does not simply blame the function or its caller, but provides additional information about the specific value that caused the violation.
  • The library uses Template Haskell to derive all data-type-dependent code and include source code locations. Thus the programmer can formulate contracts for new algebraic data types without any additional work.

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 23/07/2012 15:35