[Haskell-cafe] Haskell.org GSoC

[Wouter Swierstra]

> This could look like:
>
> module Integer where
>  ..
>  theorem read_parses_what_show_shows :
>    (a :: Integer, Show a, Read a) =>
>    show . read a = id a
>    proof
>      axiom

There are several problems with this approach.

For example, I can show:

const 0 (head []) = 0

But if I pretend that I don't know that Haskell is lazy:

const 0 (head []) = const 0 (error ....) = error ...

Which would allow me to substitute each occurrence of 0 with "error" -  
which probably isn't a good idea. So to do proper equational reasoning  
in a lazy language you need to be extremely careful with evaluation  
order. Predicting the evaluation order of code generated by "ghc -O2  
Main.hs" is non-trivial to say the least.

To make matters worse, as you're working in a language with general  
recursion, you have to be fight quite hard to avoid introducing  
inconsistencies in your proof language.

Alberto wrote:
> As far as I understand,  a dependent type system can restrict the  
> set of values for wich a function apply, but it can not express  
> complex relationships between operations. My knowledge on dependent  
> types is very limited. I would like to be wrong on this.

I'm sorry, but you're wrong. Dependent types can encode the kind of  
equational proofs Sylvain mentioned perfectly adequately. Lennart  
Augustsson has a nice note explaining the principle in the context of  
Cayenne:

http://www.cs.chalmers.se/~augustss/cayenne/eqproof.ps

The good news is: in languages like Coq and Agda you can write total  
functional programs, like map or ++, verify such properties and  
extract Haskell code.

Hope this helps,

   Wouter