Skip to content

Abstracts.2017.PTS

Jump to bottom
Fabian edited this page Jan 15, 2020 · 1 revision

Pure Type Systems (PTS)

by Sandro Stucki

ITC Meeting on Thursday, 11 April 2018, 4pm in EDIT 3364.

Abstract

The framework of Pure Type Systems (PTS) captures many interesting typed lambda calculi including the simply typed lambda calculus, System F and the Calculus of Constructions in just 7 typing rules. PTSs lack some of the features you might have encountered in type theories like Agda (e.g. they don't have dependent sums/pairs or propositional equality types) but they provide a nice framework for formalizing and relating various theories (and logics) in a uniform way. For example, PTSs capture and relate all the languages in the so-called lambda cube (which I'm also going to talk about).

There are no lecture notes. Instead, I encourage you to have a look at this old book chapter by H. Barendregt:

  • H. Barendregt, Lambda Calculi with Types. Chap. 2 in the Handbook of Logic in Computer Science, Oxford University Press, 1992.

It covers the basics of typed lambda calculi as well as the PTS framework, and much more, in a very accessible way. IMO, this chapter is a must-read for anybody interested in type theory and programming languages research, and also just an excellent piece of theoretical CS writing — well worth reading!

Summary and additional pointers to the literature

  • We discussed the systems of the lambda cube, following the "edges" of the cube from the simply typed lambda calculus (STLC) to the Calculus of Constructions (CC). All these systems are discussed in Barendregt's chapter on typed lambda calculi (Sec. 5), but also in Pierce's TAPL and ATAPL:

    TAPL: B. C. Pierce, Types and programming languages, MIT Press, 2002.

    • STLC: Chap. 9,
    • System F: Chap. 23,
    • Fω: Chap. 30.

    ATAPL: B. C. Pierce, Advanced Topics in Types and Programming Languages, MIT Press, 2004.

    • LF/λP: Sec. 2.2,
    • CC: Sec. 2.6,
    • PTSs: Sec. 2.7.

  • We discussed how data structures can be encoded in System F, in particular, we discussed a typed encoding of church numerals. Wikipedia has lots of examples of untyped Church encodings, and also mentions some of the typed counterparts in the article on System F. Pierce (TAPL, Sec. 23.4, Ex. 23.4.5, etc.) and Barendregt (Sec. 5.4, Thm 5.4.3.2, Ex. 5.4.3.5) also discusses them.

    The church encodings of datatypes can be derived systematically from a datatype definition (along with their generalized fold), which might be worth discussing in a separate ITC lecture.

  • Fredrik and Andreas also mentioned the (Mogensen-)Scott encoding, which I'm not familiar with myself.

  • After the official meeting time was up, we were forced to change rooms. We continued discussing the general PTS framework and some instances (the lambda cube, λ*, "pseudo Agda") and some more encodings of "datatypes" (Leibniz equality in CC). I mentioned briefly the difference between predicative and impredicative systems, which seemed unfamiliar to most people. It might be good to have a session on impredicativity at some point?

  • I also forgot to mention that I mechanized the basic metatheory of PTSs in Agda a while back. For those who are interested, the code is available at

Clone this wiki locally