No subject
Thu Feb 24 17:58:36 CET 2011
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
More information about the Haskell-Cafe
mailing list