Scala 3: Dependent Types, Part I
Scala 3 expands on the type-level computing you can do at compile time. This post starts a discussion of dependent types.
Happy New Year! I hope 2021 is better than 2020 for all of us.
For an even more concise summary of most of the notable changes in Scala 3, see my new Scala 3 Highlights page.
You can start reading the rough draft of Programming Scala, Third Edition on the O’Reilly Learning Platform. The first half or so of the chapters are available. I am refining them still, but any feedback is welcome!
Dependent types are types that depend on values. For example, the following declarations are legal in Scala 3:
The type 1 is a subtype of Int (i.e., 1 <: Int) and "" is a subtype of String. Here’s how we can demonstrate those relationships:
We can assign one to an object of type Int, because 1 <: Int, and similarly for emptyString, since "” <: String.
The last three examples with summon might be unfamiliar. Recall from my Contextual Abstractions: Part II post that summon is the new alternative to implicitly. It finds a given instance (implicit value in Scala 2 terminology) in scope for the enclosed type, if one exists. In this case, I’m using the <:< type, which can be used with the infix notation shown. (It’s also available in Scala 2 and see the similar =:= type.) For example, 1 <:< Int is equivalent to <:<[1, Int].
The compiler attempts to instantiate a given instance of this type. Note what the compiler prints for res0 and res1. An instance was successfully created and its toString method just prints generalized constraint. Whereas when I attempt to construct 1 <:< 2, the error message, Cannot prove that (1 : Int) <:< (2 : Int) actually comes from the implicit not found message. Here is the signature of <:<:
<:< typeNote that you can use the annotation @implicitNotFound to define custom error messages when a type is intended for implicit resolution and an instance can’t be found. Also, you can reference the type parameters in the error string. Handy!
This type is also declared sealed abstract, which effectively means that only the compiler can synthesize instances of the type.
Finally, this type also has some interesting methods for composition, etc. Try playing with them in the Scala REPL.
Because 1, "”, etc. can only have one instance, they are singleton types. There is another function called valueOf for retrieving the one value for the type, if one exists:
It has some limits. As expected, it finds the instances for the “types” 1 and 2.2, but there is definitely more than one value for Int.
Note how we have to refer to the type of a declared object, like Nil. We have to use .type. This is generally true when you need the type for an object.
The one instance of Unit is (). (Yes, that’s the name. Think of Unit as a zero-element tuple!) The REPL doesn’t print anything for valueOf[Unit], but the next two lines show that a value is returned and calling toString on it confirms our expectations.
Attempting to get an instance for Nothing returns an error, because it has no instances. In the language of type theory, Nothing is uninhabited.
The last example shows an implementation limitation. There is only one instance for the tuple given, but it can’t resolve it. I don’t know why.
You’ll notice another method is mentioned, summonFrom, which is similar to summon. I won’t discuss the details, but see this Dotty page for examples of how it’s used. There’s also a similar summonAll method.
We can do various forms of algebra and comparisons on types. In the following examples, restart the Scala 3 REPL for each block of code, because sometimes the imports shown have colliding definitions.
First, let’s import the ability to compare any types:
The import ...ops.any._ enables the types like 2 == 2. We can also use valueOf to try them out, but I’ll mostly stick to doing assignments in what follows. Try using some Double examples, too.
There any many options for integer arithmetic:
Hopefully these are self-explanatory. I’ve added comments where additional clarity is useful.
What about Doubles, Longs, etc.? Floating point numbers don’t make a lot of sense here, in part because doing comparisons is tricky, due to rounding, etc. Supporting Long is also of limited value, because mostly these operations are intended for working with literal values and it’s unlikely you would use Long literals in these contexts!
There’s another useful tool, which I’ll exploit in the next post, called S[N], for “successor” of N. One way to encode all the natural (nonnegative) integers is to define a 0 and then a successor function, let’s call it … oh I don’t know, how about s? In this encoding, 3 would be s(s(s(0))). That’s what S[N] does for us at the type level. This this encoding is part of the Peano axioms:
Because we actually have “types” for 1, 2, etc., we don’t have to start with 0. In case this seems useless to you, and to give you a hint about the next post’s topic, if I add an element to a sequence of size N, then the new size should be S[N]. I know…, mind blown! (Well, hopefully it will be after you see how we can leverage this ability…)
Need to cheat on your next boolean logic quiz? Here you go:
You’re welcome, Interwebs!
By the way, I suggested above that you restart the REPL between each example. Note that boolean.ops._ defines a ^ type (exclusive or) and so does int.ops._. This is the collision I was concerned about.
Finally, there’s string concatenation:
What’s Next?
Okay, so dependent types are interesting and fun to play with, but how useful is all this, really? I hope to answer that question in the next post.
For an even more concise summary of most of the notable changes in Scala 3, see my new Scala 3 Highlights page.
You can start reading the rough draft of Programming Scala, Third Edition on the O’Reilly Learning Platform. The first half or so of the chapters are available. I am refining them still, but any feedback is welcome!
