[Haskell-cafe] Haskell.org GSoC
wss at cs.nott.ac.uk
Thu Feb 19 05:58:38 EST 2009
> This could look like:
> module Integer where
> theorem read_parses_what_show_shows :
> (a :: Integer, Show a, Read a) =>
> show . read a = id a
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.
> 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
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,
More information about the Haskell-Cafe