| 1 | = Contracts for Haskell = |
| 2 | |
| 3 | == Involved == |
| 4 | * Simon Peyton-Jones |
| 5 | * Dimitrios Vytiniotis |
| 6 | * Koen Claessen |
| 7 | * Charles-Pierre Astolfi |
| 8 | |
| 9 | |
| 10 | == Overview == |
| 11 | |
| 12 | Contracts, just as types, give a specification of the arguments and return values of a function. For example we can give to head the following contract: |
| 13 | |
| 14 | {{{ |
| 15 | head ::: {x | not (null x)} -> Ok |
| 16 | }}} |
| 17 | |
| 18 | Where Ok means that the result of head is not an error/exception as long as the argument isn't. |
| 19 | |
| 20 | |
| 21 | Any Haskell boolean expression can be used in a contract, for example |
| 22 | {{{ |
| 23 | fac ::: a:Ok -> {x | x >= a} |
| 24 | }}} |
| 25 | is a contract that means that for every a which is an actual integer (not an error), then fac a >= a |
| 26 | |
| 27 | |
| 28 | We can also use a higher-order contracts: |
| 29 | {{{ |
| 30 | map ::: ({x | x >= 0} -> {x | x > 0}) -> {xs | not (null xs)} -> Ok |
| 31 | }}} |
| 32 | This contract means that if we apply map to a non-empty list with a function that takes a non-negative integer and returns an positive integer then map returns a list of values without errors. |
| 33 | |
| 34 | |
| 35 | For a formal introduction, one can read [1]. |
| 36 | |
| 37 | == The plan == |
| 38 | Verifying that a function satisfies a given contract is obviously undecidable, but that does not mean that we can't prove anything interesting. Our plan is to translate Haskell programs to first-order logic (with equality) and then use Koen's automated theorem prover to check contract satisfaction. Given that first-order logic is only semi-decidable, the theorem prover can (and in fact does) hang when fed with contracts that are in contradiction with the function definition. |
| 39 | |
| 40 | == Current status == |
| 41 | The current status is described in [3] and some code and examples can be found in [2]. Note that given it's just a prototype the input syntax is slightly different from Haskell. In the end, we should get a ghc extension for contracts. |
| 42 | |
| 43 | == Questions == |
| 44 | * Do we need cfness predicate anymore? It was important in the POPL paper but is still relevant? |
| 45 | * UNR should be renamed to a less confusing name. |
| 46 | * Hoare logic vs liquid types |
| 47 | * Semantics & domain theory to prove the correctness of the translation |
| 48 | * Unfolding for proving contracts on recursive functions |
| 49 | |
| 50 | |
| 51 | == References == |
| 52 | [1] : http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm [[BR]] |
| 53 | [2] : https://github.com/cpa/haskellcontracts and https://github.com/cpa/haskellcontracts-examples [[BR]] |
| 54 | [3] : https://github.com/cpa/haskellcontracts/blob/master/draft2.pdf |