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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
