Over the past few weeks, I’ve been experimenting with Idris. One of the key things about this language is that types are just values (with type `Type`). This means you can use normal values in type signatures, such as natural numbers. Idris uses the peano construction of the natural numbers. The parts of the axioms that are of use here are:

• 0 is a natural number.
• For every natural number n, S(n) is a natural number.

These can be easily expressed in Idris by

Then they can be just used in other type signatures, for example a length-encoded list

This gives us types such as `Vect 1 Nat`, which contains only single-element lists with elements belonging to the type `Nat`. This is a different type to `Vect 2 Nat`, which contains all 2-element lists with elements belonging to the type `Nat`.

This is easy in Idris, but how would we do it in a more everyday language, C#?

This lets us construct natural numbers at the type level. So the type `Zero` represents the number `0`, `Succ<Zero>` represents the number `1`, `Succ<Succ<Zero>>` represents the number `2`, and so on.

We can then create a `Vector` type, a linked list which is parametrised by it’s length. Just like the Idris example, a member of the type `Vector` is either an empty vector (of length 0), or it is a vector of length n+1, constructed from an element (known as the head) and a vector of length n (known as the tail). In the absence of sum types, we’ll use inheritance to model these two possibilities.

The name `Cons` is standard in functional programming languages. It seems to come from Lisp.

Because type parameter inference does not work for constructors, we need to create some helper functions to give us more terse syntax for creating these vectors.

Okay, so we can create and print our length-encoded lists. But we can’t do much else with them yet, so let’s define some of the fundamental operations for lists: `Map`, `ZipWith` and both left and right fold.

Unfortunately, we have to do a typecast in `ZipWith`, because the compiler does not know that if something is a non-empty vector, it must be of type `ConsVector`. In fact, this assumption isn’t actually true, because somebody else could subclass `Vector` and pass it to `ZipWith`. But we’ll ignore this possibility.

So now we can do stuff like

But if we try to zip `vect1` and `vect3`, we get a type error:

``````The best overloaded method match for `Vector<Nat.Succ<Nat.Succ<Nat.Succ<Nat.Zero>>>,int>.ZipWith<int,int>(System.Func<int,int,int>, Vector<Nat.Succ<Nat.Succ<Nat.Succ<Nat.Zero>>>,int>)' has some invalid arguments
Argument `#2' cannot convert `ConsVector<Nat.Succ<Nat.Succ<Nat.Succ<Nat.Zero>>>,int>' expression to type `Vector<Nat.Succ<Nat.Succ<Nat.Succ<Nat.Zero>>>,int>'
``````

Awesome.

Open questions:

• To append two vectors, we need to sum two type level naturals. Is this even possible?
• How useful is this in practice? For example, how do we convert user input to these vectors?