# What is the intuitive meaning of star and box in a pure type system?

The systems of the λ-cube have the axiom $\star:\square$.

I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\square$ in each interpretation?

$t : T : \star : \square$

Programs: t is a program of type T. (Possibility: T is a program of type $\star$?)

Proofs: t is a proof of theorem T. It's hard to see T as a proof of $\star$, though.

Set elements: t is a member of set T. (Possibility: T is a member of the universe $\star$ of sets. Then it seems difficult to assign a meaning to $\square$ that avoids the membership $\square : \star$.)

I'd like to fill out this table both vertically and horizontally, with both further interpretations and the missing descriptions of $\star$ and $\square$, and possibly meanings of $T : \square$ for $T \neq \star$.

Thank you!

-

$\star$ is a kind, which classifies types. $\square$ is a sort, and it classifies kinds. So this is a 4-layer deep classification. Once you get to have type-constructors, kinds get really useful. Eventually, you wish for kind-constructors too, and then you need sorts.

Turns out that you really rarely ever need to get deeper than that (even though Coq and Agda have infinitely many such levels). I am not sure I have ever read a good Curry-Howard explanation of kinds and sorts. I would hazard a guess that classical mathematics rarely worries about kinds/sorts, I would tend to dig into $n$-categories to find a good relation.

-
Then for the "Programs" interpretation we have: t is a program of type T classified by * classified by square. I was hoping that the relationships would stay the same within a given interpretation: if we say that t is a program of type T, then it seems that T should be some kind of program of type *. Then perhaps * is the type of type-checking programs? – Matthew Willis Apr 30 '10 at 2:10
Yes, T is some kind of program of type *, but usually the type language is not Turing-complete, so the type-level programs are not so complicated. That's not true when you have dependent types, like some of the systems in the lambda cube. – Jacques Carette Apr 30 '10 at 2:18

I seem to recall there’s a really good explanation of kinds and sorts in Sørensen and Urzyczyn’s Lectures on the Curry-Howard Isomorphism (a previous version is available online).

-
In any case, that's an excellent recommendation - that is a splendid set of 'lectures'. – Jacques Carette Apr 29 '10 at 23:24
There's a lot of material in the published book that are not in the online lecture notes. – Charles Stewart May 7 '10 at 11:18

I've found you won't go far wrong if you think of the objects in * as sets, and the objects in $\Box$ as proper classes. Thus, * is the proper class of all sets.

-

I found J. W. Roorda's masters thesis to be a good exposition of PTS. It is linked from here:

http://people.cs.uu.nl/johanj/MSc/jwroorda/

-