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.

### Like this:

Like Loading...

*Related*

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.

I’m confident that it can be.

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.

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

nvariables for a fixednnot to arbitrary many.Pingback: Scala type level encoding of the SKI calculus « Michid’s Weblog