Lambda Cube and programming languages

I've been reading about the Lambda cube type scheme of Henk Barendregt and found it interesting if a little obscure. Does anyone know of any languages that implement the "full cube" (the 8th corner of the cube). I'm familiar with Haskell but I don't think it has dependent types (axis 2 IIRC).

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


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.


There is a discussion of Dependent Types and the Calculus of Constructions in an unified way, as well as a presentation of the lambda cube, in the "Dependent Types" chapter of Advanced Topics in Types and 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.