STLC as a Pure Type System

September 7, 2019,
keywords: pure type systems, simply typed lambda calculus

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 simple rules they can express crazy type systems.

The general system is defined as being polymorphic over three sets: a empty set of sorts SS, and the set of axioms AxAx and the set of rules RR, where AxAx contains pairs of sorts and RR contains triples of sorts. By selecting various S,Ax,RS, 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={,}S = \{\square{},*\}, ss ranges over sorts, x,yx,y and X,YX,Y ranges over variables, and a,b,c,fa,b,c,f and A,B,C,FA,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 *.

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

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

ΓA:BΓC:sΓ,x:CA:B(Weakening)\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 (Axiom)(\text{Axiom}) rule can be read as “* is a kind”.

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

Γ,X:X:\Gamma, X:* \vdash X : *

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

Γ,X:,x:Xx:X\Gamma, X:*, x: X \vdash x : X

The (Weakening)(\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:X:*. The next rule allows us to work with function types.

ΓA:ΓB:ΓAB:(Product)\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.

Γ,X:,Y:,x:XYx:XY\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.

Γ,x:Aa:BΓAB:Γλ(x:A).a:AB(Abstraction)\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})

Γf:ABΓa:AΓfa:B(Application)\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. Anything else, must be typed in a non-empty context.

X:λ(x:X).x:XX\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 Cases

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

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

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

Lemma (Progress): For any ΓA:\Gamma\vdash A : *, either AA is a variable, a λ\lambda-abstraction, AA is a sort, or there exists a term BB such that AβBA\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:Ax:A into the context, we must first show that A:sA:s for some sort ss.

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 Nat:\vdash Nat:* and constants 00 and functions succ,predsucc,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!