A genuine type-level computation.

Our Nat are now ordered.

(Lt, Gt, Gte can all be defined similarly or derived from one another)AdditionThe 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 typeWhich 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 writteninstead 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.

.. More details