# 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
: Exactly Z
eZ : Exactly n -> Exactly (S n) eS
```

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:

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

However, we have more static information: an `Exactly n`

value will have `n`

occurences of
the `eS`

constructor, hence it
guarantees the following:

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

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`

:

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

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

:

```
: Fin n -> Nat
plain = Z
plain fZ = S (plain n) plain (fS 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:

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

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`

:

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

We can throw away the type info to get:

```
: NatLTE n m -> Nat
plain = Z
plain nEqn = S (plain n) plain (nLTESm 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:

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

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`

:

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

Again, dynamically a value of `Elem x xs`

is
only useful as a counter. The static guarantee we get is the
following:

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

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`

:

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

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`

:

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

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`

:

```
: Delay t
loop = Later loop 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`

:

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

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

:

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

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