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

[pbrowne]

Hi,
I am attempting to explain an example of dependent types to computing
practitioners who do not have any background in functional programming.
My goal is to explain the example rather than implement or improve it. I
have been told in previous postings that the approach below is a bit
dated. Any comments on the correctness or otherwise would be appreciated.

Regards,
Pat

=======================================================

Dependent Types (DT)
The purpose of dependent types (DT) is to allow programmers to specify
dependencies between the parameters of a multiple parameter class.  DTs
can be seen as a move towards more general purpose parametric type
classes. DTs are declared in a class header, where the type of one class
parameter is declared to depend on another class parameter. Consider the
following example:

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

instance (Eq name, Named object name) => Eq object where
object1 == object2 = (namef object1) == (namef object2)

The first part of the class definition Named takes two type variables as
parameters; namely object and name. We say, that object determines name
or alternatively that name is determined by object. This is denoted in
the second part of the class header (i.e. | object -> name). With DTs,
the dependent type depends on values of the determining type.  Hence, a
DT involves a relation between Haskell’s value-level and the type-level
(or type system). The Named class contains the signature, but not the
definition, of one function called namef. Note, the in the definition of
namef, the argument and return type (object -> name) are textually
identical to that occurring in the class header, however the semantic is
that of function definition rather that of type dependency.
In the instance declaration, the part before the => is called the
context, while the part after the => is called the head of the instance
declaration. The context contains one or more class assertions, which is
a list of classes each with their respective type variables, asserting
that a type variable is a parameter of a particular class. The context
for the above example includes two previously defined classes. The Eq
class is defined in the Haskell prelude and our user defined Named
class.  The instance asserts:
If  (type of name is an instance of the Eq class) and
 (type pair (object, name) is an instance of  Named)  then
                                      object is an instance of Eq
The Eq instance is quite general, it asserts that every type object is
an instance of the Eq class.  It does not say that every type object
that is an instance of Named is also an instance of Eq.
Now we consider the definition of equality (==) for the type object in
the instance body. Initially, the definition determines the type name in
a type->type dependency (e.g. via the function call namef object1). When
the two names have been calculated the function uses this information to
define equality on values of type  object via equality on values of type
name.



















Dan Doel wrote:
> 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