# Mechanics of unboxed union types in Scala

This post is inspired by Miles Sabin’s “Unboxed union types in Scala via the Curry-Howard isomorphism”.

And then use it as follows?

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 type-safe encoding of union types”.

Miles’s final result is our starting point.

It employs the Curry-Howard 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.

Unfold by knowing that `type ¬¬[A] = ¬[¬[A]]`

.

Unfold by knowing that `type ∨[T, U] = ¬[¬[T] with ¬[U]]`

.

Eliminate the outer `¬`

on both sides of `<:<`

. Note that we must swap operands since `¬`

is contravariant.

More on contravariance later on.

This gives us the simplified code below.

Let’s continue simplifying things.

Expand the context bound into an implicit evidence parameter.

Unfold `|∨|`

knowing that `type |∨|[T, U] = {type λ[X] = ¬[T] with ¬[U] <:< ¬[X]}`

.

Put together it gives us the code below.

# Simplify more

We’ll now take a closer look at the type in the implicit parameter.

Let’s give the `<:<`

operator a more descriptive name `isSubtypeOf`

.

which is the same as saying

Wait. What was the `¬`

type again?

Let’s make it simpler. Recall that `=>`

is just an alternative syntax for `Function1`

.

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.

# 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).

Let’s use that knowledge and replace `¬`

with `Contra`

in our equation.

So what are the supertypes of `Contra[Int] with Contra[String]`

?

The answer is both `Contra[Int]`

and `Contra[String]`

(Fig. 2).

We’re nearly there. We know

and

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.

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`

.

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`

and`String`

with classes that we can actually inherit from.

Check if you can pass instances of those subclasses to the`size()`

method. - What will happen if we replace
`Contra[-A]`

with`Inva[A]`

? What about`Covar[+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