Unpacked types of unions in Scala based on the Curry-Howard isomorphism

Translator's note. The future version of Scala (“Don Giovanni”) 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 union types now.
UPD . The approach presented in the article does not allow to get real types of union and, moreover, can significantly affect the compilation time. The types of intersection ( A with B ) used in the article are also different from the classical ones because they do not have the commutative property. Details about the Dotty pilot project, within the framework of which these and other problems will be solved, can be found in Dmitry Petrashko’s wonderful presentation by darkdimius , 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 desired elements. There are several truly useful types that fall under this category - these are types of higher rank polymorphic functions and recursive structural types. But I’ll talk about them in more detail 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 a little light on the Curry-Howard isomorphism and show how to use it for our purposes.



So, to begin with, what is a type of union? The type of association is in many ways what you expect from it: the union of two (or more, but I will confine myself to only two) types. Values ​​of this type include all values ​​of each of the types being combined. What this means will help us to clarify an example, but first we introduce a notation system. For reasons that will soon become clear, I will write the union of types T and U using the OR operation symbol: T ∨ U Thus, the union of the Int and String types is written as Int ∨ String . Values ​​of this type of union include all values ​​of type Int and all values ​​of type String .
')
But what does this mean more specifically? 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, the size method can take arguments of type Int , or type String (including their subtypes Null and 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 analogue of the union type in languages ​​that do not support subtypes. Rewriting our example using Either will 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 

The Either[Int, String] type can model the type of the combination Int ∨ String , since there is a correspondence (isomorphism) between them and their values. However, it is absolutely clear that the Either type achieves this as an additional level of boxed representation, and not as an unboxed type system primitive. Can we create something better than Either ? Can we find a way to represent the types of unification in Scala without 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 first-order logic using the Curry-Howard isomorphism . This isomorphism tells us that relationships between types in a type system can be viewed as an image of the relationship between statements in a logical system (and vice versa). We can interpret this statement in different 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 can see that there is a correspondence between the types of intersection ( A with B ) and logical conjunction ( A ∧ B ); between my hypothetical types of union ( A ∨ B ) and logical disjunction (also A ∨ B , which was hinted at above); and between subtypes ( A <: B ) and logical implication ( A ⇒ B ). In the left column of the table below, we have subtype relationships performed in Scala (but in the case of union types, not expressed directly in the language), and in the right column we have logical formulas derived from relations between types on the left by simply replacing with ∧ and <: ⇒ . 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 maintains its correctness — the correct type formula is always rewritten 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 (the key operation in today's discussion) and quantifiers of generality and existence.

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

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

To begin with, let us recall the De Morgan equality:

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

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

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

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

Unfortunately, we can not. But what we can do is convert all our types in such a way as to make possible the recording of the negation in the transformed context. Then we need to find a way to make it all work in its original, non-transformed 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 ratio paired with implication. Usually, product types (product types), i.e. (A, B) model a conjunction, sum types ( Either[A, B] ) model a disjunction, and function types model an 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)

In the left part, we no longer expect correctness in terms of the relationship of subtypes; instead, we need to follow the principle of parametricity , which allows us to determine whether the type of function 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 of our function, so we can easily get a value of type A or B from this pair using _1 or _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 type A and B respectively, so we can get the result of type Either[A, B] using the Left[A] and Right[B] constructors:

 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, join types, as well as intersection types, are inherently based on subtypes. Therefore, the mapping considered does not help us in any way with the union. But it can help us with the negation, which is the same missing piece of the puzzle.

With or without subtypes, the lowest type (bottom type), represented in Scala as Nothing , is mapped to a logical false. For example, all of the following equations are true:

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

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

 A => Nothing 

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

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

 type ¬[A] = A => Nothing 

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

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

Now we can check our type using the 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)] <console>:11: error: Cannot prove that Int <:< ((Int) => Nothing with (String) => Nothing) => Nothing. implicitly[Int <:< (Int ∨ String)] 

The REPL shows us that the decision has not yet been fully received. The implicitly[Int <:< (Int ∨ String)] expression implicitly[Int <:< (Int ∨ String)] asks the compiler if it can prove that Int is a subtype of 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 <:< into function types to use the type negation given as A => Nothing . This means that the type of union itself is a type of function. But this is obviously not consistent with the fact that Int a subtype of a union type, which is shown by the error message from the REPL. To eliminate the error, we must also convert the left part of the operator <:< to a type that would be a subtype of the type on the right side.

What could be this transformation? How about double denial?

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

Let's see what the compiler will say to this:

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

Bingo! Both ¬¬[Int] and ¬¬[String] are subtypes of Int ∨ String !

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

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

So, we are almost finished, it remains to put the final touches. The relationship of the subtypes that we have is isomorphic to what we want to get (since the type ¬¬[T] is isomorphic to T ). But so far we have no way to express the same relations with non-transformed types, which is exactly what we need.

We can solve this problem by counting ¬[T] , ¬¬[T] and T ∨ U phantom types and using them only to represent the required subtype relationships, rather than working directly with the values ​​of these types. Here’s how it 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 generic type constraint that requires the compiler to prove that any T outputted as a type argument to the size method satisfies that its double negation is a subtype of Int ∨ String . As the next REPL session shows, this condition is fulfilled only if T is an Int or 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) <console>: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 the syntax, the implicit parameter of the proof looks ugly and heavy, but we can fix it by transforming it into a context constraint of a parameter of 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 Scala union types, 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. It now remains to pester Martin and Adriaan to make the types of unions accessible directly.