What is the intuitive meaning of star and box in a pure type system? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-25T21:46:54Z http://mathoverflow.net/feeds/question/23032 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system What is the intuitive meaning of star and box in a pure type system? Matthew Willis 2010-04-29T19:56:34Z 2011-01-29T18:55:35Z <p>The systems of the &lambda;-cube have the axiom \$\star:\square\$.</p> <p>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?</p> <p>\$t : T : \star : \square\$</p> <p><strong>Programs:</strong> t is a program of type T. (Possibility: T is a program of type \$\star\$?)</p> <p><strong>Proofs:</strong> t is a proof of theorem T. It's hard to see T as a proof of \$\star\$, though.</p> <p><strong>Set elements:</strong> 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\$.)</p> <p>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\$.</p> <p>Thank you!</p> http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/23044#23044 Answer by Jacques Carette for What is the intuitive meaning of star and box in a pure type system? Jacques Carette 2010-04-29T21:40:46Z 2010-04-30T14:23:21Z <p>\$\star\$ is a <em>kind</em>, which classifies <em>types</em>. \$\square\$ is a sort, and it classifies <em>kinds</em>. 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.</p> <p>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.</p> http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/23045#23045 Answer by Antonio E. Porreca for What is the intuitive meaning of star and box in a pure type system? Antonio E. Porreca 2010-04-29T21:49:48Z 2010-04-29T21:49:48Z <p>I seem to recall there’s a really good explanation of kinds and sorts in Sørensen and Urzyczyn’s <a href="http://www.amazon.com/Lectures-Curry-Howard-Isomorphism-Foundations-Mathematics/dp/0444520775/" rel="nofollow">Lectures on the Curry-Howard Isomorphism</a> (a previous version is available <a href="http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf" rel="nofollow">online</a>).</p> http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/48220#48220 Answer by none for What is the intuitive meaning of star and box in a pure type system? none 2010-12-03T20:56:17Z 2010-12-03T20:56:17Z <p>I found J. W. Roorda's masters thesis to be a good exposition of PTS. It is linked from here:</p> <p><a href="http://people.cs.uu.nl/johanj/MSc/jwroorda/" rel="nofollow">http://people.cs.uu.nl/johanj/MSc/jwroorda/</a></p> http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/53733#53733 Answer by robin-adams for What is the intuitive meaning of star and box in a pure type system? robin-adams 2011-01-29T18:55:35Z 2011-01-29T18:55:35Z <p>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.</p>