Changes between Initial Version and Version 1 of Commentary/Contracts


Ignore:
Timestamp:
Jun 20, 2011 2:01:16 PM (4 years ago)
Author:
cpa
Comment:

Very first version!

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Contracts

    v1 v1  
     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
     12Contracts, 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{{{
     15head ::: {x | not (null x)} -> Ok
     16}}}
     17
     18Where Ok means that the result of head is not an error/exception as long as the argument isn't.
     19
     20
     21Any Haskell boolean expression can be used in a contract, for example
     22{{{
     23fac ::: a:Ok -> {x | x >= a}
     24}}}
     25is a contract that means that for every a which is an actual integer (not an error), then fac a >= a
     26
     27
     28We can also use a higher-order contracts:
     29{{{
     30map ::: ({x | x >= 0} -> {x | x > 0}) -> {xs | not (null xs)} -> Ok
     31}}}
     32This 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
     35For a formal introduction, one can read [1].
     36
     37== The plan ==
     38Verifying 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 ==
     41The 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