Unpacked union types in Scala based on Curry-Howard isomorphism

Note by the translator. A future version of Scala (“Don Giovanni”) has announced support for union types. Miles Sabin, widely known in narrow circles as the creator of Shapeless, demonstrates in this 2011 article how to create join types now.
UPD . The approach presented in the article does not allow one to obtain real types of unification and, in addition, can significantly affect compilation time. The types of intersection ( A with B) used in the article also differ from the classical ones because they do not possess the commutativity property. Details on the Dotty pilot project, within the framework of which these and other problems will be solved, can be found in a wonderful presentation by Dmitry Petrashko darkdimius is the developer of the Scala compiler in EPFL.

Scala has a very expressive type system. However, it does not include (at least as primitives) all the coveted elements. There are several truly useful types that fall into this category - these are the types of polymorphic functions of higher rank (higher-rank) and recursive structural types. But I’ll tell you more about them in the next posts, and today I’m going to show you how in Scala we can create union types. In the course of the explanation, I will shed some light on the Curry-Howard isomorphism and show how to use it for our purposes.



So, for starters, what is a union type? The type of union is in many ways what you expect from it: the union of two (or more, but I will limit myself to only two) types. Values ​​of this type include all the values ​​of each of the combined types. What this means will help us figure out an example, but first we introduce a notation system. For reasons that will soon become clear, I will write the union types Tand Uusing the operation symbols or: T ∨ U. Thus association types Intand Stringwritten as Int ∨ String. The values ​​of this union type include all type values Intand all type values String.

But what does this mean more specifically? And this means that if we were able to directly express such a type in Scala, then we could, for example, write this:

def size(x: Int ∨ String) = x match {
  case i: Int => i
  case s: String => s.length
}
size(23) == 23   // OK
size("foo") == 3 // OK
size(1.0)        // Не OK, ошибка компиляции

In other words, a method sizecan accept arguments of either type Intor type String(including their subtypes Nulland Nothing), and no others.

It is important to emphasize the difference between using this type of association and standard Either. Either, known as the sum type, is an analog of the union type in languages ​​that do not support subtypes. Rewriting our example using Eitherwill give us:

def size(x: Either[Int, String]) = x match {
  case Left(i) => i
  case Right(s) => s.length
}
size(Left(23)) == 23    // OK
size(Right("foo")) == 3 // OK

A type Either[Int, String]can model the type of union Int ∨ String, since there is a correspondence (isomorphism) between them and their values. However, it is absolutely clear that a type Eitherachieves this by being an additional layer of a boxed representation, and not as an unpacked primitive of a type system. Can we create something better than Either? Can we find a way to represent union types in Scala without involving packaging and with all the expected static guarantees?

It turns out that we can, but on the way to the result we need to make a detour through the first-order logic using the Curry-Howard isomorphism. This isomorphism tells us that relations between types in a type system can be considered as an image of relations between statements in a logical system (and vice versa). We can interpret this statement in various ways, depending on which type system we are talking about and which logical system we have chosen, but for our discussion I will ignore most of the details and focus on simple examples.

We illustrate the Curry-Howard isomorphism in the context of a type system with subtypes as in Scala. You may notice that there is a correspondence between the types of intersection ( A with B) and the logical conjunction ( A ∧ B); between my hypothetical types of unification ( A ∨ B) and logical disjunction (just as A ∨ Bhinted at above); and between subtypes (A <: B) and logical implication ( A ⇒ B). In the left column of the table below we have the subtype relations executed in Scala (but in the case of union types not directly expressed in the language), and in the right column we have logical formulas obtained from the relations between types on the left by simply replacing withwith ∧and <:by ⇒. In each case, such a replacement gives a logically correct formula.

(A with B) <: A	(A ∧ B) ⇒ A
(A with B) <: B	(A ∧ B) ⇒ B
A <: (A ∨ B)	A ⇒ (A ∨ B)
B <: (A ∨ B)	B ⇒ (A ∨ B)

The essence of the Curry-Howard isomorphism is that the mechanical replacement process always remains correct - the correct type formula always rewrites into the correct logical formula, and vice versa. And this is done not only for conjunction, disjunction and implication. We can also generalize correspondence to logical formulas including negation (a key operation in today's consideration) and quantifiers of generality and existence.

What will the addition of negation mean to us? A conjunction of two types (i.e. A with B) has values ​​that are instances of both, and A, at the same time B. Similarly, we can assume that type negation A(I will write it as ¬[A]) should have values ​​that are not instances of typeA. Denial also cannot be directly expressed in the Scala language, but where do we go by assuming this is not so?

In that case, we could use the Curry-Howard isomorphism and De Morgan's laws to get the definition of union types from the types of intersection and negation. Here's how it could have happened ...

To begin with, recall the De Morgan equality:

(A ∨ B) ⇔ ¬(¬A ∧ ¬B)

Then we apply the Curry-Howard isomorphism (using the =:=Scala language equivalence operation ):

(A ∨ B) =:= ¬[¬[A] with ¬[B]]

If we could only find a way to write this into Scala, then our goal would be achieved and we would have our types of unification. So can we express type negation in Scala?

Unfortunately, we can’t. But what we can do is convert all our types in such a way as to make it possible to write negation in a transformed context. Then we need to find a way to make it all work in the original unreformed context.

Some readers may have been a little surprised when I previously illustrated the Curry-Howard isomorphism using intersection types paired with conjunction, union types paired with disjunction, and subtype ratios paired with implication. Typically, product types, i.e. (A, B)model conjunction, sum types (Either[A, B]) model disjunction and function types model implication. If we rewrite our previous table using products, sums and functions, we get the following:

(A, B) => A	(A ∧ B) ⇒ A
(A, B) => B	(A ∧ B) ⇒ B
A => Either [A, B]	A ⇒ (A ∨ B)
B => Either [A, B]	B ⇒ (A ∨ B)

On the left side, we no longer expect correctness in terms of the relationship of subtypes, instead we need to observe the principle of parametricity , which allows us to determine whether a function type can be implemented based only on the signature of the function. Obviously, all function signatures in the left column can be implemented. For the first two cases, we have a pair (A, B)as an argument to our function, so we can easily get from this pair a value of type Aor B, using _1or _2:

val conj1: ((A, B)) => A = p => p._1
val conj2: ((A, B)) => B = p => p._2

In the second and third cases, the arguments of the function are values ​​of the type Aand, Baccordingly, therefore, we can get the result of the type Either[A, B]using the constructors Left[A]and Right[B]:

val disj1: A => Either[A, B] = a => Left(a)
val disj2: B => Either[A, B] = b => Right(b)

It is in this form that the Curry-Howard isomorphism is usually expressed for languages ​​without subtypes. However, union types, as well as intersection types, are inherently based on subtypes. Therefore, the considered mapping will in no way help us with the unification. But it can help us with the negation, which is the missing piece of the puzzle.

With or without subtypes, the smallest type (bottom type) represented in Scala as Nothingmaps to a logical false. For example, all of the following equalities are true:

A => Either [A, Nothing]	A ⇒ (A ∨ false)
B => Either [Nothing, B]	B ⇒ (false ∨ B)

This follows from the fact that all function signatures on the left are realizable, and the logical formulas on the right are true (a post by James Airy explains why I do not show the case of matching products / conjunctions). Now let's think about what corresponds to a function with the following signature:

A => Nothing

On the right logical side of the Curry-Howard isomorphism, this signature maps to a formula A ⇒ falsethat is equivalent ¬A. It seems quite intuitively reasonable - there are no type values Nothing, therefore, a signature A => Nothingcannot be implemented (except by throwing an exception, but in our case this is not allowed).

Now let's see what happens if we use this signature as our representation of type negation,

type ¬[A] = A => Nothing

and apply it in the context of De Morgan's laws to get the type of association:

type ∨[T, U] = ¬[¬[T] with ¬[U]]

Now we can check our type using Scala REPL:

scala> type ¬[A] = A => Nothing
defined type alias $u00AC
scala> type ∨[T, U] = ¬[¬[T] with ¬[U]]
defined type alias $u2228
scala> implicitly[Int <:< (Int ∨ String)]
:11: error: Cannot prove that Int <:< 
  ((Int) => Nothing with (String) => Nothing) => Nothing.
       implicitly[Int <:< (Int ∨ String)]

REPL shows us that the solution has not yet been received. The expression implicitly[Int <:< (Int ∨ String)]asks the compiler if it can prove that it Intis a subtype Int ∨ String, which should be true for the type of union.

What went wrong? The problem is that we converted the types on the right side of the operator <:<to function types in order to use the type negation given as A => Nothing. This means that the type of union itself is a type of function. But this, obviously, is not consistent with being Inta subtype of the union type, which shows the error message from REPL. To eliminate the error, we must also convert the left side of the operator <:<to a type that would be a subtype of the type on the right.

What kind of transformation can this be? What about double negation?

type ¬¬[A] = ¬[¬[A]]

Let's see what the compiler says:

scala> type ¬¬[A] = ¬[¬[A]]
defined type alias $u00AC$u00AC
scala> implicitly[¬¬[Int] <:< (Int ∨ String)]
res5: <:<[((Int) => Nothing) => Nothing,
  ((Int) => Nothing with (String) => Nothing) => Nothing] =
    
scala> implicitly[¬¬[String] <:< (Int ∨ String)]
res6: <:<[((String) => Nothing) => Nothing,
  ((Int) => Nothing with (String) => Nothing) => Nothing] =
    

Bingo! And ¬¬[Int], and ¬¬[String]are subtypes Int ∨ String!

Now we need to check that we do not just return a positive answer every time:

scala> implicitly[¬¬[Double] <:< (Int ∨ String)]
:12: error: Cannot prove that
  ((Double) => Nothing) => Nothing <:<
    ((Int) => Nothing with (String) => Nothing) => Nothing.

So, we are almost done, it remains to put the finishing touches. The relationships of the subtypes that we have are isomorphic to the ones we want to get (because the type ¬¬[T]is isomorphic T). But we still have no way to express the same relationships with unreformed types, which we just need.

We can solve this problem apart ¬[T], ¬¬[T]and T ∨ Uphantom types and using them only to submit the required subtype rather than working directly with the values of data types. Here's how this happens in our test case:

def size[T](t: T)(implicit ev: (¬¬[T] <:< (Int ∨ String))) =
  t match {
    case i: Int => i
    case s: String => s.length
  }

It uses a generalized type constraint, which requires the compiler to prove that anyone Tdeduced as a type argument to a method sizesatisfies that its double negation is a subtype Int ∨ String. As the next REPL session shows, this condition is only satisfied if Tit is Intor String:

scala> def size[T](t: T)(implicit ev: (¬¬[T] <:< (Int ∨ String))) =
     |   t match {
     |     case i: Int => i
     |     case s: String => s.length
     |   }
size: [T](t: T)(implicit ev: <:<[((T) => Nothing) => Nothing,
  ((Int) => Nothing with (String) => Nothing) => Nothing])Int
scala> size(23)
res8: Int = 23
scala> size("foo")
res9: Int = 3
scala> size(1.0)
:13: error: Cannot prove that
  ((Double) => Nothing) => Nothing <:<
    ((Int) => Nothing with (String) => Nothing) => Nothing.

And now the last trick. From the point of view of syntax, the implicit parameter of the proof looks ugly and heavy, however, we can fix this by converting it into a contextual restriction of a parameter of the type T:

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
  }

Done! We got an unpacked, statically type-safe representation of union types in Scala, without modifying the language itself!

Naturally, it would be better if Scala supported union types as primitives. But at least the solution we got demonstrates that the Scala compiler has all the necessary information to do this. Now it remains only to pester Martin and Adriaan so that they make the types of unification available directly.