Background Required: This post assumes some familiarity with the simply typed -calculus and -reduction.
Pure Type Systems
Pure Type Systems (PTS) are a class of explicitly typed -calculi. The most remarkable thing about PTSs, is that types, terms, kinds are all expressed in one syntax and with only a simple rules they can express crazy type systems.
The general system is defined as being polymorphic over three sets: a empty set of sorts , and the set of axioms and the set of rules , where contains pairs of sorts and contains triples of sorts. By selecting various we can express different -calculi.
The simply typed -calculus (STLC) can be viewed as a Pure Type System, but this system has some interesting (and sometimes annoying) properties. In this post, I will highlight some of these properties.
STLC as a Pure Type System
The typing rules for Pure Type Systems are usually expressed in their most general setting, having rules that can express dependent types and type level computation. These are not necessary to study the STLC, so in what follows we only express the rules necessary to express simple types and expressions.
In the following, the set of sorts is , ranges over sorts, and ranges over variables, and and range over terms.
Type Variables as Base Types
When studying the non-PTS STLC, we usually assume a set of base types. In the PTS version of STLC, we instead assume a base kind and allow the introduction of type variables as base types of kind .
Here the rule can be read as “ is a kind”.
The rule is used in two ways. Firstly, it allows for typing judgements of the following form which can be roughly read as “ is a new base type”.
Secondly, it allows us to introduce variables of base types into the context.
The rule allows us to type terms in extended contexts.
The rules so far, only allow us to work with types of the form . The next rule allows us to work with function types.
Using the above rule we can get typing judgements such as the following.
Abstractions and Applications
The next rules are somewhat standard and allow us to type abstractions and applications.
The above are all the rules we need to study the PTS version of the simply typed calculus. The system we presented does not have any type-level abstraction or computation, so some PTS rules were elided.
1. No Elimination Rule for Type Variables
One of the wierder quirks of the PTS version of STLC is that there are no Elimination rules for type variables. This means that the only thing that we can type in the empty context is . Anything else, must be typed in a non-empty context.
Although, there are no “closed” terms, we can still define -reduction and prove progress and preservation lemmas, they just must happen in non-empty contexts. This brings us to our second interesting fact.
2. Progress Lemma has an Additional Special Cases
The progress lemma for the non-PTS STLC is stated as follows.
Lemma (non-PTS Progress): For any , either is a variable, a -abstraction, or there exists a term such that .
The PTS version has an additional special case, since sorts are treated as first class in PTSs.
Lemma (Progress): For any , either is a variable, a -abstraction, is a sort, or there exists a term such that .
3. Only Allow Types and Sorts in Contexts
This is not specific to STLC, but to applies to any PTSs. To introduce any binding of the form into the context, we must first show that for some sort .
4. Still Simply Typed!
While the PTS version of STLC has type variables, non-type/non-sort terms are still simply typed. We still do not have any form of polymorphism, type constructors, or dependent types. We also do not have any kind of recursion.
The fact that there are no typable closed terms other than is somewhat weird, but it stems from the fact that we do not want -abstractions which are polymorphic over types when studying STLC. This makes the PTS version of STLC somewhat uninteresting. However, there are many interesting extensions of the PTS version of STLC. For example, we can introduce an additional axiom and constants and functions to study PCF in a PTS setting. We can also consider the above system extended with simple inductive types, which we will explore in a future post!