# 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...
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.

jQuery(window).blur( function() {
});
});

var stat_gif = document.location.protocol + "//stats.wordpress.com/g.gif?v=wpcom-no-pv";
new Image().src = stat_gif + "&baba=" + Math.random();
return true;
}

if (wpcom_adclk_recorded) { return true; } // no double counting
var stat_gif = document.location.protocol + "//stats.wordpress.com/g.gif?v=wpcom-no-pv";

new Image().src = stat_gif + "&baba=" + Math.random();
var now=new Date(); var end=now.getTime()+250;
while(true){now=new Date();if(now.getTime()>end){break;}}
return true;
}

}

if ( jQuery(".wpa script[src*='shareth.ru']").length > 0 || jQuery(".wpa iframe[src*='boomvideo.tv']").length > 0 || jQuery(".wpa iframe[src*='viewablemedia.net']").length > 0 || jQuery(".wpa .sharethrough-placement").length > 0 ) {
jQuery( '.wpa' ).css( 'width', '400px' );
}
} );

## 6 thoughts on “More Scala Typehackery”

1. michid says:

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.

• apocalisp says:

I’m confident that it can be.

• michid says:

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 ;-)

• apocalisp says:

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.

• michid says:

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