Counting at compile time
Counting at compile time is one of the world’s simple pleasures. We have taken the scala compiler and hacked something in to it to make it do things it really doesn’t look like it should be doing.
The standard approach of ‘counting at compile time’ utilises a type commonly called Nat. It’s available in libraries such as shapeless. We have types available, that look like this: type _13 = <something> — this represents the number 13. <something> is yet to be revealed.
Through type-class trickery and a clever definition of something we can make the compiler perform magic for us, and turn two types such as _13 and _3 into a third type _16 by ‘adding’ them together, all at compile time. You can, of course, also make it do any other arithmetic operation you can dream of, if you have the time to implement it.
A use-case might look a bit like this:
Here, Sum is our yet-to-be-defined typeclass which adds two Nat together. s.Out is an inner type of this typeclass, representing the sum of A and B. The magic thing is if A=3 and B=7 then the return type is 10 — not just a normal path-dependent types.Out.
Why do we want to do this? Because we can! So let’s.
Nat Definition
Here’s what a bare-bones Nat implementation looks like:
You can go as high as you like, but eventually the compiler starts complaining as the type nesting gets too deep.
You can see that each number is just defined as the successor of the previous number. The full expanded type of _3 would be Succ[Succ[Succ[_0]]] for example. In any calculation we do, we could peel off a layer of _3 and then perform our calculation recursively on _2. This is how the majority of Nat typeclasses (and type-level programming typeclasses in general) work.
ToInt
You may have noticed that these are purely types. Nothing else. No runtime version exists of these things, in this version of Nat I’ve just cobbled together. (Unless you did new _3 {}, but there’s really no reason to do that).
But, it’s a perfectly reasonable request to want to take a type N <: Nat and have the runtime integer it represents, n.
This could be done with macro magic, as in shapeless, or by defining companions like the following explicitly:
But I will forego these and derive the integer representations implicitly, as an example of a very simple compile-time calculation we can do on these Nats.
We need a type-level function which takes in one type, a Nat, and spits out a run-time value Int. A compile-time (or type-level) function is a trait, and its arguments are its type parameters. The return of the function (either a type or a value) is contained within the trait. So it looks like this:
You can see how this would now work. If, in our code, we found ourselves in possession of a val i: ToInt[_3] instance, we could do i.value to get the run-time representation of _3. Which we hope would be 3.
How do we find ourselves in possession of these objects? We generate them implicitly, for every Nat. And then they’re available automatically for us whenever we need them.
Of course, implementing one implicit for each Nat would be horrendous. But remember above, where I pointed out _3 is one layer of Succ wrapped around _2. If we knew the result of _2 we might in theory be able to calculate our instance for _3. This is induction/recursion, so here’s what ToInt looks like:
Now you can do the following:
and we have turned our completely arbitrary Nat construction into real runtime integers!
Comparisons
That’s all well and good, we ‘proved’ our Nat can make sense as real integers. But we didn’t do any real compile time calculation on them.
The next step would be to have a typeclass which proves one Nat is less than or equal to another. Say this typeclass was called Lte (for ‘less than or equal’). Then an instance of type Lte[A, B] would be available implicitly if and only if A <= B (well, if their runtime representations held that relationship).
So it’s a typelevel function which has two arguments this time, and no return value or type: we just make it not available implicitly for invalid arguments. This would be roughly equivalent to an exception in a runtime algorithm.
So it’s very simple and looks like this:
Now we have to generate the implicit instances, again recursively. They are again reasonably simple:
So say we were trying to compute Lte[_3, _5]. Then we would call succCase implicitly with the arguments _2 and _4, since we peeled away one layer of Succ on both arguments. We would continue peeling away until we tried to compare _0 to _2, where we could call zeroCase and finish our recursion. We’d then zip back up the stack and return a value of type Lte[_3, _5].
If, on the other hand, we were searching for a value of type Lte[_5, _3], we would as a first step look for Lte[_4, _2] and so on. Eventually we would search for Lte[_2, _0]. However, zeroCase isn’t applicable since the _0 is on the right instead of the left. And succCase isn’t applicable since _0 is the Succ of no integer.
So we cannot compile a value of type Lte[_5, _3] — as we would expect since 5 is not less-than-or-equal to 3.
You can try it in a repl:
which is great! A genuine type-level computation. Our Nat are now ordered.
(Lt, Gt, Gte can all be defined similarly or derived from one another)
Addition
The big one.
This is the first time our typelevel computation returns a type as its result, rather than a value. We could, of course, add two Nat and return their runtime sum instead of their compile time sum if we wanted, but that would be boring.
So, we’re going to write a typelevel function Sum which takes two summands, and returns a type. It looks like this:
Notice that the return type Out is an inner type, not in the type parameter list. This is because if you wanted to summon an implicit Sum[A, B, Out] then you would always have to know the sum of A and B before you could summon it, which would ruin the point. Instead we want to summon a Sum[A, B] and have the compiler work out the innards for us.
We’re going to implement this naïvely at first, as we would want to write it, and then fix it when we realise the compiler won’t let us do that.
So, how do you add two numbers a and b together if all you can do is peel one layer of Succ off, and recurse?
Well, suppose we could write a = z + 1, for some z. Which we definitely can do, for every a except 0. Then we can see that a + b = z + (b + 1).
That seems like a recursive step to me. We just need to plug in the zero case on top of it.
So, Sum could look like this:
Note here the return types. What we want to say is that the type of the implicit we’re generating is Sum[Succ[A], B] { type Out = sum.Out }, where the inner type has been fully realised as a type we calculated (in this case sum.Out). Unfortunately this is not valid scala (though it should be) — but we’ll ignore this for now and examine the algorithm.
If you imagine searching for a Sum[_3, _2], what would happen? We would examine succCase, and then recursively search for a Sum[_2, _3]. Then a Sum[_1, _4], and then finally a Sum[_0, _5], which is provided by zeroCase. We see the result of Sum[_0, _5] is just _5 ( type Out = B )- so we take this value, zip back up the stack and plug in the type _5 and we get an instance of type
Which works wonderfully… nearly.
Unfortunately due to limitations in scala the above type is not expressible in the position of a return type (or argument type come to that) of a function. We can’t specify inner types at that position. But we have to — we need to tell the compiler what the inner type is as the return type so it’s available at compile time rather than runtime.
Thankfully, someone once upon a time came up with a horrible hack known as the ‘aux pattern’ (aux meaning auxiliary). This is where we recognise such an expression is invalid, and we simply substitute a dummy type which is valid.
So we define this:
Think of Aux simply as an alias for what we actually want to express. Now we can revisit Sum and write it like this:
We’ve simply substituted Aux in. And, amazingly, this now works. You can test it yourself:
and we’re done! Genuine calculations performed purely at compile time. You can of course go further and define multiplication, or lowest common denominator, or exponentiation, or whatever you want.
A quick note about the aux pattern. Let’s take zeroCase as an example. If we had written
instead of using the aux pattern, then the Out type B would not be known to the compiler, it would be a runtime thing only. So in this case, in our test sum[_0, _6] above, the return type would be a path-dependent s.Out and would not be fully realised as _6. Putting the return type in the type of the implicit definition elevates the runtime calculation to compile time, and the Aux pattern allows us to do genuine typelevel calculations.
