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

[Ryan Ingram]

On Fri, Oct 9, 2009 at 6:11 AM, pat browne <Patrick.Browne at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091010/3f086966/attachment.html