Unboxed union types in Scala via the Curry-Howard isomorphism

Posted by Miles Sabin on 9th Jun 2011

Update — I’ll be giving a talk on this material on the 16th of August in London. Please come along.

Scala has a highly expressive type system, but it doesn’t include everything you might find yourself hankering after — at least, not as primitives. There are a few genuinely useful things which fall under this heading — higher-rank polymorphic function types and recursive structural types are two I’ll talk about more in later posts. Today I’m going to show how we can encode union types in Scala, in the course of which I’ll have an opportunity to shed a little light on the Curry-Howard isomorphism and show how it can be put to work for us.

So, first up, what is a union type? A union type is pretty much what you’d expect: it’s the union of two (or more, but I’ll limit this discussion to just two) types. The values of that type are all of the values of each of the types that it’s the union of. An example will help to make this clear, but first a little notation — for reasons which will become apparent later I’ll write the union of types T and U as T ∨ U (ie. the two types flanking the logical ‘or’ operator), and so we write the union of the types Int and String as Int ∨ String. The values of this union type are all the Ints and all the Strings.

What does this mean more concretely? It means that if we could express this type directly in Scala we would be able to write,

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)        // Not OK, compile time error

In other words, the size method would accept arguments of either type Int or type String (and their subtypes, Null and Nothing) and nothing else.

It’s important to recognize the difference between this use of a union type and the similar use of Scala’s standard Either. Either is what’s known as a sum type, the analog of union types in languages which don’t support subtyping. Recasting our example in terms of Either we get,

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

Either[Int, String] can model the union type Int ∨ String because there is an isomorphism between the two types and their values. But equally clearly the Either type manages this by way of a layer of boxed representation, rather then by being an unboxed primitive feature of the type system. Can we do better than Either? Can we find a way of representing union types in Scala which doesn’t require boxing, and which provides all of the static guarantees we would expect?

It turns out that we can, but to get there we have take a detour through first-order logic via the Curry-Howard isomorphism. Curry-Howard tells us that the relationships between types in a type system can be viewed as an image of the relationships between propositions in a logical system (and vice versa). There are various ways that we can fill that claim out, depending on the type system we’re talking about and the logical system we’re working with, but for the purposes of this discussion I’m going to ignore most of the details and focus on simple examples.

To illustrate Curry-Howard (in the context of a type system with subtyping like Scala’s), we can see that there is a correspondence between intersection types (A with B in Scala) and logical conjunction (A ∧ B); between my hypothetical union types (A ∨ B) and logical disjunction (also A ∨ B, as hinted earlier); and between subtyping (A <: B in Scala) and logical implication (A ⇒ B). On the left hand side of each row in the table below we have a subtype relationship which is valid in Scala (although, in the case of the union types at the bottom, not directly expressible), and on the right hand side we have a logical formula which is obtained from the type relationship on the left by simply rewriting ("with" to "∧" and "<:" to "⇒") — in each case the result of the rewriting is a logically valid.

(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 Curry-Howard is that this mechanical rewriting process (whichever direction you go in) will always preserve validity — valid type formulae will always rewrite to valid logical formulae, and vice versa. This isn’t only true for conjunction, disjunction and implication. We can also generalize the correspondence to logical formulae which include negation (the key one for us here) and universal and existential quantification.

So what would it mean to add negation to the mix? The conjunction of two types (ie. A with B) has values which are instances of both A and B, so similarly we should expect the negation of a type A (I’ll write it as ¬[A]) to have as it’s values everything which isn’t an instance of A. This is also something which can’t be directly expressed in Scala, but suppose it was?

If it was, then we would be able to crank on the Curry-Howard isomorphism and De Morgan’s laws to give us a definition of union types in terms of intersection types (A with B) and type negation. Here’s how that might go …

First recall the De Morgan equivalence,

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

Now apply Curry-Howard (using Scala’s =:= type equality operator),

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

If we could work out a way of expressing this in Scala, we’d be home and dry and have our union types. So can we express type negation?

Unfortunately we can’t. But what we can do is transform all of our types in a way which allows negation to be expressed in the transformed context. We’ll then need to work out how make that work for us back in the original untransformed context.

Some readers might have been a little surprised earlier when I illustrated Curry-Howard using intersection types as the correlate of conjunction, union types as the correlate of disjunction and the subtype relation as the correlate of implication. That’s not how it’s normally done — usually product types (ie. (A, B)) model conjunction, sum types (ie. Either[A, B]) model disjunction and function types model implication. If we recast our earlier table in terms of products, sums and functions we end up with this,

(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 hand side we’re no longer looking for validity with respect to the subtype relation, instead we’re looking for evidence of the principle of parametricity, which allows us to determine if a function type is implementable just by reading it’s signature. It’s clear that all the function signatures on the left in the table above can be implemented — for the first two we have an (A, B) pair as our function argument, so we can easily evalutate to either an A or a B, using _1 or _2,

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

and for the last two we have either an A or a B as our function argument, so we can evalute to Either[A, B] (as Left[A] or Right[B] respectively).

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

This is the form in which the Curry-Howard isomorphism is typically expressed for languages without subtyping. Because this mapping doesn’t reflect subtype relations it isn’t going to be much direct use to us for expressing union types which, like intersection types, are inherently characterized in terms of subtyping. But it can help us out with negation, which is the missing piece that we need.

Either with or without subtyping, the bottom type (Scala’s Nothing type) maps to logical falsehood, so for example, the following equivalences all hold,

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

because the function signatures on the left are once again all implementable, and the logical formulae on the right are again all valid (see this post from James Iry for an explanation of why I haven’t shown the corresponding cases for products/conjunctions). Now we need to think about what a function signature like,

A => Nothing

corresponds to. On the logical side of Curry-Howard this maps to A ⇒ false, which is equivalent to ¬A. This seems fairly intuitively reasonable — there are no values of type Nothing, so the signature A => Nothing can’t be implemented (other than by throwing an exception, which isn’t allowed).

Let’s see what happens if we take this as our representation of the negation of a type,

type ¬[A] = A => Nothing

and apply it back in the subtyping context that we started with to see if we can now use De Morgan’s laws to get the union types we’re after,

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

We can test this using the Scala REPL, which will very quickly show us that we’re not quite there yet,

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 expression “implicitly[Int <:< (Int ∨ String)]” is asking the compiler if it can prove that Int is a subtype of Int ∨ String, which it would be if we had succeeded in coming up with an encoding of union types.

So what’s gone wrong? The problem is that we have transformed the types on the right hand side of the <:< operator into function types so that we can make use of the encoding of type negation as A => Nothing. This means that the union type is itself a function type. That’s clearly not consistent with Int being a subtype of it — as the error message from the REPL shows. To make this work, then, we also need to transform the left hand side of the <:< operator into a type which could possibly be a subtype of the type on the right. What could that transformation be? How about double negation?

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

Lets see what the compiler says now,

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! ¬¬[Int] and ¬¬[String] are both now subtypes of Int ∨ String!

Let's just check that this isn't succeeding vacuously,

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

We're almost there, but there's one remaining loose end to tie up — we have subtype relationships which are isomorphic to the ones we want (because ¬¬[T] is isomorphic to T), but we don't yet have a way to express those relationships with respect to the the untransformed types that we really want to work with.

We can do that by treating our ¬[T], ¬¬[T] and (T ∨ U) as phantom types, using them only to represent the subtype relationships on the underlying type rather that working directly with their values. Here's how that goes for our motivating example,

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

This is using a generalized type constraint to require the compiler to be able to prove that any T inferred as the argument type of the size method must be such that it's double negation is a subtype of (Int ∨ String). That's only ever true when T is Int or T is String, as this REPL session shows,

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.
       size(1.0)

One last little trick to finesse this slightly. The implicit evidence parameter is syntactically a bit ugly and heavyweight, and we can improve things a little by converting it to a context bound on the type parameter T like so,

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
}

And there you have it — an unboxed, statically type safe encoding of union types in unmodified Scala!

Obviously it would be nicer if Scala supported union types as primitives, but at least this construction shows that the Scala compiler has all the information it needs to be able to do that. Now we just need to pester Martin and Adriaan to make it directly accessible.

59 comments

That is so cool! Thanks for this post.

Comment by Alexandre Bertails on June 9, 2011 at 3:43 pm
Coming from Haskell I was a bit confused about how Scala was type checking your “match” statement, until I realised that it isn’t doing coverage or possibility tests for “match”. So in particular you can define this:

def size[T](t : T)(implicit ev : (\lnot\lnot[T] <: i
case d : Double => 10
}

It doesn’t complain. But when you try to find the size of a String you get an error, and the Double case of the match is inaccessible.

(Coming from Haskell I was also confused about the use of the “boxed” terminology, as in Haskell a boxed data type is one that is represented as a heap value. This Scala code clearly still represents (Foo \lor Bar) as a heap value, though it does avoid the extra layer of indirection imposed by Either.)

Comment by Max Bolingbroke on June 9, 2011 at 3:58 pm
Er, you blog has totally destroyed my code. That code sample is meant to match on the argument of size and has cases for both Int and Double.

Comment by Max Bolingbroke on June 9, 2011 at 3:59 pm
Miles,

This is pure awesomeness! Please let the promised followups come.

One little imperfection, though. The following compiles:
def size[A: (Int |∨| String)#M](a: A) = a match {
case d: Double => -1
}

Cheers,

Heiko

Comment by Heiko Seeberger on June 9, 2011 at 6:03 pm
Interesting that Racket, generally considered a typeless scheme, has Union types.

#lang typed/racket

(: size ((U Integer String) -> Integer))
(define (size x)
(cond
((exact-integer? x) x)
((string? x) (string-length x))))

;; compiles and runs just fine
(size 3)
(size “ray”)

;; fails TO COMPILE
(size 1.0)

Comment by Ray Racine on June 9, 2011 at 6:24 pm
This post is awesome, probably one of the best I’ve read. Both the result, the way and the explanation.

However, at least for the example given, isn’t using type classes better? It avoids the use of reflection to match the type in the body of the function and is also more easily extensible to more than 2 types.

Again, blown away

Comment by Ittay Dror on June 9, 2011 at 7:13 pm
Mind: blown.

Brilliant post.

Comment by Lachlan O'Dea on June 10, 2011 at 7:02 am
Awesome! I keep being impressed what can be achieved through Scala’s type system. Great post, thanks!

Comment by Michid on June 10, 2011 at 8:22 am
@heiko.seeberger

Yes, it’s a shame that the type constraint doesn’t propagate into the method body so, within the body, A is viewed as an unbounded type variable, and your case clause is accepted as possible.

OTOH, simple type constraints do seem to propagate into method bodies, eg.,
```
// Note that T is String in the body
def string[T](s : T)(implicit ev : T =:= String) = s.length
```
So maybe this is a compiler bug? Or possibly there’s some special-casing in the compiler for =:= and <:< ? Adriaan would know.
Comment by Miles Sabin on June 10, 2011 at 10:45 am
Really an awesome and especially inspiring post!

I am trying to push it just a bit forward but I found a weird issue and I am not able to figure out in what I am wrong. I defined a function like that:

scala> def asString[T : (String |∨| Int)#λ](t : T)(f : T => String): String = f(t)

asString: [T](t: T)(f: (T) => String)(implicit evidence$1: <: Nothing) => Nothing,((java.lang.String) => Nothing with (Int) => Nothing) => Nothing])String

but when I try to use it as it follows:

scala> asString(23)(_ match {
| case s : String => s
| case i : Int => “” + i
| })

the REPL complains:

:12: error: scrutinee is incompatible with pattern type;
found : String
required: Int
case s : String => s
^
Any idea on what’s wrong here?

Comment by Mario Fusco on June 10, 2011 at 10:34 am
@mario.fusco

T will have been inferred as Int in the second parameter block, so the String case is correctly rejected by the compiler as never applicable.

Comment by Miles Sabin on June 10, 2011 at 10:38 am
@batterseapower

See my reply to @heiko.seeberger for the within-body type constraint issue.

On boxing, it’s a relative thing. If you were to use Scala’s Either you would have an additional boxing layer, irrespective of the boxed-ness or otherwise of the underlying types.

And actually, this construction is perfectly compatible with Scala’s @specialization mechanism, so if you specialized the T type parameter of the size method for Int you would have a completely unboxed representation for the Int case.

Comment by Miles Sabin on June 10, 2011 at 10:53 am
Thanks for your prompt reply Miles, now I see my mistake. Do you think there is a way to use union types as parameters of an higher order function as in my example? I cannot find how.

Comment by Mario Fusco on June 10, 2011 at 11:20 am
@mario.fusco

The encoding works by transforming a union-type argument into an argument of type parameter with a constraint. So, I’m afraid it’s not going to be possible to directly represent a function value with a union-type argument, for the same reason that it’s not possible to directly represent a function value with a type parameter (ie. a polymorphic function value). I’ve got quite a lot more to say on this, so watch this space.

Comment by Miles Sabin on June 10, 2011 at 11:58 am
@Miles: About Either: Instead of making the argument of type Either, you can define that it is viewable as Either:

def size[T <% Either[Int, String]](t: T) = t match {
case i: Int => i
case s: String => s.length
}

If you supply the implicit conversions in scope, then you can avoid boxing (because all it says is T can be converted to Either. it isn’t really converted)

See http://cleverlytitled.blogspot.com/2009/03/disjoint-bounded-views-redux.html

I think that if you invent your own type, say Or[A, B], then the companion object can hold all conversions, so there’s no need for the client to import anything. Furthermore, by using the Or (or Either) type you can store the parameter for later use.

Comment by Ittay Dror on June 10, 2011 at 1:29 pm
@Ittay

Yes, that works too. The principle of using phantom types (Either in your case) to impose type constraints on a base type is a very powerful one.

Comment by Miles Sabin on June 10, 2011 at 2:58 pm
Nice work and neat post.

For comment 11, s is of type T, so it doesn’t statically have a length member. T =:= String is a subtype of T => String and because it is implicit, the compiler uses it to convert s to String in order to call length. As far as I know, the compiler knows nothing about =:= and <:<, so they are only constraints in the sense that they provide implicit conversions and arguments.

Related to =:= being implemented completely as library code, see the implementation of Predef.conforms for why I expect a bit more work is needed to actually make this solution less boxed than a solution based on Either.

Comment by Mark Harrah on June 10, 2011 at 3:35 pm
@Mark

Re: comment 11, try that in the REPL … s does have a length member within the method body, despite T being unbounded and only being =:= String. I’m guessing there must be compiler magic here.

Comment by Miles Sabin on June 10, 2011 at 5:32 pm
I’m not saying it won’t compile. It will, but that is because the compiler uses the implicit =:= instance to convert T to a String just like it would with any other implicit function parameter. Look at the generated bytecode and you can see it invokes ‘apply’ on ‘ev’.

Comment by Mark Harrah on June 10, 2011 at 6:49 pm
@Mark

Oh blimey … yes of course.

Comment by Miles Sabin on June 10, 2011 at 8:59 pm
Awesome.

About comment #15, is the viewable construct amenable to specialisation too?

Comment by HRJ on June 18, 2011 at 12:34 pm
@HRJ

Yes, a view bounded type variable will get along just fine with specialization.

Comment by Miles Sabin on June 18, 2011 at 12:47 pm
Using this union type, how would one declare a variable, i.e., something like:
var intOrString: Union(Int & String) = 4
intOrString = “four”

Comment by Richard on July 13, 2011 at 12:45 am
This is ingenious; I loved it a lot.

But wait, how come you throw in double negation into Curry-Howard isomorphism? Double negation is not an identity in an intuitionist logic; so you cannot seriously count on using de Morgan laws. I believe. I could not find yet where’s the error, but if Curry-Howard is correct, then there should be one, I think.

Comment by Vlad Patryshev on July 21, 2011 at 6:17 am
@Richard There’s not currently any way of expressing a union type as anything other than a context or view bound on a type variable so, no, you can’t do that just yet.

However, there are (tentative) plans to expose the implicit resolution mechanism (in a future version of Scala) which would enable that — with the proposal currently on the table it would look something like var intOrString : Solve[(Int |∨| String)#λ, Any] = 4. If you’re feeling brave you could give this a try by checking out and building the topic/implicits_solve branch of Adriaan Moors github mirror of the Scala toolchain.

That said, by the time this arrives in a released version of Scala we might have first class union types in the language anyway.

Comment by Miles Sabin on July 21, 2011 at 9:11 am
@Vlad I agree that the Curry-Howard isomorphism is normally presented in an intuitionistic setting, but I don’t think it’s invalid in classical logic. Alternatively, maybe the use of double negation here means that I’ve (pretty much accidentally) helped myself to the Gödel-Gentzen double negation embedding of classical into intuitionistic logic. That would be lovely given that the inspiration for this post struck me while I was rereading Geoffrey Washburns article on encoding higher-ranked types in Scala, which also uses a double negation encoding (though expressed very differently, using continuations).

I’d delighted if someone with more logical sophistication than me could shed some light on this.

Comment by Miles Sabin on July 21, 2011 at 9:20 am
This is lovely, but I think your explanation emphasizes the isomorphism too much, or provides too limited of an encoding scheme to really match the isomorphism. There is a simpler explanation for why the scheme works, which is that the argument of a function is contravariant.

Let Z[-T] be contravariant, meaning that if R <: S, then Z[S] <: Z[R]. Now let A and B be any pair of types. Since (A with B) <: A, and (A with B) <: B, it follows that Z[B] <: Z[A with B] and Z[A] <: Z[A with B]. That’s all we need.

Thus, if you define,
```
trait Contra[-A] {}
def f[A](a: A)(implicit ev: Contra[A] <:< Contra[Int with String]) = a match {
  case s: String => s
  case i: Int => i.toString
}
```
you get your union type with less work:
```
scala> f(5)
res2: String = 5

scala> f(“Wish”)
res3: String = Wish

scala> f(Some(false))
:10: error: Cannot prove that Contra[Some[Boolean]] <:< Contra[String with Int].
f(Some(false))
```
As a further improvement, you can skip the encoding entirely and just use <:< (or, rather, let <:<’s encoding, which includes a contravariant first parameter, do the work for you):
```
def g[A](a: A)(implicit ev: (Int with String) <:< A) = ...
```
The Howard-Curry isomorphism encoding, although true, is something a red herring because you cannot (AFAICT) encode type negation in a usable way, at least not easily.
Comment by Rex Kerr on July 22, 2011 at 9:57 pm
Nice, but actually, what you’ve shown is that contravariance provides yet another mechanism for encoding negation in type systems with subtyping.

Comment by Miles Sabin on July 24, 2011 at 10:04 am
Rex,

It seems to me that neither of your shorter solutions is quite correct.

The problem is that `(Int with String)` has several valid supertypes besides Int and String, namely Any, AnyRef, and AnyVal. So I can pass any value, of any class whatsoever, to your functions f and g as long as the compiler doesn’t know anything about that value except that it’s one of those types. So for example `f(Some(5): Any)` gets past the compiler, which defeats the purpose.

Miles’s code doesn’t have this problem.

Comment by Seth Tisue on August 3, 2011 at 11:04 pm
Seth,

Good point. Somehow I’d missed that. You do need the double negation to get the types right; you just don’t need a function because it’s only the contravariant parameter that matters.

So I retract my original comment: although the reason the code works is slightly less obvious than it could be, the double negation motivated by the HC isomorphism is key if you want a strict union type. Except as implemented it’s not really negation but reverse implication.

Comment by Rex Kerr on August 13, 2011 at 5:58 am
Interesting stuff, thanks.

What’s the advantage of Union types over function overloading? I can’t think of a “slam dunk” reason here. Given the union type we have to pattern match, and given overloading we have to dispatch dynamically. One could say that overloading allows for smaller functions, but perhaps unions provide an opportunity for exhaustive compiler checks on the pattern match (?)

Comment by Derek Wyatt on August 18, 2011 at 1:31 pm
Oh hell, scratch that question… :) I was only thinking about implementation of decisions like “size” and the like but clearly it’s got usages way beyond that that nobody else needs to describe since it should have been obvious.

Comment by Derek Wyatt on August 18, 2011 at 2:15 pm
Is this still supposed to work when you use type union as generic parameters for collections? (Because it doesn’t seem to work at all for me in Scala 2.9…..)

Comment by A B on August 23, 2011 at 2:29 pm
@andyd89 This only works as a bound on a type parameter, so it’s definition-site, rather than use site (the latter is what you’re trying to do).

Comment by Miles Sabin on August 23, 2011 at 4:18 pm
@Miles Does this mean that there is no way to achieve something like:
```
val collec = new scala.collection.mutable.HashSet[_ <: (String ∨ Int)]
collec.add("banana")
collec.add(7)
```
?
Comment by A B on August 23, 2011 at 8:13 pm
@andyd89 No, I’m afraid not.

Comment by Miles Sabin on August 23, 2011 at 9:11 pm
@Miles: Is there a way of defining that A is not of a certain type? In particular, that A is not a function? Something like:
```
def foo[A, B, C](a: A)(implicit ev: ¬¬[A] <: C])
```
Comment by Ittay Dror on September 13, 2011 at 4:04 am

@Ittay Yes it is possible, but it takes a slightly different encoding of negation which really deserves a blog post of its own. Here’s the general idea,

def unexpected : Nothing = sys.error("Unexpected invocation")

// Encoding for "A is not a subtype of B"
trait <:!<[A, B]

// Uses ambiguity to rule out the cases we're trying to exclude
implicit def nsub[A, B] : A <:!< B = null
implicit def nsubAmbig1[A, B >: A] : A <:!< B = unexpected
implicit def nsubAmbig2[A, B >: A] : A <:!< B = unexpected

// Type alias for context bound
type |¬|[T] = {
  type λ[U] = U <:!< T
}

def notFn[T: |¬|[_ => _]#λ](t : T) = t

val nfn1 = notFn(23)                // OK
val nfn2 = notFn("foo")             // OK
val nfn3 = notFn((x : Int) => x+1)  // Does not compile

Nb. as defined this only excludes functions of one argument.

Comment by Miles Sabin on September 13, 2011 at 10:15 am

@Miles. Amazing what great ideas come up along the(your) way. Thank you!

Comment by Peter Schmitz on September 13, 2011 at 11:39 am
@Miles: This is the solution I eventually used also (btw: http://www.tikalk.com/java/blog/avoiding-nothing), but the error message is totally incomprehensible if someone is not familiar with the trick (unlike the “could not prove that…” message for missing implicits)

Comment by Ittay Dror on September 13, 2011 at 11:45 am

I am thinking that the first class disjoint type is a sealed supertype, with the alternate subtypes, and implicit conversions to/from the desired types of the disjunction to these alternative subtypes.

I assume this addresses comments 33 – 36, so the first class type that can be employed at the use site, but I didn’t test it.

sealed trait IntOrString
case class IntOfIntOrString( v:Int ) extends IntOrString
case class StringOfIntOrString( v:String ) extends IntOrString
implicit def IntToIntOfIntOrString( v:Int ) = new IntOfIntOrString(v)
implicit def StringToStringOfIntOrString( v:String ) = new StringOfIntOrString(v)

object Int {
   def unapply( t : IntOrString ) : Option[Int] = t match {
      case v : IntOfIntOrString => Some( v.v )
      case _ => None
   }
}

object String {
   def unapply( t : IntOrString ) : Option[String] = t match {
      case v : StringOfIntOrString => Some( v.v )
      case _ => None
   }
}

def size( t : IntOrString ) = t match {
    case Int(i) => i
    case String(s) => s.length
}

scala> size("test")
res0: Int = 4
scala> size(2)
res1: Int = 2

One problem is Scala will not employ in case matching context, an implicit conversion from IntOfIntOrString to Int (and StringOfIntOrString to String), so must define extractors and use case Int(i) instead of case i : Int.

Comment by Shelby Moore III on September 18, 2011 at 9:09 am

@Shelby Moore III Maybe I’m missing something, but it looks like you’ve just replicated (a special case of) Scala’s standard Either type — ie. a boxed union type. The point of the article is to show that we can encode union types without any boxing.

Comment by Miles Sabin on September 18, 2011 at 9:26 am
Maybe also I am missing something, but seems there are several improvements over Either:

1. It extends to more than 2 types, without any additional noise at the use or definition site.
2. Arguments are boxed implicitly, e.g. don’t need size(Left(2)) or size(Right(“test”)).
3. The syntax of the pattern matching is implicitly unboxed.
4. The boxing and unboxing may be optimized away by the JVM hotspot.
5. The syntax could be the one adopted by a future first class union type, so migration could perhaps be seamless? Perhaps it would be better to use V instead of Or, e.g. IntVString, or `Int |v| String`?

Comment by Shelby Moore III on September 18, 2011 at 10:02 am
@Shelby Moore III I’m afraid you’re missing the point: the aim of this article is precisely to show the derivation of an unboxed union type — anything else, however interesting it might be in it’s own right, is off-topic.

Comment by Miles Sabin on September 18, 2011 at 10:11 am
Okay apologies. In my mind, it is for all practical purposes an unboxed solution, because the boxing and unboxing is implicit and maybe optimized away. But I can also appreciate your point, and there may be more corner cases (in addition to the one I noted) lurking with my method? Thanks for accepting my comments in spite of them being off topic.

Comment by Shelby Moore III on September 18, 2011 at 10:17 am

I was wondering whether one could generalize this to n-ary unions. Here’s my first approach for n = 3:

implicitly[¬¬[¬¬[Int]] <:< ((Int ∨ String) ∨ (Float ∨ Float))]

Works so far, but you have to extend it to a power of two, which is not too useful.

Can we do better? We can.

trait Disj[T] { 
  type or[S] = Disj[T with ¬[S]]
  type apply = ¬[T]
}

// for convenience
type disj[T] = { type or[S] = Disj[¬[T]]#or[S] }


type T = disj[Int]#or[Float]#or[String]#apply
implicitly[¬¬[Int] <:< T] // works
implicitly[¬¬[Double] <:< T] // doesn't work

Comment by Lars on November 14, 2011 at 5:31 pm

I like it … nicely done.

Comment by Miles Sabin on November 15, 2011 at 12:47 am
1) Just to understand the discussion with Rex Kerr – this code seems to work without problems, and it seems that you already agreed on that, right?

def f[A](a: A)(implicit ev: Contra[Contra[A]] <: s
case i: Int => i.toString
}

2) What is the runtime cost of constructing and passing all these proof terms? When implementing dependently-typed languages, people work hard to erase all of them – the literature suggests (implicitly) that not having erasure would be a significant problem, and it sounds quite reasonable. Now, erasure would not happen in Scala; on the contrary implicits are not just passed around but also used as conversion functions (as in comment 19); that could be avoided if the compiler knew that <:< and =:= are just identities. Either we make them built-ins, or we introduce GHC's user-specified rewrite rules for optimization in Scala, too.

Comment by Paolo G. Giarrusso on February 5, 2012 at 2:17 pm
A correction: actually <:< and =:= are just identities, but for slightly more complex reasons.
Given erasure of generics, probably <:< and =:= are identity functions but some of their calls will produce a cast in the caller (just as l.get() where l: List[Int] produces a cast to Int). Since the cast is in the caller, removing the function call _after the cast is inserted_ should be no problem.

Comment by Paolo G. Giarrusso on February 5, 2012 at 2:26 pm
@Paolo G. Giarrusso

On 1) … yes, correct.

On 2), you’re quite right that these proof terms exist at runtime. I haven’t benchmarked to see what the runtime costs are, although I suspect that a sufficiently recent JVM would do a reasonably good job of inlining (and eliminating) some of them. In practice I haven’t found this to be a problem, but in general I agree with you that currently the Scala compiler isn’t going to do as good a job of code generation for these kinds of things as languages like Agda which are designed from the ground up for this purpose.

Comment by Miles Sabin on February 5, 2012 at 2:38 pm

Negation of the disjunction (i.e. all types not in the disjunction) employing Miles’s ambiguity rule.

type ¬|∨|[T, U] = { type λ[X] = ¬¬[X] <:!< (T ∨ U) }
def size[T : (Int ¬|∨| String)#λ](t : T) = t match {
    case d : Double => d
}

scala> size(0)
error: ambiguous implicit values:
 both method nsubAmbig2 in object $iw of type [A,B >: A]<:!<[A,B]
 and method nsubAmbig1 in object $iw of type [A,B >: A]<:!<[A,B]
 match expected type <:!<[((Int) => Nothing) => Nothing,((Int) => Nothing with
  (java.lang.String) => Nothing) => Nothing]
       size(0)
           ^

scala> size(5.0)
res1: Double = 5.0

Extensible disjunction type values employing Lar’s recursive trait.

type ∨[T, U] = T with ¬[U]
class Disj[T <: (_ ∨ _)] { type or[U] = Disj[T ∨ U] }
def size[T, D <: (_ ∨ _)](t : T, d : Disj[D])(implicit ev : (¬¬[T] <:< ¬[D])) =
  t match {
    case i : Int => i
    case s : String => s.length
    case d : Double => d
  }
type T = disj[Int]#or[String]

scala> size(0,new T)
res0: Double = 0.0

scala> size("",new T)
res1: Double = 0.0

scala> size(5.0,new T)
error: could not find implicit value for parameter ev:
  <:<[((Double) => Nothing) => Nothing,
            ((Int) => Nothing with (String) => Nothing) => Nothing]
       size(5.0,new T)
           ^

scala> size(5.0,new T#or[Double])
res3: Double = 5.0

Compose them.

def size[T, D <: (_ ∨ _)](t : T, d : Disj[D])(implicit ev : (¬¬[T] <:!< ¬[D])) =
  t match {
    case i : Int => i
    case s : String => s.length
    case d : Double => d
  }

scala> size(0,new T)
error: ambiguous implicit values:
 both method nsubAmbig2 in object $iw of type [A,B >: A]<:!<[A,B]
 and method nsubAmbig1 in object $iw of type [A,B >: A]<:!<[A,B]
 match expected type <:!<[((Int) => Nothing) => Nothing,
  ((Int) => Nothing with (String) => Nothing) => Nothing]
       size(0,new T)
           ^

scala> size(5.0,new T)
res5: Double = 5.0

One use case is to statically type check the list of unique types for a list of values (one per unique type) added to a collection (the collection’s type will subsume to Any).

def addTypeToDisj[T, D <: (_ ∨ _)](t : T, d : Disj[D])
  (implicit ev : (¬¬[T] <:!< ¬[D])) = new Disj[D]#or[T]

scala> addTypeToDisj(0,new T)
error: ambiguous implicit values:
 both method nsubAmbig2 in object $iw of type [A,B >: A]<:!<[A,B]
 and method nsubAmbig1 in object $iw of type [A,B >: A]<:!<[A,B]
 match expected type <:!<[((Int) => Nothing) => Nothing,
  ((Int) => Nothing with (String) => Nothing) => Nothing]
       addTypeToDisj(0,new T)
                    ^

scala> addTypeToDisj(5.0,new T)
res5: Disj[(Int) => Nothing with
           (String) => Nothing with
           (Double) => Nothing] = Disj@df61ca

Note, I needed this for some dependently-typed kungfu where I statically type the keys of a hash map and want to statically (at compile-time) prevent duplicate operations (within each event handler function) on the state object hash map.

Comment by Shelby Moore III on February 15, 2012 at 5:21 pm

@Shelby Interesting looking stuff! You might also be interested in the (dependently typed) encoding of extensible records in shapeless.

Comment by Miles Sabin on February 16, 2012 at 1:02 am

@Miles Thanks I will have a look. To eliminate ¬¬.

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

scala> size(5.0 : Any)
error: could not find implicit value for parameter
  ev: <:<[?[Int,String],(Any) => Nothing]
       size(5.0 : Any)
           ^

Note the function type ¬[A] = A => Nothing is necessary so that we don’t otherwise get the supertype of each type in the disjunction as follows.

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

scala> size(5.0 : Any)
res8: Double = 5.0

scala> size(5.0)
error: could not find implicit value for parameter ev: <:<[Int with String,Double]
       size(5.0)
           ^

Comment by Shelby Moore III on February 20, 2012 at 5:29 pm

I don’t see how,

> because ¬¬[T] is isomorphic to T

In general (as Vlad says in #24) that’s only true for a Boolean algebra. Assuming that Scala types with subtyping is a Heyting algebra, one always has T <: ¬¬[T]. This will not work directly, this does not compile:
```
implicitly[Int <:< ¬¬[Int]]
```
but, moving to implicit conversions:
```
// x to  ¬¬[x]
implicit def toDoubleNeg[X](x: X): Function1[Function1[X,Nothing], Nothing] =
  new Function1[Function1[X,Nothing], Nothing] {
    def apply(not_X: Function1[X,Nothing]): Nothing = not_X.apply(x)
  }

// works:
implicitly[Int <%< ¬¬[Int]]
```
Concerning ¬¬[T] <: T, I don't see how you can get this.
Comment by Eduardo Pareja Tobes on March 22, 2012 at 4:59 pm
@Eduardo I think all I need for isomorphism here is that T <: U iff ¬¬[T] <: ¬¬[U] and that does hold.

Comment by Miles Sabin on March 22, 2012 at 5:30 pm
@Miles

If any of this resembles double negation, what you state is equivalent to ¬¬[U] <: U. In
```
T <: U iff ¬¬[T] <: ¬¬[U]
```
take T = ¬¬[U] and you get
```
 ¬¬[U] <: U iff ¬¬¬¬[U] <: ¬¬[U] 
```
which (should) reduce to
```
 ¬¬[U] <: U iff ¬¬[U] <: ¬¬[U] 
```
because every monad in Poset is idempotent, and double negation is a monad.
Comment by Eduardo Pareja Tobes on March 22, 2012 at 6:37 pm
@Eduardo It looks to me as though you’re asking for something much stronger than what I need here. In particular, I don’t think your reduction step is necessary. It would be if I was claiming that ¬[T] (resp. ¬¬[T]) actually was negation (resp. double negation), but I’m not, and I don’t think I need that for the purposes of this article.

Comment by Miles Sabin on March 22, 2012 at 6:51 pm
@Miles of course you don’t need any of this for the purpose of your (really nice!) article. I’m not saying that anything of what you wrote is wrong or something.

It’s just that I’d like to understand up to which point useful analogies like A => Nothing = ¬[T] can be made precise.

Anyway, I don’t see how T <: U iff ¬¬[T] <: ¬¬[U] holds; maybe it's just me :)

cheers

Comment by Eduardo Pareja Tobes on March 22, 2012 at 7:52 pm
@Eduardo ¬¬[A] is (A => Nothing) => Nothing, which is Function1[Function1[A, Nothing], Nothing]. Function1 is contravariant in it’s first type argument, so Function1[Function1[A, Nothing], Nothing] is covariant in A, hence if A <: B then Function1[Function1[A, Nothing], Nothing] <: Function1[Function1[B, Nothing], Nothing] so ¬¬[A] <: ¬¬[B].

Going back the other way is an exercise left for the reader ;-)

Comment by Miles Sabin on March 22, 2012 at 8:16 pm