In his recent blog post Miles Sabin came up with an ingenious way of expressing union types in Scala. A union type is the union of some types: its values are the union of the values of each of the individual types.

In a nutshell he first defines the negation of types as

type ¬[A] = A => Nothing

and then the union of two types via De Morgan’s law

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

With the following auxiliary constructs

type ¬¬[A] = ¬[¬[A]] type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) }

union types can be used in a very intuitive way

def size[T: (Int |∨| String)#λ](t: T) = t match { case i: Int => i case s: String => s.length } scala> size(3) res0: Int = 3 scala> size("three") res1: Int = 5 scala> size(4.2) :13: error: Cannot prove that ((Double) => Nothing) => Nothing >: Nothing with (java.lang.String) => Nothing) => Nothing. size(4.2) ^

#### … and beyond

With type negation and disjunction from above, it becomes possible to express all types whose set of values can be expressed by a term in propositional calculus. But can we do better? That is, is it possible to express types which don’t have a corresponding term in propositional calculus?

Generalizing the type constructor ∨[T, U] to some arbitrary acceptor

type Acceptor[T, U] = { type λ[X] = ... }

it becomes apparent, that all types for which there is a corresponding type level acceptor function are expressible. Since type level calculations in Scala are Turing complete, it should be possible to find an acceptor for any recursive function. This means that – in theory at least – Scala’s type system is powerful enough to express any type whose set of values is recursive.

Mark Mendel(19:38:01) :Something got garbled above.

type |∨|[T, U] = { type λ[X] = ¬¬[X] s.length

}

should be

type |∨|[T, U] = { type λ[X] = ¬¬[X] }

michid(21:22:12) :Thanks for pointing this out. Fixed.

Paolo G. Giarrusso(18:25:54) :That’s somehow buggy again – see the last two lines of:

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

type |∨|[T, U] = { type λ[X] = ¬¬[X] <: s.length

}

Is this a WordPress bug??

michid(18:55:52) :Thanks, fixed. Not sure whether this was a copy & past error or a WordPress problem. It wouldn’t be the first time that WordPress chokes on my code.

okomok(02:07:53) :>This means that – in theory at least –

In practice, we can implement even type-level balanced-search-tree.

If interested, see my sing library: https://github.com/okomok/sing

In sing, type and value are equivalent.

Greg(23:28:24) :Ok, the union type ability is pretty cool, but what’s with all the non-typeable characters? Eclipse doesn’t like these at all. In the code above in the def size piece, what does #-lambda mean after the union?

Andrew Skiba(14:28:54) :Thanks for using non-latin symbols! It finally caused me to fix my OSX terminal to support UTF8 🙂 If anybody has the same problem on Mac, here is the easy way to fix it: http://andskiba.blogspot.com/2011/09/utf8-in-osx-terminal.html

Jonathan Neufeld(19:40:17) :Two thumbs way-up for using the proper unicode symbols consistent with De Morgan’s laws. Otherwise I don’t think I would be able to follow it.

Yeti Lappen Von Mopp(22:47:24) :I don’t undestand a shit, but it looks to me a lot like mental masturbation