Safe Haskell | None |
---|
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
.
- data Contract a
- data ContractFailed = ContractFailed {}
- data Partner
- assert :: Q Exp
- attach :: Q Exp
- (&) :: Contract a -> Contract a -> Contract a
- (|>) :: Contract a -> Contract a -> Contract a
- (>->) :: Contract a -> Contract b -> Contract (a -> b)
- (>>->) :: Contract a -> (a -> Contract b) -> Contract (a -> b)
- true :: Contract a
- false :: Contract a
- class Show a => Flat a where
- p :: Name -> ExpQ
- pNot :: Name -> ExpQ
- deriveContracts :: Name -> Q [Dec]
- dropContext :: Contract a -> Contract a
- pNil :: Contract [a]
- pCons :: Contract a -> Contract [a] -> Contract [a]
- (=:) :: Contract a -> Contract [a] -> Contract [a]
- pNotNil :: Contract [a]
- pNotCons :: Contract [a]
- list :: Contract a -> Contract [a]
- io :: Contract a -> Contract (IO a)
- pTuple0 :: Contract ()
- pTuple2 :: Contract a -> Contract b -> Contract (a, b)
- pTuple3 :: Contract a -> Contract b -> Contract c -> Contract (a, b, c)
- pTuple4 :: Contract a -> Contract b -> Contract c -> Contract d -> Contract (a, b, c, d)
- pNothing :: Contract (Maybe a)
- pJust :: Contract a -> Contract (Maybe a)
- pNotNothing :: Contract (Maybe a)
- pNotJust :: Contract (Maybe a)
- maybe :: Contract a -> Contract (Maybe a)
Documentation
Different contract partners. For any violated contract a partner is blamed.
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
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 aSource
Disjunction of contracts, given priority to first.
(>->) :: Contract a -> Contract b -> Contract (a -> b)Source
Function contract combinator, taking contracts for pre- and post-condition.
(>>->) :: Contract a -> (a -> Contract b) -> Contract (a -> b)Source
Dependent function contract combinator. The post-condition also takes the function argument. Warning: This combinator does not protect laziness!
class Show a => Flat a whereSource
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.
Pattern contract for given constructor. The argument must be the name of a data constructor. E.g. $(p 'Left)
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]Source
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 aSource
Drop context information in a contract to avoid unbound context growth. Can be wrapped around any context.
pCons :: Contract a -> Contract [a] -> Contract [a]Source
Contract combinator for non-empty list. Cf. (:) :: a -> [a] -> [a]
list :: Contract a -> Contract [a]Source
Contract combinator for list with elements meeting given contract.
io :: Contract a -> Contract (IO a)Source
Contract combinator for IO-monad with return value meeting given contract.
pTuple2 :: Contract a -> Contract b -> Contract (a, b)Source
Contract combinator for tuple with values meeting given contracts.
pTuple3 :: Contract a -> Contract b -> Contract c -> Contract (a, b, c)Source
Contract combinator for 3-tuple with values meeting given contracts.
pTuple4 :: Contract a -> Contract b -> Contract c -> Contract d -> Contract (a, b, c, d)Source
Contract combinator for 4-tuple with values meeting given contracts.
pJust :: Contract a -> Contract (Maybe a)Source
Contract combinator for data constructor Just
with value meeting given contract.
pNotNothing :: Contract (Maybe a)Source
Contract for non-Nothing
value.