[Haskell-cafe] equations and patterns

[Thomas Schilling]

On 5/31/07, Stefan Holdermans <stefan at cs.uu.nl> wrote:
> Dan,
>
> > If you want to enforce associativity just create your own Eq
> > instance and
> > make it a pattern there.
>
> Could you elaborate on that? It's still early here and I've had only
> one cup of of coffee yet.
>
> Cheers,
>
>    Stefan

QuickCheck allows you to approximately verify properties by testing
them on randomly generated input.  The stated properties thus cannot
formally be proved, but they act as a pretty good formal
specification.  (Full automatic theorem proving for a language as
expressive as Haskell is impossible or infeasible. So we have to
approximate.)

prop_assocJoin x y z = join x (join y z) == join (join x y) z

-- or, more generally

associative :: (Eq a) => (a -> a -> a) -> a -> a -> a -> Bool
associative f x y z = f x (f y z) == f (f x y) z

prop_assocJoin = associative join

-- to check this for a given implementation of "join", you need to:

import Test.QuickCheck

Main> quickCheck  prop_assocJoin

This also requires that QC can generate arbitrary values of type "e".
See the QuickCheck documentation for more infos on that:

http://www.cs.chalmers.se/~rjmh/QuickCheck/manual.html

/ Thomas
-- 
"Remember! Everytime you say 'Web 2.0' God kills a startup!" -
userfriendly.org, Jul 31, 2006