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.
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>'
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?