11 January 2018 / Pawel Batko
Mechanics of unboxed union types in Scala
Mechanics of unboxed union types in Scala
Paweł Batko, VirtusLab
This post is inspired by Miles Sabin’s “Unboxed union types in Scala via the CurryHoward isomorphism”.
Wouldn’t it be nice to be able to write a type like this:
1 2 
type StringOrInt = String  Int 
And then use it as follows?
1 2 3 4 5 6 7 8 
def foo(x: String  Int) = { x match { case s: String => println("I'm a String") case i: Int => println("I'm an Int") case _ => println("I cannot be anything else 'cuz compiler guarantees it!") } } 
I’ll try to show you how you can define such a type and, more importantly, try to explain how it works.
It’s not as pretty as in the example above, but it turns out it’s not so hard either!
Sum types
A sum type (also called a union type) is a type whose values can be those of any type comprising the sum.
Bear with me.
One way of expressing it in Scala is by using Either[A, B]
which can be interpreted as a sum of types A
and B
.
Another representation is Miles’ intricate formula, which gives us “unboxed, statically typesafe encoding of union types”.
Miles’s final result is our starting point.
1 2 3 4 5 6 7 8 9 10 11 12 
type ¬[A] = A => Nothing type ¬¬[A] = ¬[¬[A]] type ∨[T, U] = ¬[¬[T] with ¬[U]] type ∨[T, U] = {type λ[X] = ¬¬[X] <:< (T ∨ U)} def size[T: (Int ∨ String)#λ](t: T) = t match { case i: Int => i case s: String => s.length } 
It employs the CurryHoward isomorphism and DeMorgan’s laws. Fancy!
But how does it work? Let’s try to understand the core Scala mechanisms that are at play here.
Simplify
We’ll start with a couple of substitutions and one elimination to simplify things a bit.
1 2 
type ∨[T, U] = {type λ[X] = ¬¬[X] <:< (T ∨ U)} 
Unfold by knowing that type ¬¬[A] = ¬[¬[A]]
.
1 2 
type ∨[T, U] = {type λ[X] = ¬[¬[X]] <:< (T ∨ U)} 
Unfold by knowing that type ∨[T, U] = ¬[¬[T] with ¬[U]]
.
1 2 
type ∨[T, U] = {type λ[X] = ¬[¬[X]] <:< ¬[¬[T] with ¬[U]]} 
Eliminate the outer ¬
on both sides of <:<
. Note that we must swap operands since ¬
is contravariant.
More on contravariance later on.
1 2 
type ∨[T, U] = {type λ[X] = ¬[T] with ¬[U] <:< ¬[X]} 
This gives us the simplified code below.
1 2 3 4 5 6 7 8 9 10 
type ¬[A] = A => Nothing type ∨[T, U] = {type λ[X] = ¬[T] with ¬[U] <:< ¬[X]} def size[T: (Int ∨ String)#λ](t: T) = t match { case i: Int => i case s: String => s.length } 
Let’s continue simplifying things.
1 2 
def size[T: (Int ∨ String)#λ](t: T) = 
Expand the context bound into an implicit evidence parameter.
1 2 
def size[T](t: T)(implicit ev: (Int ∨ String)#λ[T]) = 
Unfold ∨
knowing that type ∨[T, U] = {type λ[X] = ¬[T] with ¬[U] <:< ¬[X]}
.
1 2 
def size[T](t: T)(implicit ev: ¬[Int] with ¬[String] <:< ¬[T]) = 
Put together it gives us the code below.
1 2 3 4 5 6 7 8 
type ¬[A] = A => Nothing def size[T](t: T)(implicit ev: ¬[Int] with ¬[String] <:< ¬[T]) = t match { case i: Int => i case s: String => s.length } 
Simplify more
We’ll now take a closer look at the type in the implicit parameter.
1 2 
¬[Int] with ¬[String] <:< ¬[T] 
Let’s give the <:<
operator a more descriptive name isSubtypeOf
.
1 2 
¬[Int] with ¬[String] isSubtypeOf ¬[T] 
which is the same as saying
1 2 
¬[T] isSupertypeOf ¬[Int] with ¬[String] 
Wait. What was the ¬
type again?
1 2 
type ¬[A] = A => Nothing 
Let’s make it simpler. Recall that =>
is just an alternative syntax for Function1
.
1 2 
type ¬[A] = Function1[A, Nothing] 
Notice that Nothing
doesn’t do anything here.
It’s A
that’s important here.
Notice also that A
is a contravariant type parameter since Function1
is defined as class Function1[P, +R]
.
Let’s replace function type with a new type which we’ll call Contra
since its sole purpose is to be contravariant.
1 2 3 
trait Contra[A] type ¬[A] = Contra[A] 
Contravariance
Let’s now take a break for a quick contravariance recap.
When we talk about contravariance, or variance in general, we concern ourselves with both subtyping and parametric polymorphism (generic types).
Variance relates the subtyping relation of a component type to the subtyping relation of a more complex type (a generic type which is parameterized with the component types).
In the case of contravariance, respective subtyping relations go in the opposite (contra) directions.
Notice the inversion in the position of A
and B
(Fig. 1).
1 2 3 4 5 6 7 8 9 10 11 12 
A Contra[B] ^ ^     isSubtypeOf isSubtypeOf     + + B Contra[A] Figure 1. Contravariance. 
Let’s use that knowledge and replace ¬
with Contra
in our equation.
1 2 
Contra[T] isSupertypeOf Contra[Int] with Contra[String] 
So what are the supertypes of Contra[Int] with Contra[String]
?
The answer is both Contra[Int]
and Contra[String]
(Fig. 2).
1 2 3 4 5 6 7 8 9 10 11 12 13 14 
Contra[Int] Contra[String] ^ ^       isSubtypeOf isSubtypeOf   +++  + Contra[Int] with Contra[String] Figure 2. Supertypes of Contra[Int] with Contra[String] 
We’re nearly there. We know
1 2 3 
Contra[String] isSupertypeOf Contra[Int] with Contra[String] Contra[Int] isSupertypeOf Contra[Int] with Contra[String] 
and
1 2 
Contra[T] isSupertypeOf Contra[Int] with Contra[String] 
What does this tell us about type parameter T
? Clearly it can be either String
or Int
.
Can it also be a subtype of either String
or Int
(imagine we can subclass from either)?
Yes, because Contra
is contravariant!
We’ve just observed that T
, as expected, behaves like a sum type.
Final result
Let’s see how that plays out in our code example.
1 2 3 4 5 6 7 8 
trait Contra[A] def size[T](t: T)(implicit ev: Contra[Int] with Contra[String] <:< Contra[T]) = t match { case i: Int => i case s: String => s.length } 
Implicit parameter ev
finds proof that Contra[T] is a supertype of Contra[Int] with Contra[String]
.
Let’s see again for which T
this holds.
Before we do that, for the sake of convenience, let’s rename Contra[Int] with Contra[String]
to Contra[X]
for some type X
.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 
Contra[asubtypeofInt] Contra[asubtypeofString] X ^ ^ ^         +++     + + + + Contra[Int] Contra[String] Int String ^ ^ ^ ^     +++         + + + Contra[Int] with Contra[String] asubtypeofInt asubtypeofString (Contra[X]) Figure 3. Contravariance and sum types. Arrows represent `isSubtypeOf` relation. 
Let’s draw the supertypes of Contra[X]
(Fig. 3, left) and the subtypes of X
(Fig. 3, right).
We see that both (and only) Int
and String
are subtypes of X
and conversely X
is the smallest supertype of Int
and String
.
Thus X
is a sum type of Int
and String
!
Conclusion
Take another look at our final code example.
I hope we have refreshed and extended our knowledge of contravariance and subtyping.
It turned out that the nearly magical type Int ∨ String
reduces to a crafty application of these two familiar concepts.
Exercises
 Does the signature below also express a sum type? Why? Why not?
def size[T](t: T)(implicit ev: Int with String <:< T)

Replace
Int
andString
with classes that we can actually inherit from.
Check if you can pass instances of those subclasses to thesize()
method. 
What will happen if we replace
Contra[A]
withInva[A]
? What aboutCovar[+A]
? 
Why does Miles Sabin use function type
A => Nothing
, while all we needed was only the simplest contravariant type? 
Count the occurrences of “contravariant” in Miles’ blog post.
Update:
 Reddit r/scala thread
 Union and intersection types in Dotty
 Union type in Scala.js. and examples
Leave a Reply