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