Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Valentin Pasquale, Álvaro García-Pérez

TL;DR

The paper tackles the open problem of type safety in Hutchins' Pure Subtype Systems (PSS) by introducing Machine-Based PSS (MPSS), a Krivine-like continuation-stack reformulation that reveals intermediate reductions. It provides a direct proof that equivalence and subtyping reductions commute, enabling transitivity elimination and the inversion lemma necessary for type safety. A concrete sketch shows how a type-safe system could be built atop MPSS, pending a conjecture about context-independent well-subtyping. Collectively, this work lays a principled foundation for unifying terms and types under a single subtype relation and points to concrete directions for defining and verifying a complete MPSS-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.

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

TL;DR

The paper tackles the open problem of type safety in Hutchins' Pure Subtype Systems (PSS) by introducing Machine-Based PSS (MPSS), a Krivine-like continuation-stack reformulation that reveals intermediate reductions. It provides a direct proof that equivalence and subtyping reductions commute, enabling transitivity elimination and the inversion lemma necessary for type safety. A concrete sketch shows how a type-safe system could be built atop MPSS, pending a conjecture about context-independent well-subtyping. Collectively, this work lays a principled foundation for unifying terms and types under a single subtype relation and points to concrete directions for defining and verifying a complete MPSS-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.
Paper Structure (8 sections, 7 theorems, 4 equations, 4 figures)

This paper contains 8 sections, 7 theorems, 4 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Machine-Based Pure Subtype Systems
  3. Transitivity elimination
  4. Towards a Type-Safe System
  5. Related work
  6. Future work
  7. Conclusion
  8. Theorems of the text

Key Result

Lemma 1

Let $\Gamma; s$ be an extended context. Let $t_0$, $t_1$, and $t_2$ be terms. If $\Gamma;s\vdash t_0\mathop{\stackrel{\equiv}{\longrightarrow}} t_1$ and $\Gamma;s\vdash t_0\mathop{\stackrel{\leq}{\longrightarrow}} t_2$, then for any extended context $\Gamma'; s'$ such that $\Gamma; s\rightarrowtail

Figures (4)

  • Figure 1: Prevalidity in MPSS
  • Figure 2: Equivalence and subtyping reduction in MPSS
  • Figure 3: Derivation of $\Gamma; \mathrm{nil} \vdash (\lambda x \,{\leq}\, A. x) \, a \leq \mathit{Unit} \, A \, a$
  • Figure 4: Well-subtyping in MPSS

Theorems & Definitions (8)

  • Lemma 1: $\mathop{\stackrel{\leq}{\longrightarrow}}$ and $\mathop{\stackrel{\equiv}{\longrightarrow}}$ strongly commute
  • Lemma 2: $\mathop{\stackrel{\equiv}{\longrightarrow}}$ has the diamond property
  • Theorem 3: Transitivity is admissible
  • Theorem 4: Progress
  • Theorem 5: Preservation
  • Lemma 6: Evaluation preserves well-formedness
  • Lemma 7: Substitution preserves well-formedness
  • Conjecture 8: Well-subtyping is context independent