
On Fri, Oct 9, 2009 at 6:11 AM, pat browne
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