In this article we are going to take a step beyond natural numbers, and derive a type-level encoding of (positive) rational numbers in Scala. We’ll show how we can leverage natural number arithmetic to perform arithmetical operations on our new type-level rationals, all at compile-time. We’ll start with a quick refresher of how the naturals can be encoded at the type-level, before jumping deeper into some arithmetic using the new rational number types!
Those familiar with the Scala library shapeless may well have come across or used the type
Nat , which encodes at the type-level a representation of the natural numbers — 0, 1, 2, and so on. This is achieved using an encoding known as Peano numbers — with 0 being represented by one type, and the successor operation represented by another:
From this simple pair of types all natural numbers can be represented by a type —
type _1 = Succ[_0] ,
type _2 = Succ[_1] , and so forth. And we aren’t just limited to counting using these types; through a myriad of type classes defined in shapeless we can also perform all sorts of natural number arithmetic, all at the type-level. Addition, multiplication, and powers of
Nat s can all be calculated at compile time. We will need a few of these type classes going forward, so if you aren’t that familiar with compile-time arithmetic already I can definitely recommend checking out Counting At Compile Time, by James Phillips.
Twice the Nat, twice the fun
Nat in our back pocket, we are ready to encode (positive) rational numbers at the type-level. Rational numbers are made up of two parts, a numerator, which can be any natural number, and a denominator, which is a strictly positive natural number. With this in mind, we can naturally define our rational type-class, which we’ll be calling
Rat , as follows:
Denominator are given as inner types so in type signatures we can write
[A <: Rat, ...] instead of having to write the more cumbersome
[A <: Rat[_, _], ...] . We then include the helper type
/ so we can use Scala’s infix type syntax to write things like
_1 / _2 .
Now before we even get into adding or multiplying, we are faced with a problem that is not faced by
Nat : equality. While in
Nat equality of naturals can be equated with equality of types, we aren’t warranted the same luxury with
Rat . While
_2 / _3 and
_4 / _6 both represent the same rational number, as types they are different. So our first challenge is to write an
Equals type-level operation.
The goal is given two
A / B and
C / D , to be able to summon an implicit instance of
Equals[A / B, C / D] if and only if the rational numbers they represent are equal. We split this into three cases, that are encoded in the implicit defs above.
a/b = c/d if and only if either:
a = c and b = d ,
a = c = 0 , or
a * d = b * c .
Strictly speaking only case (c) is necessary: it implies (a) and (b). But we encode those special cases separately for efficiency when it comes to implicit search. We can check this works by hitting the compile button on the following:
This problem faced by
Rat is going to come back to haunt us whenever we comes to deriving type-level arithmetical operations. What we would like is that even though there are many ways a single rational number can be expressed, we can ensure that operations on equal, but differently expressed rationals produce the same result. Consider as an example of this issue a type class that encodes multiplication for
Here the result is reached simply by multiplying the numerators and multiplying the denominators. But we might think that this is a not a well-defined operation. Shouldn’t expect the output of
Mult[_1 / _2, _4 / _5] and
Mult[_2 / _4, _4 / _5] to be the same type (in terms of type equality)? Well, maybe. There are two lines of thinking we can take with all of the operations we might want to define for
- Don’t worry! We’ve got
Equals, so any time we want to compare the outputs of some
Ratoperations, we can just use that.
- That sounds like hard work. Can’t we bake a simplification step into our basic operations?
I like option 2 for a couple of reasons. Firstly, it means the outputs of functions are in their canonical representation without having to do any extra work as a user, which I think is more elegant. Secondly, it doesn’t require a user to know anything about how the operation is implemented (except that it simplifies the result!) in order to know what the output type is going to be. As a pathological example, if we were being dummies and as part of our
Mult implementation we always multiplied the result by
_2 / _2, the algorithm would give an unexpected, albeit correct, result. But if we always then simplified as the final step of the algorithm, the user doesn’t have to care about things going on under the hood that may affect the output. As a bonus reason why I like this solution, it means writing a
Simplify type-class, which is fun!
And here is what
Simplify looks like:
The implicits consist of two cases: the special zero case, where
_0 / N for any
N gets simplified to
_0 / _1 , and the general, non-zero case. To put a rational number
a/b into its simplest terms, we find the greatest common divisor of
gcd , then we divide both
gcd , giving us our simplified result. And now we can use this as part of out multiplication implementation:
and prove that it works as intended with the following tests:
Can Nat do this?
As a final sample of the operations we can perform at the type-level with
Rat, let’s look at something that can be implemented for
Rat , but not for
Nat — division. Now, you will notice that we did use the type-class
shapeless.Div in our implementation of
Simplify , but the operation this performs is better described as Euclidean division — or division with remainder — where the remainder is discarded, and we are left with a natural number “quotient”. When working with rationals, we can perform a “truer” division operation, one that is the formal inverse of multiplication. And, given that we already have a multiplication operation implemented, our
Rat -y version of
Div is remarkably easy to implement:
The only thing we have to watch out for is that division by 0 is ill-defined, so we ensure that the numerator of the divisor is non-zero by giving its type-bound as
That’s all for now! If you want to have a play with any of the other type-classes I’ve implemented for
Rat , check out the repository here. In terms of what’s next, I’d like to implement a version of
Rat that is a lot, lot faster, and that can make much larger compile-time calculations.
Nat is particularly slow due to using Peano numbers to define it, and here James Phillips (again) details a version of
Nat that is magnitudes faster. Using this as a basis for
Rat would unlock the same speed boosts for us.