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