[Haskell-cafe] Sub class and model expansion

[Brandon Moore]

> 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