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
}

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]

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.

About these ads

6 thoughts on “More Scala Typehackery

  1. Pretty cool!

    Can this be extended to more than one variable? For showing Turing completeness I think one would have to extend this to an arbitrary number of variables. Probably trying to implement the SKI calculus is an easier option!?

    I’ll definitively have to play around with it a bit more later.

      • After some more thinking I think it can’t. That is whether can we extend the lambda calculus implementation to an arbitrary number of variables nor can we implement the SK(I) calculus.

        The Scala type system (in the way we use it here) seems to correspond to the simply typed lambda calculus with the kinds of the Scala types corresponding to the types of the lambda terms. The simply typed lambda calculus is not Turing complete and type assignment is decidable for it.

        App[Lam[App[X, X]], Lam[App[X, X]]]#Eval
        

        Is just not typeable in the simply typed lambda calculus and the compiler could actually do better here ;-)

      • I have extended this to two variables, which would indicate that it could be extended to more, but you have to modify all the Lambda traits when adding more variables. I’m looking at extending to arbitrary number of variables, and my first inclination is that you’re right. It will ultimately be improperly kinded.

      • Yes sure but my point is that it is only extensible to n variables for a fixed n not to arbitrary many.

  2. Pingback: Scala type level encoding of the SKI calculus « Michid’s Weblog

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 )

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s