Rationality in a Natural World: Arithmetic at the Type-Level

Jack Wheatley
Nov 26 · 6 min read

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:

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:

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.

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:

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 :

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:

  1. Don’t worry! We’ve got Equals , so any time we want to compare the outputs of some Rat operations, we can just use that.
  2. 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:

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:

A better Mult?

and prove that it works as intended with the following tests:

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:

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.

Medium's largest active publication, followed by +536K people. Follow to join our community.

Thanks to James Phillips

Jack Wheatley

Written by

The Startup
Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade