A Scala Puzzler

I’ve been toying around with Scala’s type system a little bit, and I’ve come to the conclusion that it’s completely brilliant. And I’m very encouraged by how rapidly it has improved.

There is, for example, limited support for type-level computation. But not so much that typing becomes undecidable.

In Scala, types can have type members, and those members can take type parameters. Type members can be bounded, and so can their parameters.

trait Lambda { type a[A <: Lambda&#93; <: Lambda }

&#91;/code&#93;</pre>
This feature gives you quite a lot of expressive power in the type system. Type members are accessed by use of the # symbol. You can nest types, so Scala effectively has closures for types. So you can do crazy stuff like this:
<pre>
  trait S extends Lambda { type a[X <: Lambda&#93; = Lambda { type a&#91;Y <: Lambda&#93; = Lambda { type a&#91;Z&#93; = X#a&#91;Z&#93;#a&#91;Y#a&#91;Z&#93;&#93; }} }
&#91;/code&#93;</pre>
OK, since we basically have the power of the lambda calculus in the type system, let's see if we can do Church encoding of datatypes. It turns out that we can, to an extent. Here are booleans:
<pre>
  trait Boolean { type cond[t, f] }
  trait TFalse extends Boolean { type cond[t, f] = f }
  trait TTrue extends Boolean { type cond[t, f] = t }

Let's test that out.
scala> val x: TTrue#cond[Int, String] = 10
x: TTrue#cond[Int,String] = 10

scala> val x: TTrue#cond[Int, String] = "10"
:6: error: type mismatch;
 found   : java.lang.String("10")
 required: TTrue#cond[Int,String]
 val x: TTrue#cond[Int, String] = "10"
It works. We can assign an Int to the value if the condition is TTrue, and a String if it's TFalse, but not vice versa.
How about church numerals? Here are those:
trait Num { type a[F[_], X] }
trait Zero extends Num { type a[F[_], X] = X }
trait One extends Num { type a[F[_], X] = F[X] }
trait Two extends Num { type a[F[_], X] = F[F[X]] }
trait Three extends Num { type a[F[_], X] = F[F[F[X]]] }

The way this works is that the numerals take some type constructor F and a unit type X. For example, to get lists of strings three levels deep, Three#a[List, String] is equivalent to the type List[List[List[String]]]
scala> val x: Three#a[List, String] = List(List(List("Three")), List(List("Levels"), List("Deep")))
x: Three#a[List,String] = List(List(List(Three)), List(List(Levels), List(Deep)))
We can even do some arithmetic. Here are three type-level functions. Respectively, they add two numbers together, increment a number by one, and multiply one number by another:
trait PApp[F[P[_], _], A[_]] {
  type a[X] = F[A, X]
}

trait Plus[M <: Num, N <: Num] extends Num { type a[F[_], X] = M#a[F, N#a[F, X]] }
trait Succ[N <: Num] extends Num { type a[F[_], X] = F[N#a[F, X]] }
trait Mult[M <: Num, N <: Num] extends Num { type a[F[_], X] = PApp[N#a, PApp[M#a, F]#a]#a[X] }
[/code]
Pretty sweet. For example, a List of Strings 20 levels deep would be of the type Mult[Succ[Three], Plus[Two, Three]]]#a[List, String]
Now for the puzzler.
Exercise: Write a type-level function Exp[M, N] that yields the Church numeral M lifted to the Nth power. Can it be done? If not, why not?