Abstract

Contracts for Lazy Functional Languages

Contracts assert pre- and post-conditions for functions that go beyond standard static types. Contracts are checked at runtime. Scheme programmers have been using them for over 10 years, but until now there has been no support for contracts within lazy functional languages. A definition of contracts can easily break the semantics of lazy languages. Hence here we start with 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 types, informative error messages and ease of use. Reducing complexity, some expressivity and giving up some equivalences, we then obtain a practical contract library for Haskell.