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

[Dan Doel]

I'll see if I can't gloss over some of the stuff Ryan Ingram already covered.

On Friday 09 October 2009 9:11:30 am pat browne wrote:
> 2) Types depending on types called parametric and type-indexed types

The above distinction in types (and values) depending on types has to do with 
operations beyond just said dependency. For instance:

  data List a = Nil | Cons a (List a)

Is the definition involving types that depend on other types. And similarly:

  foo :: forall a. List (List a)
  foo = Cons Nil Nil

is a value that depends on a type. In a language more explicit about type 
application, one might write:

  foo at a = Cons@(List a) Nil at a Nil@(List a)

So far, these fall in the parametric category, but your example does not:

> class Named object name | object -> name where
> name :: object -> name

Classes in H98 allow you to define non-parametric type->value dependence, and 
when extended with functional dependencies, or alternately, if we consider 
type families, we get non-parametric type->type dependence. The difference 
isn't in what things can depend on what other things, but in what operations 
are available on types. Specifically, type classes/families are like being 
able to do case analysis on types, so in the value case:

  class Foo a where
    bar :: [a]

  instance Foo Int where
    bar = [5]

  instance Foo Char where
    bar = "c"

can be seen as similar to:

  bar at c = typecase c of
            Int  -> [5]
            Char -> "c"

And type families are similar on the type-level (it's less clear how 
functional dependencies fit in, but a one way a -> b is kind of like doing a 
type-level typecase on a to define b; more accurately you have multiple type 
parameters, but in each a-branch, b there is exactly one b-branch). Of course, 
this is an over-simplification, so take it with salt.

> I am aware that dependent types can be used to express constraints on
> the size of lists and other collections.

Technically, you don't need dependent types for this, you just need type-level 
naturals. But dependent types (or some sufficiently fancy faking thereof) are 
nice in that you only need to define the naturals once, instead of at both the 
value and type levels.

> 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.

As Ryan remarked, this is not a value->type dependency. In the instance, you 
are defining equality for the type 'object' which determines the type 'name' 
in a type->type dependency. You're then defining equality on values of type 
'object' via equality on values of type 'name', via the 'name' function. But 
that's just value->value dependency which every language of course has.

GHC does have ways of faking dependent types, though, with GADTs. GADTs allow 
you to define data such that matching on constructors refines things in the 
type system. So, along with the mirroring mentioned above, you can manually 
set up a value->type dependency that acts like full-on dependent types. For 
naturals it looks like:

  -- type level naturals
  data Zero
  data Suc n

  -- value-level GADT indexed by the type-level naturals
  data Nat n where
    Zero :: Nat Zero
    Suc  :: Nat n -> Nat (Suc n)

  -- existential wrapper
  data Natural where
    Wrap :: Nat n -> Natural

Ryan's zip function would look like:

  zip :: forall a b n. Nat n -> Vector n a -> Vector n b -> Vector n (a,b)
  zip Zero    Nil         Nil         = Nil
  zip (Suc n) (Cons x xs) (Cons y ys) = Cons (x,y) (zip n xs ys)

although the 'Nat n' parameter is technically unnecessary in this case. But, 
in some other function:

  foo :: forall n. Nat n -> T
  foo Zero    = {- we know type-level n = Zero here -}
  foo (Suc n) = {- we know type-level n = Suc m for some m here -}

Of course, mirroring like the above is kind of a pain and only gets more so 
the more complex the things you want to mirror are (although this is how, for 
instance, ATS handles dependent types). There is a preprocessor, SHE, that 
automates this, though, and lets you write definitions that look like a full-
on dependently typed language (among other things).

Anyhow, I'll cease rambling for now.

Cheers,

-- Dan