I was recently browsing through some of the source code for narya, and I noticed a pattern that Shulman was using in order to do type-level programming in a non-dependently typed language. If you want to see the code that I read to figure this out, you can look at n.ml.
Part 1 of this pattern is to encode unary numbers via type constructors. This works like
type zero = Dummy_z
type 'a suc = Dummy_s
One can then represent the number 4 as the type (((zero suc) suc) suc) suc (note that in ocaml, type constructors are applied on the right).
Part 2 is to use these type-level numbers to index GADTs. GADT stands for “generalized algebraic data type”, and you should really read an introduction to these elsewhere if you haven’t seen them before.
We can, for instance, use these to give a fixed-length vector type.
type (_, _) vec =
| Empty : (zero, 'a) vec
| Cons : 'a -> ('n, 'a) vec -> ('n suc, 'a) vec
This is interesting, because the kind signature for vec is type x type -> type. There’s nothing that says that the first argument has to be a type-level natural number. However, if we look at the constructors for vec, we can see that in fact it’s impossible to construct an element of vec ('b, 'a) if 'b is not of the form (...(zero suc)...) suc.
So this lets us actually use type-level unary numbers to meaningfully constrain values. But that’s only half of the picture; in order to well-type operations like concat, we need to perform operations on type-level unary numbers! We can’t do this the naive way, which would be to write a function type x type -> type, because, for one, there are plenty of elements of type which don’t represent unary natural numbers.
So Shulman uses a trick: instead of encoding addition as a function, he encodes it as a relation n + m = l. This can be done in the following way.
type (_, _, _) plus =
| Zero : ('n, zero, 'n) plus
| Succ : ('n, 'm, 'l) plus -> ('n, 'm suc, 'l suc) plus
There are then some other tricks to transform plus into a function and so on, but I want to just focus for now on the philosophy of this above trick. Essentially, the idea is that the existence of a term for some GADT can prove that some relationship holds between types, and this relationship can be inductively defined. If you are familiar with prolog, this should look very familiar! You can think of a GADT as defining a prolog-style relation on type, where each constructor gives a different :- rule. So in a prolog-type syntax, we’d have
:- plus(N, zero, N)
plus(N, M, L) :- plus(N, suc(M), suc(L))
Now, prolog would then allow us to query things like plus(2, 3, ?), but there’s no analogous capability in ocaml; Shulman has to build this in manually. But that makes me think; could one give a minimal extension of Standard ML in which GADTs really did work like prolog relations, e.g. where you could actually query them?
And I have some inkling that the answer is: yes, it’s called the Haskell typeclass system. But that’s just a guess based on hearing that typeclass resolution is similar in some way to prolog. Anyways, that’s all for now!