Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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!

share|improve this question
add comment

4 Answers

up vote 7 down vote accepted

$\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.

share|improve this answer
    
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
3  
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
add comment

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).

share|improve this answer
1  
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
add comment

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.

share|improve this answer
add comment

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/

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.