Term : Type : Kind : Sort

I've been reading a really interesting paper called "Introduction to Generalized Type Systems" in which the system of the lambda cube are discussed. The lambda cube consists of 8 systems, one on each point of the cube, where the simplest system is our good friend the simply typed lambda calculus and the most complex system is the calculus of construction (which has an awesome name). They consider only fairly simple situations in this paper by not including some of the operators and rules that can be defined, but the resulting theory is still very rich and complex.

There are several really neat things about this material. One is that they define a hierarchy of types that goes like this- term:type:kind:sort, where ":" is pronounced "in". A term is the basic object of the lambda calculus and involves constants, variables, lambda abstraction and application. If we group terms into what are basically sets, we get the types, and we can extend the system with different type operators to model things in programming and logic. Not only can there be abstract on the term level, but we can abstract on the type level as well, giving a type constructor (like an array type in most languages). While all normal (monomorphic) types are in the same kind, *, the type constructors have kinds built from * and ->. This means that we can have *->*, which may create lists of some type for example, or even (*->*)->* which looks suspiciously like a fix point operators (indeed there are some really cool applications of the fixed point of a type in Haskell). So these kinds can not be described simply by the symbol *, so how do we classify them? We don't want to lead ourselves into a paradox by defining *:* (kind is of kind kind) so we have another layer on top of kinds. In this paper they use a square box that I can't produce with ascii characters. This last layer is called the "sort" of a kind.

It is interesting that the systems become more and more restricted as we go up in the hierarchy- terms are basically unrestricted except when we only take those terms which can be given types, which have several operators on them are can be very complex with things like universal and existential quantification, products and co-products if we want them. If we take the simply typed lambda calculus then all types have kind *, but if we consider a more complex calculus like System F then the kinds form a simply typed lambda calculus, and it is on the sort level that there is only one symbol, the box.

Another neat thing about the material is that the lambda cube corresponds to a logic cube- a series of systems of logic with the same inclusion relation and the corresponding features as those of the lambda cube. I haven't gotten that far yet, but I always found the relation to logic very interesting.

The last thing I want to say is that the proof technique they use is very interesting. The first time I tried to read this paper I had no idea what was going on- they defined 8 systems all at once and proceed to prove things in all 8 simultaneously. I've been reading about called "Categories for Types" in which they describe a way of defining algebraic systems that is similar to what is used in this paper, which has helped a lot.