No subject

How does the concept of DT relate to the equation from my example?

>>     -- inverse a ! a =3D e

What type is depending on what value?

Once again thanks for time and insight.
Pat


On 29/05/2011 22:45, Ryan Ingram wrote:
> Hi Patrick.
>=20
> 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.)
>=20
> Usually you document it just as you have, as a comment
>=20
>     -- inverse a ! a =3D e
>=20
> You can also specify a QuickCheck property:
>=20
> propInverse :: (Eq a, Group a) =3D> a -> Bool
> propInverse a =3D (inverse a ! a) =3D=3D e
>=20
> I've put up an example on hpaste at http://hpaste.org/47234/simple_mono=
id
>=20
>   -- ryan
>=20
> On Sat, May 28, 2011 at 2:46 AM, Patrick Browne <patrick.browne at dit.ie
> <mailto:patrick.browne at dit.ie>> wrote:
>=20
>     Hi,
>     I'm not sure if this is possible but I am trying to use Haskell=92s=
 type
>     class to specify  *model expansion*. Model expansion allows the
>     specification of new symbols (known as enrichment) or the specifica=
tion
>     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 o=
f
>     Monoid. The main problem is that I cannot use ! on the LHS of equat=
ions
>     in Group.
>=20
>     Is it possible to expand the specification of Monoid to Group using
>     Haskell type classes?
>=20
>     Pat
>=20
>=20
>=20
>     data M =3D M deriving Show
>=20
>     -- Monoid with one operation (!) and identity e (no associativity)
>     class Monoid  a where
>      (!)  ::  a -> a -> a
>      e :: a
>      a ! e =3D a
>=20
>=20
>     -- 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 =3D e
>     --      2)  (inv a) ! a  =3D  e
>     class Monoid a =3D> Group a where
>      inverse  ::  a -> a
>     -- Haskell does not like  ! on the LHS of equation for inverse in G=
roup.
>     --  (inverse a) ! a  =3D e
>=20
>     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
>=20
>     _______________________________________________
>     Haskell-Cafe mailing list
>     Haskell-Cafe at haskell.org <mailto:Haskell-Cafe at haskell.org>
>     http://www.haskell.org/mailman/listinfo/haskell-cafe
>=20
>=20


This message has been scanned for content and viruses by the DIT Informat=
ion Services E-Mail Scanning Service, and is believed to be clean. http:/=
/www.dit.ie