Union types

12 06 2011

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.

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



9 responses

13 06 2011
Mark Mendel

Something got garbled above.

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

should be

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

13 06 2011

Thanks for pointing this out. Fixed.

3 02 2012
Paolo G. Giarrusso

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

3 02 2012

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.

14 06 2011

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

16 06 2011

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?

19 09 2011
Andrew Skiba

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

24 02 2015
Jonathan Neufeld

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.

17 12 2017
Yeti Lappen Von Mopp

I don’t undestand a shit, but it looks to me a lot like mental masturbation

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: