[Haskell-cafe] Approaches to dependent types (DT)
deb at pudlak.name
Sat Oct 17 07:42:22 EDT 2009
you might be interested in Agda  and the tutorial "Dependently Typed
Programming in Agda" . I'm just reading the tutorial and it helps me
a lot with understanding the concept.
Also if you'd like to have a deeper understanding of the underlying
theory, I'd suggest reading Barendregt's "Lambda Calculi with Types"
On Fri, Oct 09, 2009 at 02:11:30PM +0100, pat browne wrote:
> I am trying to understand the concept of dependent types as described in
> Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am
> particularly interested in understanding two flavours of dependency
> mentioned by Hinze et al:
> 1) Types depending on values called dependent types
> 2) Types depending on types called parametric and type-indexed types
> I think that ascending levels of abstraction are important here: values
> - types - classes (Hallgren 2001). Here is a Haskell example of the use
> of DT:
> class Named object name | object -> name where
> name :: object -> name
> instance (Eq name, Named object name) => Eq object where
> object1 == object2 = (name object1) == (name object2)
> I think that the intended semantics are:
> 1) Objects have names and can be compared for equality using these names.
> 2) Two objects are considered equal (identical) if they have the same name.
> 3) The type of a name depends on the type of the object, which gets
> expressed as a type dependency (object -> name).
> I am not sure about the last semantic it might be interpreted as "the
> named object depends on..". This may indicate a flaw in my understanding
> of DT.
> I am aware that dependent types can be used to express constraints on
> the size of lists and other collections. My understanding of Haskell's
> functional dependency is that object -> name indicates that fixing the
> type object should fix the type name (equivalently we could say that
> type name depends on type object). The class definition seems to show a
> *type-to-type* dependency (object to name), while the instance
> definition shows how a name value is used to define equality for objects
> which could be interpreted as a *value-to-type* dependency (name to
> object) in the opposite direction to that of the class.
> My questions are:
> Question 1: Is my understanding correct?
> Question 2: What flavour of DT is this does this example exhibit?
> Best regards,
> Hallgren, T. (2001). Fun with Functional Dependencies. In the
> Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January
> Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic
> Programming in Haskell. Datatype-generic programming: international
> spring school, SSDGP 2006.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe