Hi Patrick.
What you are doing isn't possible in source code (Haskell doesn't prove
things at the value level like a dependently typed language does.)
Usually you document it just as you have, as a comment
-- inverse a ! a = e
You can also specify a QuickCheck property:
propInverse :: (Eq a, Group a) => a -> Bool
propInverse a = (inverse a ! a) == e
I've put up an example on hpaste at http://hpaste.org/47234/simple_monoid
-- ryan
On Sat, May 28, 2011 at 2:46 AM, Patrick Browne <patrick.bro...@dit.ie>wrote:
> Hi,
> I'm not sure if this is possible but I am trying to use Haskell’s type
> class to specify *model expansion*. Model expansion allows the
> specification of new symbols (known as enrichment) or the specification
> further properties that should hold on old symbols. I am trying to
> enrich simplified Monoids to Groups. The code below is not intended to
> do anything other than to specify simplified Groups as a subclass of
> Monoid. The main problem is that I cannot use ! on the LHS of equations
> in Group.
>
> Is it possible to expand the specification of Monoid to Group using
> Haskell type classes?
>
> Pat
>
>
>
> data M = M deriving Show
>
> -- Monoid with one operation (!) and identity e (no associativity)
> class Monoid a where
> (!) :: a -> a -> a
> e :: a
> a ! e = a
>
>
> -- A Group is a Monoid with an inverse, every Group is a Monoid
> -- (a necessary condition in logic: Group implies Monoid)
> -- The inverse property could be expressed as:
> -- 1) forAll a thereExists b such that a ! b = e
> -- 2) (inv a) ! a = e
> class Monoid a => Group a where
> inverse :: a -> a
> -- Haskell does not like ! on the LHS of equation for inverse in Group.
> -- (inverse a) ! a = e
>
> This message has been scanned for content and viruses by the DIT
> Information Services E-Mail Scanning Service, and is believed to be clean.
> http://www.dit.ie
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
