[Haskell-cafe] Sub class and model expansion
Patrick Browne
patrick.browne at dit.ie
Tue May 31 10:40:15 CEST 2011
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
More information about the Haskell-Cafe
mailing list