---
title: 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](https://wiki.haskell.org/Currying)):
> 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](https://en.wikipedia.org/wiki/Successor_function)):
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!