The far side of the lambda cube

Of course, once you investigate higher-order types, you begin to think about unifying the type and term levels.

Reading a bit about this I found some interesting links:

Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic. A recent paper I found via Ahmed, Findler, Siek, and Wadler's new Blame for All. I find the use of a counter-example database in a compiler a bit frightening, though.

Henk: A Typed Intermediate Language, from 1997, by SPJ and Erik Meijer:

There is growing interest in the use of richly-typed intermediate languages in sophisticated compilers for higher-order, typed source languages. These intermediate languages are typically stratified, involving terms, types, and kinds. As the sophistication of the type system increases, these three levels begin to look more and more similar, so an attractive approach is to use a single syntax, and a single data type in the compiler, to represent all three.

The theory of so-called pure type systems makes precisely such an identification. This paper describes Henk, a new typed intermediate language based closely on a particular pure type system, the lambda cube. On the way we give a tutorial introduction to the lambda cube.

Languages of the Future, by Tim Sheard on Omega, on which I'll post something soon.

And, Your lambda-cube is puny.

A moment of respectful silence, please.