Hello from 2025. This is a reprint of a blog I originally posted on medium.com on Nov 26th, 2019, which I recall came out of a hackathon project at $WORK. I am moving it because (a), its nice to have all my writing in one place and under my control, and (b) medium kinda sucks.
The original, publication friendly title was “Rationality in a Natural World: Arithmetic at the Type-Level”. Similar to my note on the previous “From the Vault”, the code here was written using Scala 2.12.10, but I imagine it would be rather pain-free to rewrite in an up-to-date version. I would probably use somewhat fewer exclamation marks if I wrote this blog today. (!!)
Rationality in a Natural World
(A note from the future: I'm not sure where I sourced this original image from)
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!
Shapeless Nat
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:
trait _0 extends Nat trait Succ[P <: Nat] extends Nat
A simple natural number encoding
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
With 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:
trait Rat { type Numerator <: Nat type Denominator <: Succ[_] } type /[A <: Nat, B <: Succ[_]] = Rat { type Numerator = A; type Denominator = B }
introducing Rat
Syntax note: Numerator and 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.
trait Equals[A <: Rat, B <: Rat] object Equals { implicit def simpleEquals[A <: Nat, B <: Succ[_]]: Equals[A / B, A / B] = null implicit def equalsZeroCase[B <: Succ[_], D <: Succ[_]]: Equals[_0 / B, _0 / D] = null implicit def productEquals[ A <: Nat, B <: Succ[_], C <: Nat, D <: Succ[_], AtimesD <: Nat, BtimesC <: Nat ]( implicit ev1: Prod.Aux[A, D, AtimesD], ev2: Prod.Aux[B, C, BtimesC], eq: AtimesD =:= BtimesC ): Equals[A / B, C / D] = null }
Equals type-class
The goal is given two Rat s, 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)a = c and b = d ,
(b) a = c = 0 , or
(c) 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:
def equality[A <: Rat, B <: Rat](implicit ev: Equals[A, B]): Equals[A, B] = ev equality[_6 / _2, _3 / _1] // compiles equality[_2 / _6, _3 / _9] // compiles equality[_0 / _1, _0 / _7] // compiles equality[_4 / _7, _3 / _8] // does not compile
Equals works!
Simplifying things
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 Rat :
trait Mult[A <: Rat, B <: Rat] { type Out <: Rat } object Mult { type Aux[A <: Rat, B <: Rat, Out0 <: Rat] = Mult[A, B] { type Out = Out0 } implicit def multiply[ A <: Nat, B <: Succ[_], C <: Nat, D <: Succ[_], AtimesC <: Nat, BtimesD <: Succ[_] ]( implicit ac: Prod.Aux[A, C, AtimesC], bd: Prod.Aux[B, D, BtimesD] ): Aux[A / B, C / D, AtimesC / BtimesD] = null }
A first try at Mult
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 Rat:
- Don’t worry! We’ve got
Equals, so any time we want to compare the outputs of someRatoperations, 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:
trait Simplify[A <: Rat] { type Out <: Rat } object Simplify { type Aux[A <: Rat, B <: Rat] = Simplify[A] { type Out = B } implicit def zeroCase[B <: Succ[_]]: Aux[_0 / B, _0 / _1] = null implicit def nonZeroCase[ A <: Nat, B <: Succ[_], _GCD <: Nat, DivAOut <: Succ[_], DivBOut <: Succ[_] ]( implicit gcd: GCD.Aux[A, B, _GCD], divA: Div.Aux[A, _GCD, DivAOut], divB: Div.Aux[B, _GCD, DivBOut], ev: A =:!= _0 ): Aux[A / B, DivAOut / DivBOut] = null }
Making things simpler
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 a and b , gcd , then we divide both a and b by gcd , giving us our simplified result. And now we can use this as part of out multiplication implementation:
implicit def multiply[ A <: Nat, B <: Succ[_], C <: Nat, D <: Succ[_], AtimesC <: Nat, BtimesD <: Succ[_] ]( implicit ac: Prod.Aux[A, C, AtimesC], bd: Prod.Aux[B, D, BtimesD], simplify: Simplify[AtimesC, BtimesD] ): Aux[A / B, C / D, simplify.Out] = null]
A better Mult?
and prove that it works as intended with the following tests:
def multiply[A <: Rat, B <: Rat](implicit ev: Mult[A, B]): Option[ev.Out] = Option.empty[ev.Out] multiply[_2 / _5, _3 / _2] : Option[_3 / _5] multiply[_1 / _2, _0 / _12] : Option[_0 / _1] multiply[_1 / _2, _1 / _4] : Option[_1 / _8] // all compile!
Testing Mult
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:
trait Div[A <: Rat, B <: Rat] { type Out <: Rat } object Div { type Aux[A <: Rat, B <: Rat, Out0 <: Rat] = Div[A, B] { type Out = Out0 } implicit def divide[ A <: Rat, C <: Succ[_], D <: Succ[_] ](implicit ev: Mult[A, D / C]): Aux[A, C / D, ev.Out] = null }
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 Succ[_] .
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.