# 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!