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