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

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:

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:

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.

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:

## 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` :

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:

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:

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 `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.