Dependent Function Types

Dependent function types allow the return type of a function to refer to the argument value of the function. The classic example is “vectors”, which are like lists but have a statically-checked length. Here’s an example function involving vectors:

duplicate : (t : Type) -> t -> (n : Nat) -> (Vector n t)

We read a : b as “a has type b”, or “a is a b”, so this type signature says that duplicate is a function of 3 arguments: the a -> b notation means a function from argument type a to return type b, and multiple “arrows” like a -> b -> c can either be interpreted as:

a function taking an a and returning a b -> c

or (equivalently):

a function taking an a and a b and returning a c

Argument types are written in one of two ways: if they’re written like a (for example Int or String), then the type of the argument is a; if they’re written a : b (for example age : Int) then the argument type is b, but later types can refer to the value as a. Note that this is overloading the a : b notation for type annotations. I think of annotations like duplicate : ... as “constructing” (introducing) a type-annotated value: given a name and a type, we get a typed value; inversely, when we have a typed value, like a function argument, we can “destruct” (eliminate, or pattern-match) it to get a name and a type. This might be just a notational pun, but it fits nicely into the existing concepts of constructing and destructing data.

So this signature says that the first argument of duplicate is called t, and it is a Type. The second argument has type t; this means the type of the second argument depends on the value of the first argument: if we call duplicate with Bool : Type as the first argument, then the second argument must be a Bool.

The third argument is called n, and has type Nat (natural numbers: i.e. the positive integers including zero). The return type is Vector n t, i.e. a list of length n containing elements of type t.

Note that we’re referring to argument values by name, but we don’t know what particular value they will be (i.e. which number n will be, or which type t will be). We can think of a : b as being “for all a of type b”.

If we think about functions returning lists, like map or reverse, we can “cheat” by having them always return an empty list; such functions satisfy their type signature (they return a list), but don’t behave in the way we want.

In contrast, the “for all” nature of dependent function types can be used to prevent this sort of “cheating”. The duplicate function can’t just return an empty vector, since it must return a vector of length n, and the implementation must work for all values of n. We’re forced to write a function which constructs a vector of the correct length: empty when n is zero, or non-empty otherwise.

To construct a non-empty vector, we need to put a value inside it. What value can we use? We can’t “cheat” by using, say, the value "hello", since that would give us a vector containing String, whilst our return type forces us to make a vector containing t. Whatever our function does, it must work for all values of t (String, Bool, Int, Vector 5 (Int -> Bool), etc.).

Since we don’t know what t will be, we can’t “invent” a value of the right type. The only thing we can do is use an existing value which will always have type t. The only way something can have type t is if it appears in our type signature, since that’s the scope of the name t. The only thing in our type signature which has type t is the second argument. Hence we must use the second argument as the elements of our vector (if it’s non-empty).

One implementation which satisfies this type is the following (assuming that Nat is encoded as Peano numerals):

duplicate t x n = case n of
                       zero   -> vectorNil t
                       succ m -> vectorCons t x (duplicate t x m)

This isn’t the only possible implementation, for example we might choose to send the recursive call through a vectorReverse function (although it would be pointless), but such differences cannot alter the input/output behaviour of the function.

Of course, we don’t have to use dependent function types to restrict all of a function’s behaviour. If we think back to the map example, we take a function of type a -> b, a List a and must return a List b: the easiest thing to do is return an empty list, which satisfies the type but isn’t what we want.

If we instead make a vectorMap function, where List is replaced with Vector n, then that “cheat” no longer works (since an empty vector doesn’t always have length n). We could still mess around with the contents, like reversing it or doing some other permutation, but that’s harder than just doing the right thing. The path of least resistance is to write a correct implementation!