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.