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

### 7 responses

13 06 2011

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

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

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