Abstract

Typed Lazy Contracts

Pre- and post-conditions have been important tools for developing correct programs since the early days of programming. Contracts combine pre- and post-conditions. Contracts are usually checked at runtime. If the pre-condition of a function does not hold, then execution is aborted and the caller of the function is blamed for violating the contract. If the post-condition of a function does not hold (but the pre-condition does), then the function itself is blamed.

The runtime-checked assertions that many programming languages such as C and Java provide are precursors of language support for contracts. Since 1986 Bertrand Meyer advocates programming by contract for object-oriented programming languages. In 2002 Robby Findler and Matthias Felleisen established contracts for higher-order functional programming languages. They showed how properties of functional arguments can be checked at runtime and how to provide correct blaming for functional arguments. Since then Scheme programmers have been using contracts.

Until recently the functional language Haskell had no support for contracts. In contrast to Scheme, Haskell has a sophisticated static type system and is based on lazy, demand-driven evaluation. The main challenge is that a definition of contracts can easily break the semantics of a lazy language. Hence we start a contract system for Haskell by identifying a few axioms. We define a weak disjunction combinator and together with a conjunction combinator contracts form a bounded distributive lattice. We derive an implementation from the axioms. For a truly useful contract library for Haskell we still have to consider further issues such as non-invasiveness, informative error messages and general ease of use. Reducing complexity, some expressivity and giving up some equivalences, we obtain a practical contract library for Haskell.