When I first started teaching myself type-level programming in the context of Shapeless last year, I spent a lot of time working through simple problems with heterogeneous lists of type-level natural numbers. One fairly straightforward (but still non-trivial) example of such a problem is the second user story of this Coding Dojo kata, which is also outlined by Paul Snively in this email to the Shapeless mailing list.
The goal is to determine whether a list of numbers is the appropriate length (nine) and has a valid checksum, which is calculated by taking the sum of each element multiplied by its distance (plus one) from the end of the list, modulo eleven.
Writing a value-level implementation is easy:
We can confirm that this works as desired:
Suppose we want to write a type-level version instead—something like this:
Where this will compile:
But this won’t:
This is possible, but it requires an approach that’s a little different from the one we took in our value-level implementation. We’ll start by defining a type class that witnesses that a list
L of type-level naturals has a specific checksum
S (which is also a type-level natural):
Note that I’m using Shapeless 2.2.5—see the mailing list thread mentioned above for a version that works with Shapeless 1.2.4.
Now we’ll tell the compiler how to build up instances of this type class inductively. We start with our base case, the empty list:
This is pretty simple—we’re just providing implicit evidence that the checksum of the empty list is zero.
Next we need to deal with the case
H :: T, where
H is a type-level natural and
T is some list that we already know the checksum of. This is a little more complicated, so we’ll work in steps. First for the basics:
We’ve also said that we know the checksum of
T, which we can formalize like this:
We also need to know the length of
T in order to compute the checksum of
H :: T, so we’ll ask the compiler to find an instance of
Length.Aux is a type class provided by Shapeless that plays a role similar to that of our
HasChecksum—it just provides evidence that some
T: HList has length
TL <: Nat. (Note that this also means we need to add a new type parameter
TL <: Nat.)
Now we can take this product of
H and the length of
T plus one:
And add the result to the checksum for
And finally take the remainder of dividing that result by eleven:
Now we have all the pieces we need to write our type-level
isValid, which doesn’t even need a body, since all we care about is the fact that the compiler can assemble the appropriate pieces of evidence:
And we’re done:
See this thread on the Shapeless mailing list for some additional discussion, as well as this presentation from last year’s Strange Loop, where Paul Snively presents my original implementation as one of his examples of the power of type-level programming.