# Nat-like Types, or Dynamic and Static Information

Posted on by Chris Warburton

This is based on an explanation I gave on the Idris mailing list about using dependent types to prove that a Vector contains some element.

# The Skeleton

All of the types in this post will be variations of the `Nat` type. If you’ve not encountered it before, take a look at Peano arithmetic.

## `Nat`

`Nat` has two constructors:

``````Z : Nat
S : Nat -> Nat``````

These can be combined in an infinite number of ways: `Z`, `S Z`, `S (S Z)`, etc.

From a static (typing) point of view, `Nat` doesn’t tell us very much at all, since it can always be trivially satisfied with `Z` (`Z` is a lot like `()` or `NULL`).

From a dynamic (value) point of view, the only thing a `Nat` tells us is how many `S` constructors it has.

Hence, we can think of `Nat` as being the Natural numbers (the ‘counting numbers’, where we’re counting how many `S` wrappers there are around `Z`).

We can define types similar to `Nat` which are more informative, both statically (stronger types) and dynamically (contain more data).

# Static Information

These types start with `Nat` and add static information (ie. stronger types).

## `Exactly n`

We can define a strange type `Exactly n` which is like `Nat`, except it stores a `Nat` in its type too:

``````data Exactly : Nat -> Type where
eZ : Exactly Z
eS : Exactly n -> Exactly (S n)``````

Dynamically, an `Exactly n` value is like a `Nat`: all we can use it for is counting. We can see this if we throw away the static information:

``````plain : Exactly n -> Nat
plain eZ = Z
plain (eS n) = S (plain n)``````

However, we have more static information: an `Exactly n` value will have `n` occurences of the `eS` constructor, hence it guarantees the following:

``````guarantee : n -> Exactly n -> Bool
guarantee n e = plain e == n``````

In other words, `Exactly n` is like ‘all Naturals which are equal to `n`’.

## `Fin t`

We can change our constructors slightly to make a useful type called `Fin n`, which is a lot like `Exactly n` except for the guarantee that it provides. It has two constructors, just like `Nat` and `Exactly n`:

``````fZ : Fin (S n)
fS : Fin n -> Fin (S n)``````

Once again, we can throw away the type information to get back to `Nat`:

``````plain : Fin n -> Nat
plain  fZ    = Z
plain (fS n) = S (plain n)``````

Hence, dynamically a `Fin n` is also just a counter like `Nat`.

Statically, the guarantee we get from `Fin n` is that it has exactly `n` possible values (try it for `n` = `0`, `1`, `2`, … and see!).

The extra type information guarantees that:

``````fin : n -> Fin n -> Bool
fin n f = plain f < n``````

Hence we can think of `Fin n` as being like ‘the Naturals up to `n`’. For more info, see this informative StackOverflow answer

## `NatLTE n m`

`NatLTE n m` is like `Exactly n` but it stores two `Nat` arguments in its type. Again, its constructors follow the same basic pattern as `Nat`:

``````nEqn : NatLTE n n
nLTESm : NatLTE n m -> NatLTE n (S m)``````

We can throw away the type info to get:

``````plain : NatLTE n m -> Nat
plain nEqn = Z
plain (nLTESm n) = S (plain n)``````

Notice that again, dynamically we’re just left with a counter. However, we have some static guarantees about the value of that counter.

Notice that the two `Nat` values in our type must start out the same, although unlike `eZ` they can start at any value. Just like `eS` and `fS`, we add an `S` with the `nLTESm` wrapper, although we also have another `Nat` which gets passed along unchanged.

The guarantee for `NatLTE n m` is:

``````guarantee : n -> m -> NatLTE n m -> Bool
guarantee n m x = n + (plain x) == m``````

Hence we can think of `NatLTE n m` as being ‘`Nat`s which, when added to `n`, produce `m`’ or equivalently ‘proof that `n` is less than or equal to `m`’.

## `Elem x xs`

`Elem x xs` is like `NatLTE n m` except its type can contain more than just `Nat` values. Again, its constructors follow the same basic pattern as `Nat`:

``````Here : Elem x (x::xs)
There : Elem x xs -> Elem x (y::xs)``````

We can throw away the type information to get a `Nat`:

``````plain : Elem x xs -> Nat
plain Here = Z
plain (There n) = S (plain n)``````

Again, dynamically a value of `Elem x xs` is only useful as a counter. The static guarantee we get is the following:

``````guarantee : x -> xs -> Elem x xs -> Bool
guarantee x xs e = index' (plain e) xs == Just x``````

It does this by using `Here : Elem x xs` to tells us that `x` is the head of `xs`, whilst `There` tells us that `x` appears somewhere in the tail of `xs`.

Hence we can think of `Elem x xs` as being ‘proof that `x` is somewhere in `xs`’.

We get compile errors if we change the `Here` and `There` values in a program, because we’re changing the proof. Since the proof tells Idris what the index of the element is, changing that index makes the proof wrong and the compiler rejects it.

# Dynamic Information

These types start with `Nat` and add dynamic information (ie. data).

## `List t`

`List t` follows the same constructor pattern as `Nat`:

``````Nil : List t
Cons x : List t -> List t``````

The argument to `Cons` (the `x`) adds dynamic data to the basic “count the constructors” information found in `Nat`. Note that we gain no static information, regardless of what `t` is, since we might always be given a `Nil`.

We can throw away the dynamic information to get a `Nat`:

``````plain : List t -> Nat
plain Nil = Z
plain (Cons _ xs) = S (plain xs)``````

In the same way that we went from `Nat` to `Fin n`, you might try making a new type `FinList n t` for ‘all lists of `t` up to length `n`’.

In the same way that we went from `Fin n` to `NatLTE n m`, you might try making a new type `SuffixList l1 l2` for ‘proofs that `l1` is a suffix of `l2`’.

## `Delay t`

`Delay t` is like `List t`, except it can only store data in the `Nil` constructor, not the `Cons` constructor. For this reason, we rename the constructors to `Now` and `Later`, respectively:

``````Now x : Delay t
Later : Delay t -> Delay t``````

If we throw away the dynamic information, we get a counter like `Nat`:

``````plain : Delay t -> Nat
plain (Now   x) = Z
plain (Later x) = S (plain x)``````

What about the static information? `List t` was trivial for all `t`, since we can satisfy it with `Nil`. We can’t do that with `Delay t`, since `Now` requires an argument of type `t`.

In fact, we can satisfy `Delay t` trivially, by using `Later`:

``````loop : Delay t
loop = Later loop``````

This defines a never-ending chain of `Later (Later (Later (Later ...)))`. Since we never terminate the chain with a `Now`, we don’t have to provide a value of type `t`.

This kind of circular reasoning is called co-induction, and is logically sound as long as each constructor can be determined by a terminating function (in this case, we just step along the chain until we reach the desired depth, pattern-matching the (constant) constructors as we go). This condition is called co-termination.

If a function doesn’t terminate or co-terminate, it diverges. We can use `Delay t` to handle diverging functions in a safe way. For example, the Halting Problem tells us that it’s impossible to calculate whether a Universal Turing Machine will halt for arbitrary inputs; ie. the UTM might diverge. However, we can always perform each step of the UTM in a finite amount of time.

If we wrap the result of our UTM in a `Delay`, we can return a `Later` for each step, and if it does eventually halt we can return a `Now`. Whenever it diverges, our program doesn’t freeze; instead, we get the same `Later (Later (Later ...))` chain as `loop`, which we can inspect to various depths.

## `Vect n t`

`Vect n t` itself is a bit like `FinList n t`, except instead of containing all lists up to length `n`, it contains only lists of length `n`. It follows the same constructor pattern as `Nat` and `List t`:

``````Nil : Vect Z t
Cons x : Vect n t -> Vect (S n) t``````

Notice that the `Nat` in the type of `Nil` is forced to be `Z`, instead of being `S n` for all `n` like in `Fin` (hint, that’s the difference between `Vect` and `FinList` ;) )

If we throw away the static information of `Vect n t` we get a `List t`:

``````plain : Vect n t -> List t
plain Nil = Nil
plain (Cons x xs) = Cons x (plain xs)``````

If we throw away the dynamic information, we get an `Exactly n`:

``````plain : Vector n t -> Exactly n
plain Nil = eZ
plain (Cons _ xs) = eS (plain xs)``````

## Conclusion

We can add dynamic information (values) to a type by adding arguments to the constructors; this takes us, for example, from `Nat` to `List t`.

We can also add static information to a type by adding arguments to the type (“strengthening” it), and use the constructors to guarantee some invariant between all these values (ie. we don’t provide a way to construct an invalid value).

The simple pattern of two constructors: one which gives a `Foo` and another which turns a `Foo` into a `Foo`, is very powerful, and can represent all kinds of ‘linear’ things, including counting, lists, bounds, linear relationships, lengths, indexes, etc.