[Haskell-beginners] Re: Enforcing Monad Laws

[Jorden M]

On Fri, Jul 2, 2010 at 4:04 AM, Heinrich Apfelmus
<apfelmus at quantentunnel.de> wrote:
> 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?

That is not what they are for. Axiom is probably not a good choice of
terminology. Axioms let a concept enforce certain statements about
functions inside the concept. E.g., in a concept that describes
addition, one could use an axiom statement to enforce commutativity of
that addition operation. There seems to be no way to do this in
Haskell, hence my question.

>
>> 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.

Certainly. My question was as to why there isn't something like this
right in the syntax for type classes. Seems like it would go a long
way, esp. for things like enforcing the monad laws.

>
>
> Regards,
> Heinrich Apfelmus
>
> --
> http://apfelmus.nfshost.com
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>