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.

Type Level Programming: Equality

18 06 2010

Apocalisp has a great series on Type Level Programming with Scala. At some point the question came up whether it is possible to determine equality of types at run time by having the compiler generate types representing true and false respectively. Here is what I came up with.

trait True { type t = True }
trait False { type t = False }

case class Equality[A] {
  def check(x: A)(implicit t: True) = t
  def check[B](x: B)(implicit f: False) = f
object Equality {
  def witness[T] = null.asInstanceOf[T]
  implicit val t: True = null
  implicit val f: False = null

// Usage:
import Equality._
val test1 = Equality[List[Boolean]] check witness[List[Boolean]]
implicitly[test1.t =:= True]
// Does not compile since tt is True
// implicitly[test1.t =:= False]  

val test2 = Equality[Nothing] check witness[AnyRef]
// Does not compile since ft is False
// implicitly[test2.t =:= True]  
implicitly[test2.t =:= False]

Admittedly this is very hacky. For the time being I don’t see how to further clean this up. Anyone?

Scala type level encoding of the SKI calculus

29 01 2010

In one of my posts on type level meta programming in Scala the question of Turing completeness came up already. The question is whether Scala’s type system can be used to force the Scala compiler to carry out any calculation which a Turing machine is capable of. Various of my older posts show how Scala’s type system can be used to encode addition and multiplication on natural numbers and how to encode conditions and bounded loops.

Motivated by the blog post More Scala Typehackery which shows how to encode a version of the Lambda calculus which is limited to abstraction over a single variable in Scala’s type system I set out to further explore the topic.

The SKI combinator calculus

Looking for a calculus which is relatively small, easily encoded in Scala’s type system and known to be Turing complete I came across the SKI combinator calculus. The SKI combinators are defined as follows:

Ix \rightarrow x ,
Kxy \rightarrow x ,
Sxyz \rightarrow xz(yz) .

They can be used to encode arbitrary calculations. For example reversal of arguments. Let R \equiv S(K(SI))K . Then

R x y \equiv
S(K(SI))K x y \rightarrow
K(SI)x(Kx)y \rightarrow
SI(Kx)y \rightarrow
Iy(Kxy) \rightarrow
Iyx \rightarrow yx .

Self application is used to find fixed points. Let \beta \equiv S(K\alpha)(SII) for some combinator \alpha . Then \beta\beta \rightarrow \alpha(\beta \beta) . That is, \beta\beta is a fixed point of \alpha . This can be used to achieve recursion. Let R be the reversal combinator from above. Further define

A_0 x \equiv c for some combinator c and
A_n x \equiv x A_{n-1} .

That is, combinator A_n is the combinator obtained by applying its argument to the combinator A_{n-1}. (There is a bit of cheating here: I should actually show that such combinators exist. However since the SKI calculus is Turing complete, I take this for granted.) Now let \alpha be R in \beta from above (That is we have \beta \equiv S(KR)(SII) now). Then

\beta\beta A_0 \rightarrow c

and by induction

\beta\beta A_n \rightarrow \beta\beta A_{n-1} \rightarrow c.

Type level SKI in Scala

Encoding the SKI combinator calculus in Scala’s type system seems not too difficult at first. It turns out however that some care has to be taken regarding the order of evaluation. To guarantee that for all terms which have a normal form, that normal form is actually found, a lazy evaluation order has to be employed.

Here is a Scala type level encoding of the SKI calculus:

trait Term {
  type ap[x <: Term] <: Term
  type eval <: Term
// The S combinator
trait S extends Term {
  type ap[x <: Term] = S1[x] 
  type eval = S
trait S1[x <: Term] extends Term {
  type ap[y <: Term] = S2[x, y]
  type eval = S1[x]
trait S2[x <: Term, y <: Term] extends Term {
  type ap[z <: Term] = S3[x, y, z]
  type eval = S2[x, y]
trait S3[x <: Term, y <: Term, z <: Term] extends Term {
  type ap[v <: Term] = eval#ap[v]
  type eval = x#ap[z]#ap[y#ap[z]]#eval

// The K combinator
trait K extends Term {
  type ap[x <: Term] = K1[x]
  type eval = K
trait K1[x <: Term] extends Term {
  type ap[y <: Term] = K2[x, y]
  type eval = K1[x]
trait K2[x <: Term, y <: Term] extends Term {
  type ap[z <: Term] = eval#ap[z]
  type eval = x#eval
// The I combinator
trait I extends Term {
  type ap[x <: Term] = I1[x]
  type eval = I
trait I1[x <: Term] extends Term {
  type ap[y <: Term] = eval#ap[y]
  type eval = x#eval

Further lets define some constants to act upon. These are used to test whether the calculus actually works.

trait c extends Term {
  type ap[x <: Term] = c
  type eval = c
trait d extends Term {
  type ap[x <: Term] = d
  type eval = d
trait e extends Term {
  type ap[x <: Term] = e
  type eval = e

Eventually the following definition of Equals lets us check types for equality:

case class Equals[A >: B <:B , B]()

Equals[Int, Int]     // compiles fine
Equals[String, Int] // won't compile

Now lets see whether we can evaluate some combinators.

  // Ic -> c
  Equals[I#ap[c]#eval, c]
  // Kcd -> c
  Equals[K#ap[c]#ap[d]#eval, c]

  // KKcde -> d
  Equals[K#ap[K]#ap[c]#ap[d]#ap[e]#eval, d]
  // SIIIc -> Ic
  Equals[S#ap[I]#ap[I]#ap[I]#ap[c]#eval, c]

  // SKKc -> Ic
  Equals[S#ap[K]#ap[K]#ap[c]#eval, c]

  // SIIKc -> KKc
  Equals[S#ap[I]#ap[I]#ap[K]#ap[c]#eval, K#ap[K]#ap[c]#eval]

  // SIKKc -> K(KK)c
  Equals[S#ap[I]#ap[K]#ap[K]#ap[c]#eval, K#ap[K#ap[K]]#ap[c]#eval]

  // SIKIc -> KIc
  Equals[S#ap[I]#ap[K]#ap[I]#ap[c]#eval, K#ap[I]#ap[c]#eval]

  // SKIc -> Ic
  Equals[S#ap[K]#ap[I]#ap[c]#eval, c]
  // R = S(K(SI))K  (reverse)
  type R = S#ap[K#ap[S#ap[I]]]#ap[K]
  Equals[R#ap[c]#ap[d]#eval, d#ap[c]#eval]

Finally lets check whether we can do recursion using the fixed point operator from above. First lets define \beta .

  // b(a) = S(Ka)(SII)
  type b[a <: Term] = S#ap[K#ap[a]]#ap[S#ap[I]#ap[I]]

Further lets define some of the A_ns from above.

trait A0 extends Term {
  type ap[x <: Term] = c
  type eval = A0
trait A1 extends Term {
  type ap[x <: Term] = x#ap[A0]#eval
  type eval = A1
trait A2 extends Term {
  type ap[x <: Term] = x#ap[A1]#eval
  type eval = A2

Now we can do iteration on the type level using a fixed point combinator:

  // Single iteration
  type NN1 = b[R]#ap[b[R]]#ap[A0]
  Equals[NN1#eval, c]

  // Double iteration
  type NN2 = b[R]#ap[b[R]]#ap[A1]
  Equals[NN2#eval, c]

  // Triple iteration
  type NN3 = b[R]#ap[b[R]]#ap[A2]
  Equals[NN3#eval, c]

Finally lets check whether we can do ‘unbounded’ iteration.

trait An extends Term {
  type ap[x <: Term] = x#ap[An]#eval
  type eval = An
// Infinite iteration: Smashes scalac's stack
  type NNn = b[R]#ap[b[R]]#ap[An]
  Equals[NNn#eval, c]

Well, we can😉

$ scalac SKI.scala
Exception in thread "main" java.lang.StackOverflowError
        at scala.tools.nsc.symtab.Types$SubstMap.apply(Types.scala:3165)
        at scala.tools.nsc.symtab.Types$SubstMap.apply(Types.scala:3136)
        at scala.tools.nsc.symtab.Types$TypeMap.mapOver(Types.scala:2735)

Meta-Programming with Scala: Conditional Compilation and Loop Unrolling

29 10 2008

The kind of comments I keep getting on my static meta-programming with Scala blogs are often along the lines of: “The ability to encode Church Numerals in Scala still seems uselessly academic to me, but cool none-the-less”. In this blog I will show how meta-programming can be applied in practice – at least theoretically.

In my previous blogs I introduced a technique for static meta-programing with Scala. This technique uses Scala’s type system to encode values and functions on these values. The Scala compiler acts as interpreter of such functions. That is, the type checking phase of the Scala compiler actually carries out calculations like addition and multiplication.

In this post I show how to apply meta-programming for two practical problems: conditional compilation and loop unrolling. The examples make use of type level encoding for booleans and natural numbers. While I introduced an encoding for natural numbers before, I use an alternative method which is more powerful in this post. Previously it was not possible to build nested expressions having expressions as operands themselves. The new encoding supports such expressions. However, in general the new encoding depends on the -Yrecursion compiler flag which is experimental and as of now only available in the Scala trunk. The type level encoding for booleans is along the same lines as the one for natural numbers.

Conditional Compilation

Conditional compilation is useful for example for enabling or disabling debugging or logging statements. Ideally code which is excluded by a compile time condition does not have any effect on the run-time behavior of the rest of the code. That is, the rest of the code behaves exactly as if the excluded code were not there at all. Optimizing compilers generally remove code which is unreachable. This is where meta-programming fits in: type level encoded functions (meta-functions) are evaluated at run-time. The result of the evaluation is a type. Now we only need to trick the compiler into compiling a block of code or not compiling it depending on that type.

Lets first define meta-booleans and some operations on them (full code here):

object Booleans {
  trait BOOL {
    type a[t <: BOOL, f <: BOOL&#93; <: BOOL
    type v = a&#91;TRUE, FALSE&#93;
  final class TRUE extends BOOL {
    type a&#91;t <: BOOL, f <: BOOL&#93; = t
  final class FALSE extends BOOL{
    type a&#91;t <: BOOL, f <: BOOL&#93; = f
  trait IF&#91;x <: BOOL, y <: BOOL, z <: BOOL&#93; extends BOOL {
    type a&#91;t <: BOOL, f <: BOOL&#93; = x#a&#91;y, z&#93;#a&#91;t, f&#93;
  trait NOT&#91;x <: BOOL&#93; extends BOOL {
    type a&#91;t <: BOOL, f <: BOOL&#93; = IF&#91;x, FALSE, TRUE&#93;#a&#91;t, f&#93;
  trait AND&#91;x <: BOOL, y <: BOOL&#93; extends BOOL {
    type a&#91;t <: BOOL, f <: BOOL&#93; = IF&#91;x, y, FALSE&#93;#a&#91;t, f&#93;
  trait OR&#91;x <: BOOL, y <: BOOL&#93; extends BOOL {
    type a&#91;t <: BOOL, f <: BOOL&#93; = IF&#91;x, TRUE, y&#93;#a&#91;t, f&#93;

  // aliases for nicer syntax
  type !&#91;x <: BOOL&#93; = NOT&#91;x&#93;
  type ||&#91;x <: BOOL, y <: BOOL&#93; = OR&#91;x, y&#93;
  type &&&#91;x <: BOOL, y <: BOOL&#93; = AND&#91;x, y&#93;

The following pre-processor object contains an <a href="http://www.scala-lang.org/node/114">implicit</a> method for converting a value of type <em>TRUE</em> to an <em>Include</em> object whose <em>apply</em> method executes a block of code. Similarly it contains an implicit method for converting a value of type <em>FALSE</em> to an <em>Exclude</em> object whose <em>apply</em> method simply does nothing. The strange line where <em>null</em> is being cast to <em>B</em> is a trick for getting a witnesses of a value of type <em>B</em>.

object PreProc {
  def IF[B] = null.asInstanceOf[B]

  object Include {
    def apply(block: => Unit) {

  object Exclude {
    def apply(block: => Unit) { }

  implicit def include(t: TRUE) = Include
  implicit def exclude(f: FALSE) = Exclude

Using these definitions is quite convenient now:

object IfDefTest {
  import PreProc._

  type LOG = TRUE
  type ERR = TRUE
  type WARN = FALSE

  def errTest() {
    IF[(LOG && ERR)#v] {

  def warnTest() {
    IF[(LOG && WARN)#v] {

  def main(args: Array[String]) {

Running the above code will print err but wont print warn to the console.

Loop Unrolling

Another application for static meta-programming is loop unrolling. When the number of iterations of a loop is small and only depends on quantities known at compile time, run time performance might profit from unrolling that loop. Instead of resorting to copy paste, we can use similar techniques like above.

Again let’s first define meta-naturals and their operations (full code here):

object Naturals {
  trait NAT {
    type a[s[_ <: NAT&#93; <: NAT, z <: NAT&#93; <: NAT
    type v = a&#91;SUCC, ZERO&#93;
  final class ZERO extends NAT {
    type a&#91;s&#91;_ <: NAT&#93; <: NAT, z <: NAT&#93; = z
  final class SUCC&#91;n <: NAT&#93; extends NAT {
    type a&#91;s&#91;_ <: NAT&#93; <: NAT, z <: NAT&#93; = s&#91;n#a&#91;s, z&#93;&#93;
  type _0 = ZERO
  type _1 = SUCC&#91;_0&#93;
  type _2 = SUCC&#91;_1&#93;
  type _3 = SUCC&#91;_2&#93;
  type _4 = SUCC&#91;_3&#93;
  type _5 = SUCC&#91;_4&#93;
  type _6 = SUCC&#91;_5&#93;

  trait ADD&#91;n <: NAT, m <: NAT&#93; extends NAT {
    type a&#91;s&#91;_ <: NAT&#93; <: NAT, z <: NAT&#93; = n#a&#91;s, m#a&#91;s, z&#93;&#93;
  trait MUL&#91;n <: NAT, m <: NAT&#93; extends NAT {
    trait curry&#91;n&#91;_&#91;_&#93;, _&#93;, s&#91;_&#93;&#93; { type f&#91;z&#93; = n&#91;s, z&#93; }
    type a&#91;s&#91;_ <: NAT&#93; <: NAT, z <: NAT&#93; = n#a&#91;curry&#91;m#a, s&#93;#f, z&#93;

  // aliases for nicer syntax
  type +&#91;n <: NAT, m <: NAT&#93; = ADD&#91;n, m&#93;
  type x&#91;n <: NAT, m <: NAT&#93; = MUL&#91;n, m&#93;

The pre-processor object defines a trait <em>Loop</em> having an <em>apply</em> method which takes a block of code as argument. Again there are two implicit conversion methods. One which converts the zero type to a <em>Loop</em> with an empty <em>apply</em> function. An another one which convert the type <em>N + 1</em> to a a <em>Loop</em> with an <em>apply</em> function which executes the block once and then applies itself to the type <em>N</em>.

object PreProc {
  def LOOP[N] = null.asInstanceOf[N]

  trait Loop[N] {
    def apply(block: => Unit)

  implicit def loop0(n: ZERO) = new Loop[ZERO] {
    def apply(block: => Unit) { }

  implicit def loop[N <: NAT&#93;(n: SUCC&#91;N&#93;)(implicit f: N => Loop[N]) = new Loop[SUCC[N]] {
    def apply(block: => Unit) {

Again using this is easy and convenient:

object LoopUnroll {
  import PreProc._

  def unrollTest() {
    // The following line needs the -Yrecursion 1 flag
    // LOOP[(_3 x _2)#v] {
    LOOP[_6] {
      println("hello world")

  def main(args: Array[String]) {

The above code prints the string “hello word” six times to the console.


Scala’s type system is powerful enough for encoding commonly encountered functions. Together with Scala’s strong capability for creating internal DSLs, this results in convenient techniques for static meta-programming. Such techniques can be applied to practical problems – at least in theory. In practice Scala’s support is not (yet?) there. For one the technique presented here depends on an experimental compiler flag (-Yrecursion). Further the types required for meta-programming might causes an exponential growth in compilation time which is not desirable. And finally an analysis with c1visualizerwith showed, that the compiler seems not to remove all unnecessary calls.

Meta-Programming with Scala Part III: Partial function application

27 08 2008

In my previous post about Meta-Programming with Scala I suspected that there was no way to express partial function application in Scala’s type system. However Matt Hellige proofed me wrong in his comment.

His solution uses a trait for partially applying a function to some of its arguments. An abstract type exposed by the trait represents the resulting function which takes the remaining arguments.

object Partial {
  // Partial application of f2 to x
  trait papply[f2[_, _], x] {
    type f1[y] = f2[x, y]

  // apply f to x
  type apply[f[_], x] = f[x]

  trait X
  trait Y
  trait F[A1, A2]

  // Test whether applying the partial application of
  // F to X to Y equals in the type F[X, Y]
  case class Equals[A >: B <: B, B&#93;
  Equals&#91;apply&#91;papply&#91;F, X&#93;#f1, Y&#93;, F&#91;X, Y&#93;&#93;
Having this solved we can define a type which encodes <a href="https://michid.wordpress.com/2008/07/30/meta-programming-with-scala-part-ii-multiplication/">multiplication on the Church Numerals</a>.

    trait curry[n[_[_], _], s[_]] {
      type f[z] = n[s, z]

    // Multiplication for this encoding
    type mult[m[_[_], _], n[_[_], _], s[_], z] = m[curry[n, s]#f, z]

A full working example is available from my code page. Note, the code takes forever (i.e. some minutes) to compile. Matt also noted an issue with squares. With my version of the compiler (Ecipse plugin 2.7.2.r15874-b20080821120313) the issue does not show up however.

Meta-Programming with Scala Part II: Multiplication

30 07 2008

This was sitting on my desk for quite a while now while I was busy with other things. Finally I came around to write things up.

In my last post I showed how to encode the Church numerals and addition on them with Scala’s type system. I mentioned that this approach does not seem to scale. In this post I show the problems I faced while I tried to extend the approach to multiplication. This particular example shows that Scala’s type system does not seem to support partial function application which in general is crucial for defining more complex functions base on simpler ones. But before delving into Scala, let’s review the church numerals in lambda calculus.

Define a lambda term for each natural number n

0\equiv\lambda sz.z
1\equiv\lambda sz.sz
2\equiv\lambda sz.ssz
n\equiv\lambda sz.s^nz

where s^n stands for the n-fold application of s. Think of s standing for successor and z for zero. Then the number n is simply the n-fold successor of zero.

Addition can now be define as

add \equiv \lambda mnsz.ms(nsz) .

Here the n-fold successor of zero is used as zero element for m. Again this can be thought of as the m-fold successor of the n-fold successor of zero.

Multiplications is similar but instead of using a different value for zero, a different successor function is used:

mul \equiv \lambda mnsz.m(ns)

This boils down to the m-fold application of the n-fold successor function.

As in my previous post the Church numerals are encoded in Scala’s type system as follows

type _0[s[_], z] = z
type _1[s[_], z] = s[z]
type _2[s[_], z] = s[s[z]]
type _3[s[_], z] = s[s[s[z]]]
type _4[s[_], z] = s[s[s[s[z]]]]

I did not succeed encoding multiplication however. The most straight forward encoding – which closely follows the one for addition – looks like this

type mul[m[s[_], z], n[s[_], z], s[_], z] = m[n[s[_], z], z]

However the Scala compiler complains:

  s[_$1] forSome { type _$1 } takes no type parameters, 
  expected: one

Unlike addition, we need to pass a partially applied function here – namely the n-fold successor function. Since the above does not work, I’m not sure if there even is a syntax for expressing partial function application in Scala’s type system.

In another approach I tried to introducing a formal parameter for the n-fold successor function:

type mul[m[n[s[_], z], z], n[s[_], z], s[_], z] = m[n, z]

The compiler does not complain here which is encouraging. However this breaks on application

abstract class Zero
abstract class Succ[T]

type zero = mul[_0, _0, Succ, Zero] 
type one = mul[_1, _3, Succ, Zero] 

The first application results in a kind error

the kinds of the type arguments (Meta._0,Meta._0,Meta.Succ,Meta.Zero) do not conform to 
the expected kinds of the type parameters (type m,type n,type s,type z).
Meta._0's type parameters do not match type m's expected parameters: 
type s has one type parameter, but type n has two	

The second application causes an assertion failure of the Scala compiler (see Ticket #742).

For a better understanding let’s analyze what mul[_1, _3, Succ, Zero] expands to:

mul[_1, _3, Succ, Zero] =
_1[_3, Zero] =

While this looks somewhat correct, it is certainly not. _3 takes two arguments but gets one. This is exactly what the Scala compiler was complaining about.

Meta-Programming with Scala Part I: Addition

18 04 2008

In the solution to a puzzle I posted earlier, I mentioned that the taken approach might be a first step towards meta-programming in Scala.

While the approach to determine the depth of a type plays nicely with the Church encodings of natural numbers proposed in the paper Towards Equal Rights for Higher-kinded Types, defining arbitrary arithmetic operators seems problematic. Addition does not pose a problem. But there seems to be no easy generalization to other arithmetic operators. This is despite the fact that the authors of the above paper mention that Scala’s kinds correspond to the types of the simply typed lambda calculus.

In this post I will explain how to represent the natural numbers and an addition operator using Scala’s type system. In a later post I will show why this approach does not easily scale to the other arithmetic operators like multiplication and why I think that this might not be a problem of Scala’s type system in general but rather a shortcoming of its syntax. Finally I noted that Scala 2.7.1.RC1 dropped the contractiveness requirement for implicits. This might open up another way for meta-programming. I probably write more on this in yet another post.

The following code shows a Church encoding of the natural numbers in Scala’s type system. (The full source is available from my code page).

  type _0[s[_], z] = z
  type _1[s[_], z] = s[z]
  type _2[s[_], z] = s[s[z]]
  type _3[s[_], z] = s[s[s[z]]]
	// ...

A natural numbers is encoded as a type function which takes two arguments: a successor function and a zero element. The n-th natural number is then the n-fold application of the successor function to the zero element. Such natural numbers can be instantiated by passing them an actual type for its successor function and its zero element. The depth function form my last post can then be used to evaluate such a number;

  abstract class Zero
  abstract class Succ[T]
  type two = _2[Succ, Zero] 
  println(depth(nullval[two]))  // prints 2

We can now define an addition operator like this:

  type plus[m[s[_], z], n[s[_], z], s[_], z] = n[s, m[s, z]]
  type +[m[s[_], z], n[s[_], z]] = plus[m, n, Succ, Zero]

Basically plus takes two Church numerals n and m and composes them such that m becomes the zero element of n. The second line defines an infix + operator:

  println(depth(nullval[_2 + _2])) // prints 4
  println(depth(nullval[_2 + _3])) // prints 5

Let’s analyze in detail what _2 + _3 expands to in order to better understand above code:

  _2 + _3 =
	plus[_2, _3, Succ, Zero] =
	_3[Succ, _2[Succ, Zero]] =
	_3[Succ, Succ[Succ[Zero]]] =

So passing _2 + _3 to the depth function will indeed print 5 since this its structural depth.

From here one might want to generalize this to other arithmetic operations. I tried multiplication but failed so far. In a next post I will explain my closest shot(s) at multiplication and I will explain what I think are the difficulties with this approach.


Get every new post delivered to your Inbox.