There's a very interesting Scala library called Shapeless that let's you do some weird things with types. One such "what magic is this?!" moment is asserting a checksum derived from a list of numbers is a certain value at compile time rather than run time.
This impressed me no end, even if I can't think of a practical use for it. I'm still trying to get my head around Travis Brown's excellent tutorial since he is so much more clever than me. But here are some notes I made along the way.
First, we borrow a bit from the Peano Axioms where every natural number is a successor to the previous except 0 which has no successor. We model this much like Shapeless does with something like:
trait NaturalNumber
trait NaturalNumber0 extends NaturalNumber
trait NaturalNumberSucceeds[T <: NaturalNumber] extends NaturalNumber
Next we'll have a type representing each and every number. I'll only bother with the natural numbers 0 to 4 to make things simple:
type Type0 = NaturalNumber0
type Type1 = NaturalNumberSucceeds[Type0]
type Type2 = NaturalNumberSucceeds[Type1]
type Type3 = NaturalNumberSucceeds[Type2]
type Type4 = NaturalNumberSucceeds[Type3]
This is just shorthand. Really, Type4 is of type:
NaturalNumberSucceeds[NaturalNumberSucceeds[NaturalNumberSucceeds[NaturalNumberSucceeds[NaturalNumber0]]]]
But that's far too verbose.
So much for the types, let's have some instances:
implicit val _0 = new Type0 {}
implicit val _1 = new Type1 {}
implicit val _2 = new Type2 {}
implicit val _3 = new Type3 {}
implicit val _4 = new Type4 {}
Now comes our first function that makes assertions at compile time. It asserts that T is the immediate successor to U and looks like this:
def immediateSuccessor[T <: NaturalNumberSucceeds[U], U <: NaturalNumber]: Unit = {}
And we can see it immediately working:
immediateSuccessor[Type3, Type2] // compiles
// immediateSuccessor[Type3, Type1] // doesn't compile because Type3 is not the immediate successor to Type1
A more useful examples tells us what is the successor without us having to assert:
implicit def add1[A <: NaturalNumberSucceeds[_]](implicit b: NaturalNumberSucceeds[A]): NaturalNumberSucceeds[A] = b
val result3add1: Type4 = add1[Type3]
Well, we assert insofar as we define the type of result3add1 but we didn't have to.
Subtraction proved a little more difficult for me to understand. Playing around with some Shapeless code I got this:
trait NaturalPair[A <: NaturalNumber, B <: NaturalNumber]
implicit def sub[A <: NaturalNumber, B <: NaturalNumber](implicit e: NaturalPair[NaturalNumberSucceeds[A], NaturalNumberSucceeds[B]])
= new NaturalPair[A, B] {}
So, A is the number we want to start with and then we reduce it by B. This implicit function will then recurse until one or the other reaches 0.
implicit val analyseThis = new NaturalPair[Type3, Type1] {}
val result3sub1 = implicitly[NaturalPair[Type2, Type0]]
// val result3sub1Wrong = implicitly[NaturalPair[Type1, Type0]] // doesn't compile because 3 - 1 != 1
Here we send into the implicit ether a request to take a 3 and subtract a 1. This is picked up by our implicit sub function that decrements both 3 and 1 until one or both reach 0. We then assert that a (2,0) pair is out there in the ether and indeed it is. Our code compiles.
The example Brown uses is much more complicated than this but I thought this would be a more accessible introduction.
