[Haskell-cafe] Sub class and model expansion

[Ryan Ingram]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110529/841a809f/attachment.htm>