[Haskell-cafe] Sub class and model expansion

[Patrick Browne]

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