[Haskell-beginners] Re: Enforcing Monad Laws

[Heinrich Apfelmus]

Jorden M wrote:
> C++ `Concepts', which almost made it into the C++0x standard, are
> roughly similar to Haskell type classes. The proposal for concepts in
> C++ had a feature called axioms, which allow the programmer to specify
> semantics on the functions the concept contains. This allows for
> enforcing things such as the Monad Laws, as well as letting the
> compiler make certain optimizations it may not have been able to make
> without axiomatic guarantees.

I have a hard time imagining that axioms are being used to prove 
properties about programs in a language such as C++... :) Any pointers?

> Why does Haskell not have a similar
> functionality in its type classes? Was there not time, desire, etc.?
> Or are there technical limitations?

If you want to exploit algebraic identities like, say,

     map f . map g = map (f . g)

for program optimization, you can use the RULE pragma in GHC.

If you want to use the axioms to prove your program correct, you are 
beginning to leave the scope of Haskell. Have a look at dependently 
typed languages and proof assistants like  Agda  and  Coq . For 
instance, the latter can extract Haskell programs from proofs.

That being said, enforcing invariants in the types, using quickcheck and 
good old pen & paper calculations can carry you a long way towards 
program correctness in Haskell.


Regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com