Talk:Pure type system

Redirection Problem

I found a reference in another article (Curry's Paradox) to the page for Girard's Paradox, which kindled my curiosity: I wonder what that paradox is about. So I clicked the link, and I was redirected here (the article on Pure Type Systems). Instead of finding a detailed description of the paradox, I find an article on a different subject altogether, which includes a link to the Girard's Paradox page. Of course, clicking on it just takes you right back here all over again. What's going on? Was there ever a Girard's Paradox page? What happened to it? Hccrle (talk) 20:43, 31 August 2009 (UTC)

Girard's paradox is an analogue of the Kleene-Rosser paradox in some pure type systems (U and U^- to be precise). I think this stub makes that clear enough. In order to actually present the paradox, we need first the formal definition of a PTS, followed by the definitions of those two systems. Feel free to contribute (see todo list above). Pcap ping 05:00, 1 September 2009 (UTC)

LTU thread

Paper it points to might be useful: [1] 67.119.3.55 (talk) 18:11, 3 June 2011 (UTC)

Apparent contradiction

The first paragraph says that there may be dependencies between any two pairs of sorts, but then gives an example in which this is stated to be not the case (the simply-typed lambda calculus).--greenrd (talk) 18:44, 12 May 2013 (UTC)

What's the contradiction? "May have dependencies" does not mean "must have depdendencies". Perhaps see lambda cube ? 99.153.64.179 (talk) 17:52, 25 June 2013 (UTC)

Intention unclear

"Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy, as is the case with the calculus of constructions, but this is not generally the case, e.g. the simply typed lambda calculus allows only terms to depend on terms."

It's not clear where you're going with this. Everything up to this statement seems to imply that the simply typed lambda calculus is not a pure type system. Then, in the above quoted passage, you speak of pure type systems and the simply typed lambda calculus in the same breath. Since STLC is the weakest corner of the lambda cube, this statement seems rather trivial, not relevant, and in context quite possibly a bit misleading. If you were going somewhere with this, please find a way to reformulate it (possibly in its own section). If not, then removing the statement is probably the right course of action. Comiscuous (talk) 21:19, 28 December 2021 (UTC)