[Haskell-beginners] Re: Enforcing Monad Laws

[Jorden M]

On Sun, Jul 4, 2010 at 3:15 AM, Heinrich Apfelmus
<apfelmus at quantentunnel.de> wrote:
> Jorden M wrote:
>>
>> Heinrich Apfelmus 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.
>
> Now that I've had a really short look at Axioms, I think the Haskell
> equivalent would be QuickCheck properties. After all, Axioms are not
> enforced by the compiler, their only effect is documentation. Granted, they

Really? I thought they were.

> are part of the source code, but frankly, I don't see how this has more
> effect than stating invariants as QuickCheck properties or writing them down
> in a comment.

Would it make sense to try to formalize things like the monad laws
using QuickCheck?

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