Lambda the Ultimate

Well, the 8th corner is essentially the calculus of constructions. Add inductive definitions to this and you get CIC, the calculus of inductive constructions, which is essentially the type theory of Coq.

The interesting question is, what PLs correspond to the other corners? Algol is pretty much like the simply typed lambda calculus (i.e., the 1st corner). Adding (Term)Type quantification is dependent typing, which is essentially statically-checked assertions for a programming language, opening the way for code to come with correctness proofs. Adding (Type)(Type) quantification is a bit like adding type classes. The real power comes from adding (Type)(Term) abstraction to the PL, which is first-class polymorphism.

Postscript: Oh, this overlaps an older topic: The Lambda Cube & Some Programming Languages.

Pure Type Systems for Functional Programming
We present a functional programming language based on Pure Type Systems (PTSs). We show how we can define such a language by extending the PTS framework with algebraic data types, case expressions and definitions. To be able to experiment with our language we present an implementation of a type checker and an interpreter for our language.

PTSs are well suited as a basis for a functional programming language because they are at the top of a hierarchy of increasingly stronger type systems. The concepts of `existential types', `rank-n polymorphism' and `dependent types' arise naturally in functional programming languages based on the systems in this hierarchy. There is no need for ad-hoc extensions to incorporate these features.

The type system of our language is more powerful than the Hindley-Milner system. We illustrate this fact by giving a number of meaningful programs that cannot be typed in Haskell but are typable in our language. A `real world' example of such a program is the mapping of a specialisation of a Generic Haskell function to a Haskell function.

Unlike the description of the Henk language by Simon Peyton Jones and Erik Meijer we give a complete formal definition of the type system and the operational semantics of our language. Another difference between Henk and our language is that our language is defined for a large class of Pure Type Systems instead of only for the systems of the lambda-cube.

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 stratied, 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 identication. This paper describes Henk, a new typed intermediate language based closely on a particular pure type system, the lambda cube.