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!

Improve this question
$\endgroup$

4 Answers 4

Reset to default
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.

Improve this answer
$\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
    Commented 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$
    – Jacques Carette
    Commented 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).

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ In any case, that's an excellent recommendation - that is a splendid set of 'lectures'. $\endgroup$
    – Jacques Carette
    Commented 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$
    – Charles Stewart
    Commented 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.

Improve this answer
$\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/

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .