Singleton Types
A Scala 3 Experiment
A Scala 3 Experiment
I'll start this post by admitting that I’ve never gone deeply into any kind of Scala coding on the typelevel. It's not what I, as a common application (or microservice) developer, usually need.
Having stated that, of course, I might be missing out on a whole world of opportunities for better code without knowing. And because of that, I put some effort into trying to understanding the features of Scala that might sound strange, overly-theoretical, and maybe even useless, at first sight.
A concept I couldn't imagine a proper use case for was the so-called "singleton types" (also called "literal types" or even "literal singleton types"). As it happens, I recently attended a Scala Days talk about them. In this talk, singleton types are used for improving the type-safety of database queries, and inspired by this, I finally got an idea of where I could try them out for myself.
Remember matrix multiplication from math, and how the dimensions have to fit? And how all the usual libraries for matrix multiplication take matrices of any dimension, and then throw runtime exceptions when the dimensions don't fit? That's what I'll use singleton types for in the following.
Let's start with the conventional approach, leaving out the actual multiplication details for brevity:
final case class Matrix(n: Int, m: Int) {
def *(other: Matrix): Matrix = {
require(m == other.n,
s"matrix dimensions must fit ($m != ${other.n})")
Matrix(n, other.m)
}
}
In this piece of code, the runtime check ensures that the matrix dimensions are not just any integers, but also that they actually fit, so that the matrix multiplication can work at all.
This check is only necessary because we allow for all kinds of integers here in the first place. This is not the only option we have, though.
Here's a small Scala 3 REPL session (using dotr) that might surprise you:
scala> val y = 3
val y: Int = 3
scala> val y: 3 = 3
val y: Int(3) = 3
scala> val z: 4 = 3
1 |val z: 4 = 3
| ^
| found: Int(3)
| required: Int(4)
See how y and z somehow get their value ascribed as their type? This is what singleton types are about: A singleton type is a type inhabited by exactly one value. So we might as well name the type after the value. Of course, singleton types like 3 or 4 are subtypes of Int, just as singleton types like "meep" or "foo" are subtypes of String.
This is all well and good, but how to make use of these types?
The basic idea here is to restrict the type of the two matrix dimensions to be the singleton type, instead of Int. Then we can ensure at compile time that two dimensions are exactly the same number by ensuring that they have the same singleton type.
In order to restrict a type to a singleton type, Scala 3 has a type called Singleton. Combined with the new & (very similar to what Scala previously had with with, but symmetrical), we can express:
A should be an integer singleton type
By writing:
A <: Singleton & Int
Making use of this, we can define our matrix class in the following way:
type Dim = Singleton & Int
final case class Matrix[A <: Dim, B <: Dim](n: A, m: B) {
def *[C <: Dim](other: Matrix[B, C]): Matrix[A, C] =
Matrix(n, other.m)
}
And with this, we get the compile-time behavior we were aiming for:
scala> val a = Matrix(2, 4)
val a: Matrix[Int(2), Int(4)] = Matrix(2,4)
scala> val b = Matrix(4, 3)
val b: Matrix[Int(4), Int(3)] = Matrix(4,3)
scala> a * b
val res10: Matrix[Int(2), Int(3)] = Matrix(2,3)
scala> b * a
1 |b * a
| ^
| found: Matrix[Int(2), Int(4)](a)
| required: Matrix[Int(3), C]
|
| where: C is a type variable with constraint <: Dim
scala> val c = Matrix(3, 5)
val c: Matrix[Int(3), Int(5)] = Matrix(3,5)
scala> res10 * c
val res11: Matrix[Int(2), Int(5)] = Matrix(2,5)
And that's actually all there is to it. As an aside, notice how the error message from the compiler is pretty concisely telling us where we went wrong.
So here we are, having used singleton types to make a very simple matrix multiplication API a bit more typesafe, coming out of this with one more tool in our Scala 3 tool belt.
And now, it's your turn to find more use cases for singleton types!
We're hiring! Do you like working in an ever evolving organization such as Zalando? Consider joining our teams as a Software Engineer!