Towards the type safety of Pure Subtype Systems (Full version)

TL;DR

This paper introduces Machine-Based PSS, a reformulation of Pure Subtype Systems that proves the crucial commutativity of reduction relations, thereby establishing type safety and advancing language design for dependent types.

Contribution

We present MPSS, a new formulation of PSS that enables a direct proof of reduction relation commutativity, solving a longstanding open problem in type safety proof.

Findings

Proves the commutativity of equivalence and subtyping reductions in MPSS

Establishes transitivity elimination for higher-order subtyping systems

Provides a pathway toward a fully type-safe PSS-based language

Abstract

Hutchins' Pure Subtype Systems (PSS) offer a unified framework for types and terms, promising significant advancements in language design for features like dependent types and higher-order subtyping. However, the theory has been hampered by a critical gap: a proof of type safety has remained an open problem for over a decade. The original attempt to prove this property relied on the conjectured commutativity of two fundamental reduction relations, equivalence and subtyping. Proving transitivity elimination, however, requires this commutativity, a property that is notoriously difficult to establish for higher-order subtyping systems. In this paper, we address this issue by introducing Machine-Based PSS (MPSS), a novel reformulation of the original system. MPSS integrates a continuation stack mechanism, reminiscent of the Krivine Abstract Machine, to keep track of arguments that are passed during function application, enabling more fine-grained reductions. This architectural change exposes crucial intermediate reduction steps that were absent in the original PSS. The primary contribution of our work is a direct proof that the equivalence and subtyping reductions in MPSS commute. This result formally establishes transitivity elimination, which is the cornerstone of the inversion lemma required for type safety. We conclude by outlining a pathway from our foundational result to a complete, type-safe system, thereby paving the way for the practical realization of PSS-based languages.