Ryan, Thank you for your helpful reply. I have no real understanding of dependent types (DT) >From the web is seems that DTs are types that depend on *values*. How does the concept of DT relate to the equation from my example?
>> -- inverse a ! a = 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. > > 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 > <mailto: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 <mailto:Haskell-Cafe@haskell.org> > http://www.haskell.org/mailman/listinfo/haskell-cafe > > 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
