Pure Type Systems without Explicit Contexts

TL;DR

This paper introduces a novel formulation of pure type systems that omits explicit contexts in typing judgments, using an infinite shared context to maintain equivalence with traditional systems.

Contribution

It proposes a context-free approach to pure type systems, maintaining equivalence with standard formulations through an infinite shared context.

Findings

Equivalent to traditional pure type systems

Uses an infinite shared context for type judgments

Maintains the distinction between free and bound variables

Abstract

We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments of shape "A : B". A key feature is that we distinguish free and bound variables even in pseudo-terms. Specifically we give the rules of the "Pure Type System" class of type theories in this style. We prove that the typing judgments of these systems correspond in a natural way with those of Pure Type Systems as traditionally formulated. I.e., our systems have exactly the same well-typed terms as traditional presentations of type theory. Our system can be seen as a type theory in which all type judgments share an identical, infinite, typing context that has infinitely many variables for each possible type. For this reason we call our system "Gamma_infinity". This name means to suggest that our type judgment "A : B" should be read as "Gamma_infinity |- A : B", with a fixed infinite type context called "Gamma_infinity".