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