Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nominal Type Theory by Nullary Internal Parametricity

Antoine Van Muylder, Andreas Nuyts, Dominique Devriese

TL;DR

This work introduces nullary internally parametric type theory (nullary PTT) as a foundation for nominal dependent type theory, enabling universal name abstractions, nominal data types, and pattern matching within a cubical-type setting. It defines a first-class Nm type with a name-induction principle and establishes the Structure Abstraction Principle (SAP) to ensure parametricity translations commute with type formers, thereby recovering nominal pattern matching. The paper shows how key nominal primitives—existential/universal name quantification, typal freshness, name swapping, and locally scoped names—can be implemented in nullary PTT, and provides concrete examples including a pi-calculus datatype and a HOAS-inspired encoding linked to Kripke parametricity. By connecting nominal syntax to internal parametricity, the authors lay the groundwork for a practical nominal framework with a path toward implementation. The work also sketches semantic models and discusses how this approach relates to existing nominal theories and the transpension perspective.

Abstract

There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, which can be used to specify the type of binders. The resulting syntax representation (nominal data types) makes alpha-equivalent terms equal, and features a name-invariant induction principle. It is known that name abstraction types can be presented either as existential or universal quantification on names. On the one hand, nominal frameworks use the existential presentation for practical reasoning since the user is allowed to match on a name-term pattern where the name is bound in the term. However inference rules for existential name abstraction are cumbersome to specify/implement because they must keep track of information about free and bound names at the type level. On the other hand, universal name abstractions are easier to specify since they are treated not as pairs, but as functions consuming fresh names. Yet the ability to pattern match on such functions is seemingly lost. In this work we show that this ability and others are recovered in a type theory consisting of (1) nullary ($0$-ary) internally parametric type theory (nullary PTT) (2) a type of names and a novel name induction principle (3) nominal data types. This extension of nullary PTT can act as a legitimate nominal framework. Indeed it has universal name abstractions, nominal pattern matching, a freshness type former, name swapping and local-scope operations and (non primitive) existential name abstractions. We illustrate how term-relevant nullary parametricity is used to recover nominal pattern matching. Our main example involves synthetic Kripke parametricity.

Nominal Type Theory by Nullary Internal Parametricity

TL;DR

This work introduces nullary internally parametric type theory (nullary PTT) as a foundation for nominal dependent type theory, enabling universal name abstractions, nominal data types, and pattern matching within a cubical-type setting. It defines a first-class Nm type with a name-induction principle and establishes the Structure Abstraction Principle (SAP) to ensure parametricity translations commute with type formers, thereby recovering nominal pattern matching. The paper shows how key nominal primitives—existential/universal name quantification, typal freshness, name swapping, and locally scoped names—can be implemented in nullary PTT, and provides concrete examples including a pi-calculus datatype and a HOAS-inspired encoding linked to Kripke parametricity. By connecting nominal syntax to internal parametricity, the authors lay the groundwork for a practical nominal framework with a path toward implementation. The work also sketches semantic models and discusses how this approach relates to existing nominal theories and the transpension perspective.

Abstract

There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, which can be used to specify the type of binders. The resulting syntax representation (nominal data types) makes alpha-equivalent terms equal, and features a name-invariant induction principle. It is known that name abstraction types can be presented either as existential or universal quantification on names. On the one hand, nominal frameworks use the existential presentation for practical reasoning since the user is allowed to match on a name-term pattern where the name is bound in the term. However inference rules for existential name abstraction are cumbersome to specify/implement because they must keep track of information about free and bound names at the type level. On the other hand, universal name abstractions are easier to specify since they are treated not as pairs, but as functions consuming fresh names. Yet the ability to pattern match on such functions is seemingly lost. In this work we show that this ability and others are recovered in a type theory consisting of (1) nullary (-ary) internally parametric type theory (nullary PTT) (2) a type of names and a novel name induction principle (3) nominal data types. This extension of nullary PTT can act as a legitimate nominal framework. Indeed it has universal name abstractions, nominal pattern matching, a freshness type former, name swapping and local-scope operations and (non primitive) existential name abstractions. We illustrate how term-relevant nullary parametricity is used to recover nominal pattern matching. Our main example involves synthetic Kripke parametricity.

Paper Structure

This paper contains 18 sections, 2 theorems, 16 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Nullary PTT
  3. Nullary CH
  4. The $\mathsf{Nm}$ type, name induction, nominal data types
  5. The Structure Abstraction Principle (SAP)
  6. Semantics, Soundness and Computation
  7. Nominal Primitives for Free
  8. Universal name quantification
  9. Typal freshness
  10. Existential name quantification
  11. Swapping names
  12. Locally scoped names
  13. Nominal Pattern Matching
  14. Patterns that bind
  15. A HOAS Example by term-relevant parametricity
  16. ...and 3 more sections

Key Result

Theorem 1

We have $\mathsf{mbump}_j : (@\mathsf{N} \multimap \mathsf{HMod}_j) \simeq \mathsf{HMod}_{j+1}$, $\mathsf{nbump}_j : (@\mathsf{N} \multimap \mathsf{NMod}_j) \simeq \mathsf{NMod}_{j+1}$, $\mathsf{ebump}_j : (@\mathsf{N} \multimap \mathsf{HEnc}_j) \simeq \mathsf{HEnc}_{j+1}$ and $\mathsf{lbump}_j : (@

Figures (2)

  • Figure 1: The Bridge and Path type former commute with some example type formers.
  • Figure 2: Parametricity fragment of the CH theory DBLP:journals/lmcs/CavalloH21 where we replace the arity by $0$, and novel rules for the interval $\mathsf{Nm}$. For binding rules such as ext, we rely on the invertibility of both variable and name abstraction to bind using $\lambda$.

Theorems & Definitions (2)

  • Theorem 1
  • Lemma 2