On Fri, Oct 9, 2009 at 6:11 AM, pat browne <Patrick.Browne@comp.dit.ie> wrote:
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)

This is a type-indexed type.  On a modern GHC I would write it this way:

class Named a where
   type Name a
   name :: a -> Name a

instance (Named a, Eq (Name a)) => Eq a where
   o1 == o2 = name o1 == name o2

Although to be honest I wouldn't write it this way at all, because your Eq instance is too general (remember, constraints are not examined when doing typeclass resolution; you are not saying "every type 'a' that is an instance of Named with Eq (Name a) is also an instance of Eq", you are saying "EVERY type 'a' is an instance of Eq, and please add the additional constraints 'Eq (Name a)' and 'Named a'") 
 
My questions are:
Question 1: Is my understanding correct?
Question 2: What flavour of DT is this does this example exhibit?

When you say "Dependent Types", what is usually meant is that types can depend on *values*; for example:

data Vector :: Integer -> * -> * where
    Nil :: Vector 0 a
    Cons :: a -> Vector n a -> Vector (n+1) a

Now you might write this function:

zip :: forall a b. (n :: Integer) -> Vector n a -> Vector n b -> Vector n (a,b)
zip 0 Nil Nil = Nil
zip (n+1) (Cons x xs) (Cons y ys) = Cons (x,y) (zip n xs ys)

Notice that the *type* Vector n a depends on the *value* of the argument 'n' passed in.  Normally it is only the other way around; values are limited by what type they are.  Here we have types being affected by some object's value!

  -- ryan