7
$\begingroup$

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!

$\endgroup$

4 Answers 4

9
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Matthew
    Apr 30, 2010 at 2:10
  • 3
    $\begingroup$ 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. $\endgroup$ Apr 30, 2010 at 2:18
5
$\begingroup$

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

$\endgroup$
2
  • 1
    $\begingroup$ In any case, that's an excellent recommendation - that is a splendid set of 'lectures'. $\endgroup$ Apr 29, 2010 at 23:24
  • $\begingroup$ There's a lot of material in the published book that are not in the online lecture notes. $\endgroup$ May 7, 2010 at 11:18
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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/

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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