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 SIOrInverseAnd 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 PhysicQuantityWith that, we can for example represent a speed as the following
type Speed = Meter **: Inverse[Second] **: ScalarThis 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 / speedOutch! 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.
