Background Required: This post assumes some familiarity with the simply typed $\lambda$-calculus and $\beta$-reduction.

Pure Type Systems

Pure Type Systems (PTS) are a class of explicitly typed $\lambda$-calculi. The most remarkable thing about PTSs, is that types, terms, kinds are all expressed in one syntax and with only a few simple rules they can express crazy type systems.

The general system is defined as being polymorphic over three sets: a empty set of sorts $S$, and the set of axioms $Ax$ and the set of rules $R$, where $Ax$ contains pairs of sorts and $R$ contains triples of sorts. By selecting various $S, Ax, R$ we can express different $\lambda$-calculi.

The simply typed $\lambda$-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 $S = \{\square{},*\}$, $s$ ranges over sorts, $x,y$ and $X,Y$ ranges over variables, and $a,b,c,f$ and $A,B,C,F$ 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 $*$.

$$\begin{array}{c} \vdash *:\square{} \end{array}\quad(\text{Axiom})$$

$$\begin{array}{c} \Gamma \vdash A : s \\ \hline \Gamma, x:A \vdash x : A \end{array}\quad(\text{Start})$$

$$\begin{array}{c} \Gamma \vdash A : B \qquad \Gamma \vdash C : s \\ \hline \Gamma, x:C \vdash A : B \end{array}\quad(\text{Weakening})$$

Here the $(\text{Axiom})$ rule can be read as “$*$ is a kind”.

The $(\text{Start})$ rule is used in two ways. Firstly, it allows for typing judgements of the following form which can be roughly read as “$x$ is a new base type”.

$$\Gamma, X:* \vdash X : *$$

Secondly, it allows us to introduce variables of base types into the context.

$$\Gamma, X:*, x: X \vdash x : X$$

The $(\text{Weakening})$ rule allows us to type terms in extended contexts.

Function Types

The rules so far, only allow us to work with types of the form $X:*$. The next rule allows us to work with function types.

$$\begin{array}{c} \Gamma \vdash A : * \qquad \Gamma \vdash B : * \\ \hline \Gamma \vdash A \to B : * \end{array}\quad(\text{Product})$$

Using the above rule we can get typing judgements such as the following.

$$\Gamma, X:*, Y:*, x: X \to Y \vdash x : X \to Y$$

$\lambda$ Abstractions and Applications

The next rules are somewhat standard and allow us to type $\lambda$ abstractions and applications.

$$\begin{array}{c} \Gamma,x:A \vdash a : B \qquad \Gamma \vdash A \to B : * \\ \hline \Gamma \vdash \lambda (x:A).a : A \to B \end{array}\quad(\text{Abstraction})$$

$$\begin{array}{c} \Gamma \vdash f : A \to B \qquad \Gamma \vdash a : A \\ \hline \Gamma \vdash f\,a : B \end{array}\quad(\text{Application})$$

The above are all the rules we need to study the PTS version of the simply typed $\lambda$ calculus. The system we presented does not have any type-level abstraction or computation, so some PTS rules were elided.

Interesting Facts

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 $\vdash * : \square$. Everything else must be typed in a non-empty context.

$$\begin{array}{c} X:* \vdash \lambda (x:X).x : X \to X \end{array}$$

Although, there are no “closed” terms, we can still define $\beta$-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 Case

The progress lemma for the non-PTS STLC is stated as follows.

Lemma (non-PTS Progress): For any $\Gamma\vdash A : *$, either $A$ is a variable, a $\lambda$-abstraction, or there exists a term $B$ such that $A\to_{\beta}B$.

The PTS version has an additional special case, since sorts are treated as first class and are an additional normal form in PTS.

Lemma (Progress): For any $\Gamma\vdash A : *$, either $A$ is a variable, a $\lambda$-abstraction, $A$ is a sort, or there exists a term $B$ such that $A\to_{\beta}B$.

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 $x:A$ into the context, we must first show that $A:s$ for some sort $s$.

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.

Conclusion

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 $\lambda$-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 $\vdash Nat:*$ and constants $0$ and functions $succ,pred$ 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!