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: (¬¬[T] <:< (Int ∨ String))): Int =
  t match {
    case i: Int => i
    case d: Double => d.toInt
  }

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 ∨ Bar) as a heap value, though it does avoid the extra layer of indirection imposed by Either.)

Miles,

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

One little imperfection, though. The following compiles,

def size[A: (Int |∨| String)#λ](a: A) = a match {
  case d: Double => -1
}

Cheers,

Heiko

Interesting that Racket, generally considered a typeless scheme, has Union types.

(: 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)

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.

@hseeberger

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.

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)

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?

@mariofusco

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.

@mbolingbroke

See my reply to @hseeberger 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.

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.

@mariofusco

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.

@milessabin: 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 here.

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.

@ittayd

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.

Nice work and neat post.

In your reply to @hseeberger, 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.

Mark, 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.

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.

Mark, oh blimey … yes of course.

Awesome.

About @ittayd’s comment, is the viewable construct amenable to specialisation too?

@HRJ

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

Using this union type, how would one declare a variable, i.e., something like,

var intOrString: Union(Int & String) = 4
intOrString = "four"

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.

@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.

@vpatryshev 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.

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 of a red herring because you cannot (AFAICT) encode type negation in a usable way, at least not easily.

Nice, but actually, what you’ve shown is that contravariance provides yet another mechanism for encoding negation in type systems with subtyping.

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.

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.

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 (?)

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.

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

A B, 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).

@milessabin 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)

?

A B, No, I’m afraid not.

@milessabin 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])

@ittayd 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.

@milessabin This is the solution I eventually used, 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).

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 above, 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.

Shelby, 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.

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?

Shelby, 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.

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.

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

I like it … nicely done.

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]] <:< Contra[Contra[Int with String]]) = a match {
     case s: String => 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 commented above); 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.

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.

@Blaisorblade

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.

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.

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

@milessabin 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)
           ^

I don’t see how,

because ¬¬[T] is isomorphic to T

In general (as Vlad says above) 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.

@eparejatobes I think all I need for isomorphism here is that T <: U iff ¬¬[T] <: ¬¬[U] and that does hold.

@milessabin

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.

@eparejatobes 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.

@milessabin 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

@eparejatobes ¬¬[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 ;-)