Development.Contract

Practical typed lazy contracts. Author: Olaf Chitil. Version: July 2012.

Contracts describe properties of expressions (esp. functions) that are checked at run-time. Thus these properties are both documented and enforced. Contracts are more expressive than static types. If a contract is violated, then an informative exception is raised.

Example uses:

 head' = $attach head (pNotNil >-> true)

 nat :: (Integral a, Flat a) => Contract a
 nat = prop (>=0)
 fibs = $assert (list nat) (0 : 1 : zipWith (+) fibs (tail fibs))

 conjNF = $(p ’And) conjNF conjNF |> disj
 disj   = $(p ’Or)  disj disj |> lit
 lit    = $(p ’Not) atom |> atom
 atom   = $(p ’Atom) true
 clausalNF' = $attach clausalNF (conjNF & right >-> list (list lit))

See http://www.cs.kent.ac.uk/~oc/contracts.html or Olaf Chitil: Practical Typed Lazy Contracts, ICFP 2012, ACM.

Any user module will need Template Haskell. They will also need DeriveDataTypeable, if they use the deriving combinators for algebraic data types: p, pNot or deriveContracts.

Documentation

data Contract a

The contract type.

data ContractFailed

The exception raised when a contact fails.

Constructors

ContractFailed

Fields

culprit :: Partner

loc :: Loc

explanation :: String

Instances

Show ContractFailed

Typeable ContractFailed

Exception ContractFailed

data Partner

Different contract partners. For any violated contract a partner is blamed.

Constructors

Server

Client

Contract

Instances

Show Partner

assert :: Q Exp

Connect a contract with an expression. The resulting expression is the same except that the contract is monitored for it at runtime. assert splices in code that adds the current location in the module file.

 $assert :: Contract a -> a -> a

attach :: Q Exp

Same as assert with arguments swapped. Useful for attaching contracts in simple variable definitions: fun' = $attach fun contract

 $attach :: a -> Contract a -> a

(&) :: Contract a -> Contract a -> Contract a

Conjunction of two contracts.

(|>) :: Contract a -> Contract a -> Contract a

Disjunction of contracts, given priority to first.

(>->) :: Contract a -> Contract b -> Contract (a -> b)

Function contract combinator, taking contracts for pre- and post-condition.

(>>->) :: Contract a -> (a -> Contract b) -> Contract (a -> b)

Dependent function contract combinator. The post-condition also takes the function argument. Warning: This combinator does not protect laziness!

true :: Contract a

Contract that always succeeds.

false :: Contract a

Contract that always fails, blaming the client.

class Show a => Flat a where

Class of all flat types, for which contract prop works.

A type is flat if its only partial value is bottom / undefined. In other words: an expression of the type is either unevaluted or fully evaluated, never properly partially evaluated.

Methods

prop :: (a -> Bool) -> Contract a

Instances

Flat Bool

Flat Char

Flat Double

Flat Float

Flat Int

Flat Integer

p :: Name -> ExpQ

Pattern contract for given constructor. The argument must be the name of a data constructor. E.g. $(p 'Left)

pNot :: Name -> ExpQ

Negated pattern contract for a given constructor. The argument must be the name of a data constructor. E.g. $(pNot 'Left)

deriveContracts :: Name -> Q [Dec]

For a given algebraic data type declare pattern contracts for all constructors. The argument must be the name of an algebraic data type. E.g. $(deriveContracts ''Either)

dropContext :: Contract a -> Contract a

Drop context information in a contract to avoid unbound context growth. Can be wrapped around any context.

pNil :: Contract [a]

Contract for empty list.

pCons :: Contract a -> Contract [a] -> Contract [a]

Contract combinator for non-empty list. Cf. (:) :: a -> [a] -> [a]

(=:) :: Contract a -> Contract [a] -> Contract [a]

Alternative name for pCons.

pNotNil :: Contract [a]

Contract for non-empty list.

pNotCons :: Contract [a]

Contract for not non-empty list, i.e., empty list.

list :: Contract a -> Contract [a]

Contract combinator for list with elements meeting given contract.

io :: Contract a -> Contract (IO a)

Contract combinator for IO-monad with return value meeting given contract.

pTuple0 :: Contract ()

Contract for empty tuple.

pTuple2 :: Contract a -> Contract b -> Contract (a, b)

Contract combinator for tuple with values meeting given contracts.

pTuple3 :: Contract a -> Contract b -> Contract c -> Contract (a, b, c)

Contract combinator for 3-tuple with values meeting given contracts.

pTuple4 :: Contract a -> Contract b -> Contract c -> Contract d -> Contract (a, b, c, d)

Contract combinator for 4-tuple with values meeting given contracts.

pNothing :: Contract (Maybe a)

Contract for data constructor Nothing.

pJust :: Contract a -> Contract (Maybe a)

Contract combinator for data constructor Just with value meeting given contract.

pNotNothing :: Contract (Maybe a)

Contract for non-Nothing value.

pNotJust :: Contract (Maybe a)

Contract for non-Just value.

maybe :: Contract a -> Contract (Maybe a)

Contract combinator for type Maybe given contract for possible argument value.