Dependent types have been gaining a lot of attention among programmers. Some

would say it's "the next thing" in programming. Why is it gaining popularity? In

this post, I hope to show some of the advantages of dependent types and get you

started on programming in dependent types.

To understand dependent types, let's take a step back and review what *types* are.

## What are types?

From *Programming in Martin-LΓΆf's Type Theory*: "Intuitively, a type is a

collection of objects together with an equivalence relation. Examples of types

are the type of sets, the type of elements in a set, the type of propositions,

...the type of predicates over a given set." Let's look at some of these

examples in detail.

### The type of sets

"To know that `A`

is a set is to know how to form the canonical elements in the

set and under what conditions two canonical elements are equal."

Canonical elements are evaluated expressions or values.

In a universe of small types, which contains all types except itself, the type

of sets is called `Type`

(or sometimes `Set`

). Elements of `Type`

include the

type of *natural numbers*, the type of *booleans*, etc.

### The type of propositions

What are propositions? "To know that `A`

is a proposition is to know that `A`

is

a set." That is, propositions are types! This leads to an important

feature/advantage of dependent types: types can depend on propositions!

What does it mean for a proposition to be true? "To know that the proposition `A`

is true is to have an element `a`

in `A`

."

For example, from Idris's documentation `onePlusOne`

below is a proposition of the *equality type*, the only constructor it has is `Refl`

, which stands for *reflexivity*.

```
onePlusOne : 1+1=2
onePlusOne = Refl
```

Thus, the only way to construct the `onePlusOne`

type is via the `Refl`

constructor, which we can only use if the left and right hand sides of the

equality sign evaluate to the same thing.

## What are *dependent* types?

A dependent type is a type whose definition depends on a *value*. The classic

example is `Vector A n`

, which is a `list`

of type `A`

with a specified length

`n`

. The `Vector`

type depends on a natural number (the value).

In a dependently typed language, types *are* values. But in a language like

Haskell, there is a distinction between *polymorphic* and *dependent* types.

`Vector A n`

is both polymorphic and dependent. It's polymorphic because it can

take any type `A`

. It's dependent because its output type depends on a *value*

`n`

.

## A datatype definition for dependent types

Here I present a definition of datatype that allows for dependent types. It's similar to Agda's.

In a universe of small types, we declare a datatype `D`

, of type `π© β Type`

, as follows:

```
data D (pβ : Pβ) ... (pβ : Pβ) : π© β Type
cβ : π«β β D pβ ... pβ tβΒΉ ... tβΒΉ
...
cβ : π«β β D pβ ... pβ tβα΅ ... tβα΅
```

That's a lot of symbols! Let's go through them in detail:

`D`

is the name of the datatype.- The colon
`:`

is read as "is of type". E.g.,`pβ : Pβ`

should be read as`pβ`

is of type`Pβ`

. `D`

takes in two types of inputs:*parameters*and*indices*.**Parameters are the same for all constructors, indices can vary from constructor to constructor.**`pβ ... pβ`

are**parameters**of`D`

. They are declared after the name of the datatype.- The indices of
`D`

are of types`π©`

. `cβ ... cβ`

are**constructors**of`D`

. They take arguments`π«α΅’`

and have the return types`D pβ ...`

where

pβ tββ± ... tββ±`tββ± ... tββ±`

are the arguments of the indices of`D`

.

The following sections I illustrate some example datatypes in this context.

### The type of natural numbers

The datatype of *natural numbers* can be introduced by:

```
data Nat : Type
zero : Nat
suc : Nat β Nat
```

`Nat`

is a datatype of type `Type`

. It has no parameter (there is no `p`

). It is not indexed (`π©`

is empty).

`zero`

is a constructor (`cβ`

) of `Nat`

. It doesn't take any argument (`π«β`

is empty). Its type is `Nat`

.

`suc`

is another constructor (`cβ`

) of `Nat`

. It takes a `Nat`

as an argument (`π«β = Nat`

). Its return type is `Nat`

.

### The type family of lists

The datatype family of *lists* is parameterised by `A`

, without being indexed:

```
data List (A : Type) : Type
nil : List A
cons : A β List A β List A
```

`List`

is a datatype of type `Type`

. It has one parameter, `pβ = A`

. The type of the parameter is `Type`

, so `Pβ = Type`

.

It is not indexed (`π©`

is empty).

`nil`

is a constructor (`cβ`

) of `List`

. It doesn't take any argument (`π«β`

is empty). Its type is `List A`

.

`cons`

is another constructor (`cβ`

) of `List`

. It takes two arguments, `π«β = A, List A`

. Its return type is `List A`

.

### The type family of vectors

The datatype family of *vectors* is parameterised by `A`

, indexed by the length

of the list:

```
data Vec (A :Type) : Nat β Type
vnil : Vec A zero
vcons : {n : Nat} β A β Vec A n β Vec A (suc n)
```

`Vec`

is a datatype of type `Nat β Type`

. It has one parameter, `pβ = A`

. The type of the parameter is `Type`

, so `Pβ = Type`

.

It is indexed by a `Nat`

, so `π©`

= `Nat`

.

`vnil`

is a constructor (`cβ`

) of `Vec`

. It doesn't take any argument (`π«β`

is empty). Its type is `Vec A zero`

, so `tβΒΉ = zero`

.

`vcons`

is another constructor (`cβ`

) of `Vec`

. It takes 2 arguments, `π«β = A, Vec A n`

(the type of `n`

is specified by the *implicit argument* to be

`Nat`

). Its return type is `Vec A (suc n)`

, so `tβΒ² = suc n`

.

### The type family of identity type

The family of *identity type* can be defined by

```
data Id (A : Type) (x : A) : A β Type
refl : Id A x x
```

`Id`

is a datatype of type `A β Type`

. It has two parameters, `pβ =`

,

A`pβ = x`

. The types of the parameters are `Type`

and `A`

, so `Pβ =`

,

Type`Pβ = A`

.

It is indexed by `x`

of type `A`

, so `π© = A`

.

`refl`

is a constructor (`cβ`

) of `Id`

. It doesn't take any argument

(`π«β`

is empty). Its type is `Id A x x`

, so `tβΒΉ = x`

.

### The type of `Even`

Dependent types can also be used to describe predicates. For example the

predicate of even numbers, `Even : Nat β Type`

, can be defined as follows:

```
data Even : Nat β Type where
even-zero : Even zero
even-plus2 : {n : Nat} β Even n β Even (suc (suc n))
```

`Even`

is a datatype of type `Nat β Type`

. It has no parameter.

It is indexed by a `Nat`

, so `π© = Nat`

.

`even-zero`

is a constructor (`cβ`

) of `Even`

. It doesn't take any argument

(`π«β`

is empty). Its type is `Even zero`

, so `tβΒΉ = zero`

.

`even-plus2`

is another constructor (`cβ`

) of `Even`

. It takes an

argument `Even n`

(the type of `n`

is specified by the *implicit argument* to be

`Nat`

) (`π«β = Even n`

). Its type is `Even (suc (suc n))`

, so

`tβΒ² = (suc (suc n))`

.

To construct `Even`

, the index has to either be

`zero`

, in which case we can construct`Even zero`

with`even-zero`

,- or
`suc (suc n)`

such that`Even n`

can be constructed. Using that`Even n`

and`even-plus2`

, we can construct`Even (suc (suc n))`

. Therefore, it has to be

`two = (suc (suc zero))`

or`(suc (suc two))`

and so on.

We've learned that dependent types allow us to define more intricate types

using parameters and indices. They also allow us to construct predicates and proofs. In

the next post, I will show some more real world dependent type programming!