# Fun with Types: All Types of Physics Computations

One of the first things you learn when you make computations involving Physical quantities is to *at least* check that the units match. For example, if your goal is to compute the gravitational force between two objects, you must at least check that the units of your answer are kg·m/s². It doesn’t prove that you have the correct answer, but is a required condition.

Developers also do that (although in an automated way) using **type checkers** of some kind. In compiled languages like Scala, it is one of the many things that the compiler do. If you ask some variable to be a `String`

, it will check that you don’t assign (directly or via a computation) a `Double`

to it.

Now, what if we could make the Scala compiler type checks our Physics computations? For example, we would define a bunch of variables, telling the compiler (via usual typing) that some are distances, some are times, some are masses. Then, we could make all sorts of computations with them and, at the end, requiring that the result is a force. If we make a mistake such as physical units don’t match, then it would simply not compile!

The goal of this blog post is to achieve that. We are going to define some clear design goals (to keep in mind while going through the implementation). Then, we will start the implementation, which will directly hit issues that we will overcome. We are going to make a small example about computing the gravitational force between the Earth and the Moon, and finish by discussing how one can test such thing (it’s not that trivial!).

If you would prefer to directly browse the accompanying repository, then you can head over here. A word of warning: when I first showed this to several people, they all separately answed with the same exact two words: my god (and not in a good way). So, you be warned.

# Design Goals

We need to define clear design goals of things we want for our implementation:

- There should
**not**be any**performance implication**. If we are making physics computations within a software, it’s probably either for an actual physics simulation, or perhaps a video game. In both cases, we can’t afford to sacrifice run-time performance for our compile-time safety - Computations should compile
**if and only if**the physical quantities match. We don’t want either false positive or negative, as this would downgrade the value of this feature - It should not affect the way we write the computations. We want this to be as seamless as possible and, if someone basically has to re-learn how to code for this feature, it is not worth it.

The first point will be achieved using **opaque types**. These are type alias (so, no affect on run-time) where the compiler “forgets” that they are alias outside of their scope of definition. That means that we can restrict what a user can do with them. Points 2. and 3. will be achieved by defining clever (if I can say so myself) type-level computations that Scala 3 offers built-in.

On the surface, our API will define the following `Physic[T <: PhysicQuantity]`

type as an opaque alias for `Double`

. The missing pieces will be the definition of these `PhysicalQuantity`

, `Meter/Second/Kilo/Scalar`

, `**:`

, `***`

or `InverseOfPhysicQuantity`

.

`opaque type Physic[T <: PhysicQuantity] = Double`

object Physic {

extension (value: Double) {

inline def withUnit[T <: PhysicQuantity]: Physic[T] = value

inline def meters: Physic[Meter **: Scalar] = value

inline def seconds: Physic[Second **: Scalar] = value

inline def kilos: Physic[Kilo **: Scalar] = value

inline def asScalar: Physic[Scalar] = value

}

extension [T <: PhysicQuantity](phys: Physic[T])

inline def +(other: Physic[T]): Physic[T] = phys + other

inline def -(other: Physic[T]): Physic[T] = phys - other

inline def *[U <: PhysicQuantity](other: Physic[U]): Physic[T *** U] =

phys * other

inline def /[U <: PhysicQuantity](

other: Physic[U]

): Physic[T *** InverseOfPhysicQuantity[U]] = phys / other

inline def value: Double = phys

}

You can see from this that we will only allow to sum/substract quantities if they have the same `Physic[T]`

type (aka, the same units). We allow any kind of products/divisions, but in that case we return a type that we will need to compute.

**First implemenation**

The idea behind the implementation is to make a type `PhysicQuantity`

that can either be a lone `Scalar`

(no unit) or be composed of a bunch of “primitives” from the International System of Units (SI) (meters, seconds, kilos…) and their inverse.

These primitives can be encoded in a trait `SIOrInverse`

`sealed trait SIOrInverse`

sealed trait SI extends SIOrInverse

sealed trait Second extends SI

sealed trait Meter extends SI

sealed trait Kilo extends SI

sealed trait Kelvin extends SI

sealed trait Ampere extends SI

sealed trait Inverse[T <: SI] extends SIOrInverse

And now, we can encode the full `PhysicQuantity`

as some kind of “list of types” using the `**:`

“operator”/type:

`sealed trait PhysicQuantity`

sealed trait Scalar

extends PhysicQuantity

sealed trait **:[Head <: SIOrInverse, Tail <: PhysicQuantity]

extends PhysicQuantity

With that, we can for example represent a speed as the following

`type Speed = Meter **: Inverse[Second] **: Scalar`

This has to be thought of as “the type `Speed`

is a product of the type `Meter`

with the inverse of the type `Second`

” (and a `Scalar`

, which has no unit and does nothing).

Note also that we never give any concrete implementation for these types! They will always stay purely in the type system, and the computations that we do afterwards are purely at the type level. They will never be done at run-time!

Multiplying two `PhysicQuantity`

would then be the concatenation:

`type Concat[A <: PhysicQuantity, B <: PhysicQuantity] <: PhysicQuantity =`

A match {

case Scalar => B

case head **: tail => head **: Concat[tail, B]

}

type ***[Left <: PhysicQuantity, Right <: PhysicQuantity] =

Concat[Left, Right]

And for dividing two `PhysicQuantity`

, we need to take the inverse of a `SIOrInverse`

, and then take the inverse of a full `PhysicQuantity`

`type InverseOf[T <: SIOrInverse] <: SIOrInverse = T match {`

case Inverse[t] => t

case T => Inverse[T]

}

type InverseOfPhysicQuantity[T <: PhysicQuantity] <: PhysicQuantity =

T match {

case Scalar => Scalar

case h **: tail => InverseOf[h] **: InverseOfPhysicQuantity[tail]

}

(The inverse of a `Scalar`

is again a `Scalar`

, since neither have physical units!)

At this point, we have all the missing parts from our `Physic[T]`

opaque type from earlier. But are we done, though? Let’s try a simple computation:

`import Physic.*`

val distance = 6.meters

val speed = 2.meters / 1.seconds

// here we type explicitly to verify our computation

val time: Physic[Second **: Scalar] = distance / speed

Outch! This does indeed **not** compile, because the type on the right hand side of `time`

is actually `Physic[Meter **: Inverse[Meter] **: Second **: Scalar]`

, which is different from what we want! As human, we know that `Meter`

and `Inverse[Meter]`

should cancel out, but we have never told that to the compiler.

Another problem is that we don’t have commutativity.

`val distance = 6.meters`

val time = 2.seconds

distance * time // type is Physic[Meter **: Second **: Scalar]

time * distance // type is Physic[Second **: Meter **: Scalar]

So we need to instruct the compiler how to take care of that as well.

# Product type reduction

There are actually two ways to solve this problem. Both are (in my opinion) entirely valid, as both will achieve our design goals. A first way of doing things would be to not make `PhysicQuantity`

a “list” of types, but rather a “map” of the SI primitive to its power (positive, negative or zero) in the product of units. The second way is to keep the list of types, but apply some product reduction until it goes to a “minimum” representation (that must be unique). We are going to go with this second option, as the first one would throw away everything we did already. But you can try the other one as an exercise.

Let’s begin by cancelling out inverses. To do that, we go through our list of SI types and for each one, we look at the remaining ones to see if we can cancel an inverse or not:

`type ProductReduction[P <: PhysicQuantity] <: PhysicQuantity = P match {`

case Scalar => Scalar

case h **: tail =>

Contains[InverseOf[h], tail] match {

case true => ProductReduction[RemoveFirst[InverseOf[h], tail]]

case false => h **: ProductReduction[tail]

}

}

type RemoveFirst[

T <: SIOrInverse,

Tup <: PhysicQuantity

] <: PhysicQuantity =

Tup match {

case Scalar => Scalar

case T **: tail => tail

case head **: tail => head **: RemoveFirst[T, tail]

}

type Contains[T <: SIOrInverse, Tup <: PhysicQuantity] <: Boolean =

Tup match {

case Scalar => false

case T **: _ => true

case _ **: tail => Contains[T, tail]

}

With that, we already solve the first problem that we had. Moreover, after applying this product reduction, we know that we can’t further remove any elements of our list. So it’s minimal in that sense, but it’s not enough. Types could still be in whatever order.

We can solve this is by sorting the types, in a way that we put them always in the same order (for example, we start with `Meter`

, then `Second`

, then `Kilo`

, … And at the end, we put the inverses — in the same order). We define a “weight” for each SI primitive

`type SIOrdering[T <: SIOrInverse] <: Int = T match {`

case Meter => 0

case Second => 1

case Kilo => 2

case Kelvin => 3

case Ampere => 4

// putting inverses at the end

case Inverse[x] => 1000 + SIOrdering[x]

}

These weights are completely arbitrary. The only constraint is to not give the same weight to two different primitives. And then we can sort them using that ordering:

`type SortBy[`

P <: PhysicQuantity,

F <: [_ <: SIOrInverse] =>> Int

] <: PhysicQuantity =

P match {

case Scalar => Scalar

case h **: tail =>

Concat[

SortBy[Filter[tail, [t] =>> (F[t] < F[h])], F],

h **: SortBy[Filter[tail, [t] =>> (F[t] >= F[h])], F]

]

}

type Filter[

P <: PhysicQuantity,

Predicate <: ([_ <: SIOrInverse] =>> Boolean)

] <: PhysicQuantity =

P match {

case Scalar => Scalar

case h **: tail =>

Predicate[h] match {

case true => h **: Filter[tail, Predicate]

case false => Filter[tail, Predicate]

}

}

This is an implementation of the QuickSort algorithm, but at the level of the types! The `F`

can be seen as a “type level function” taking an SI primitive, and returning a number. The good thing is that we have the `F`

already, it’s the `SIOrdering`

weights defined above. So we now have

`type SIOrderingFn = [T <: SIOrInverse] =>> SIOrdering[T]`

type SortBySIOrdering[P <: PhysicQuantity] = SortBy[P, SIOrderingFn]

Putting everything together, we can finally have our correct definition for the `***`

type:

`type ***[Left <: PhysicQuantity, Right <: PhysicQuantity] =`

SortBySIOrdering[ProductReduction[Concat[Left, Right]]]

We first concatenate the `Left`

and `Right`

operands, then we reduce all the inverses, and finally we sort the whole thing. This definition will now properly compile if and only if our computations are correct.

# A small example: computing the Earth-Moon attraction

If you remember Newton’s law of universal gravitation, you know that the force between two bodies of masses m1 and m2, separated by a distance r, is given by G·m1·m2/r², where G is universal gravity constant, roughly given by (6.6743 ± 0.00015) × 10−11 m3 kg−1 s−2. (If you didn’t remember it, then this reminder is probably the best thing to retain from this blog post.)

Now we can look up the masses of the Earth and the Moon, and the distance between them, and we can do

`import physicstypes.Physic.*`

val G = 6.67430e-11 * 1.meters * 1.meters * 1.meters /

1.kilos / 1.seconds / 1.seconds

val earthMass = 5.972e24.kilos

val moonMass = 7.348e22.kilos

val distance = 384400e3.meters

val force: Physic[Meter **: Kilo **: Inverse[Second] **: Inverse[Second] **: Scalar] =

G * earthMass * moonMass / (distance * distance)

Works like a charm! You can try to, for example, “forget” the parenthesis in the denominator, and you see that it will fail to compile.

I am sure you will note that it can be cumbersome to make this triple `1.meters`

product. We could simplify that by implementing a `power`

function. I will leave that as an exercise, although this is actually implemented in the repo, if you’d like to take a peak.

# Testing

Testing that the implementation works properly is surprisingly harder than it looks! Testing the “happy paths” are essentially trivial. You can write tests to verify that we support commutativity, that we divide in the proper way, and so on so forth… But how do you test that the code does indeed not compile when it’s wrong? The problem is that if it does not compile, then neither do your tests, and so you can’t run them!

Fortunately, Scala provides a function `scala.compiletime.testing.typeCheckErrors`

which returns, at run-time, a list of compile errors that would occur if the argument string was injected in the codebase at that place.

Here is a test example from the codebase

`test("Can't sum meters and seconds") {`

val compileErrors = typeCheckErrors(

"""

val sum = Physic.meters(1.0) + Physic.seconds(2.0)

"""

)

assertOneCompileErrorContains(

compileErrors,

"Required: physicstypes.Physic[physicstypes.Meter **: physicstypes.Scalar]"

)

}

def checkOneCompileErrorContains(errors: Iterable[Error], substring: String) = {

errors.exists(_.message.contains(substring))

}

def assertOneCompileErrorContains(errors: Iterable[Error], substring: String) = {

assert(

checkOneCompileErrorContains(errors, substring),

s"Expected a compile error with message containing '$substring', but got: $errors"

)

}

# Closing words

I hope this was fun! And perhaps even … useful? Inserting a lot of business knowledge directly in the type system, rather than “only” in unit tests or run-time conditions can be very powerful. We can think, for example, of the use case where only a user with Admin rights can access some parts of the codebase. You could directly inject these restrictions within the type system, and your code would not even compile if you have a security breach. At this point, this is only theoretical, but I hope that the above would convince you that it’s possible!

If you liked what you read, the first “episode” of my **Fun with Types** series talks about making a type-level map.