Continuing the thread on model expansion. I have changed the example trying to focus on expanding models of M in G Why is the operation ! ok or RHS but not visible on LHS of G? The equation itself does not seem to suffer from the dependent type problem of my previous post.
class M a where (!) :: a -> a -> a e :: a class M a => G a where (!-) :: a -> a -> a -- OK in G a !- e = e ! a -- Switching LHS/RHS is not OK in G but fine in S -- if I declare both ! and !- in S -- ! is not a (visible) method of class `G' -- a ! e = e !- a Thanks, Pat On 30/05/2011 00:47, Brandon Moore wrote: >> From: Patrick Brown; Sent: Sunday, May 29, 2011 5:42 PM > >> Subject: Re: [Haskell-cafe] Sub class and model expansion >> >> 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? > > You want part of the group interface to be a proof > that your inverse function agrees property with the > monoid operation and unit. > > If that's going to be a value, it has to have some type. > If that type is anything like "Proof that inverse a ! a = e", > then the type mentions, or "depends on" the values > inverse, (!), and e. > > You can see exactly this in the Agda standard library, > in the definitions IsMonoid and IsGroup in > Algebra.Structures, which define records containing > proofs that a set of operations actually forms a monoid > or group. > > > You could probably avoid the apparent circularity > of full dependent types if you split up a language > into values which can have types, and a separate > pair of propositions and proofs which can refer to > values and types, but not to themselves. > > I think that's basically the organization of any system > where you use a separate prover to prove things about > programs in some previously-existing programming > language, but I haven't stumbled across any examples > where that sort of organization was designed into > a single language from the start. > > > Brandon > 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