[Haskell-cafe] Approaches to dependent types (DT)

[pat browne]

Hi,
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,
Pat


Hallgren, T. (2001). Fun with Functional Dependencies. In the
Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January
2001.
Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic
Programming in Haskell. Datatype-generic programming: international
spring school, SSDGP 2006.