More Scala Typehackery

Inspired by this page on the Haskell Wiki, here’s a stripped down version of the lambda calculus encoded in the Scala type system:

trait Lambda {
  type subst[U <: Lambda] <: Lambda
  type apply[U <: Lambda] <: Lambda
  type eval <: Lambda
}

trait App[S <: Lambda, T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
  type apply[U] = Nothing
  type eval = S#eval#apply[T]
}

trait Lam[T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = Lam[T]
  type apply[U <: Lambda] = T#subst[U]#eval
  type eval = Lam[T]
}

trait X extends Lambda {
  type subst[U <: Lambda] = U
  type apply[U] = Lambda
  type eval = X
}
[/code]

Now to see if it works. Here's a simple identity:

scala> type x = Equal[App[Lam[X], X]#Eval, X]
defined type alias x

Yay! You might want to know what Equal is. It's a trait that doesn't typecheck unless both of its type parameters are the same (thanks, Jesper):

trait Equal[T1 >: T2 <: T2, T2]
[/code]

Let's try an expression that diverges (never terminates) in the untyped lambda calculus:

scala> type x = App[Lam[App[X, X]], Lam[App[X, X]]]#Eval
:8: error: illegal cyclic reference involving type Eval

That's Scala 2.7.4. It figures out that we're trying to construct an infinite type. Hurray! But that also means it's not Turing-equivalent. There will be other, legitimate types that it can't check either.

Try the same thing in 2.8 and you get...

Exception in thread "main" java.lang.StackOverflowError
        at scala.tools.nsc.symtab.Symbols$Symbol.isPackageClass(Symbols.scala:407)
        at scala.tools.nsc.symtab.Types$Type.isGround(Types.scala:640)
        at scala.tools.nsc.symtab.Types$Type.isGround(Types.scala:640)
        at scala.tools.nsc.symtab.Types$Type.isGround(Types.scala:640)
        at scala.tools.nsc.symtab.Types$Type.isGround(Types.scala:640)
        at scala.tools.nsc.symtab.Types$Type.isGround(Types.scala:638)
        at scala.tools.nsc.symtab.Types$Type$$anonfun$isGround$1.apply(Types.scala:638)
        at scala.tools.nsc.symtab.Types$Type$$anonfun$isGround$1.apply(Types.scala:638)
        at scala.collection.generic.LinearSequenceTemplate$class.forall(LinearSequenceTemplate.scala:97)
        at scala.collection.immutable.List.forall(List.scala:27)

...which is what you would expect. So it looks like typechecking in 2.8 has become undecidable in general. But don't fret. You really have to try hard to get this kind of result.

Data types such as the Church numerals and Booleans can be encoded in this calculus. I might post those a bit later.

Scala rocks.