# Nat-like Types, or Dynamic and Static Information

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.