Nominal Type Theory by Nullary Internal Parametricity

TL;DR

This paper introduces a novel type theory that combines nullary internal parametricity with nominal data types, enabling pattern matching and name abstraction features in a unified framework for syntax with binders.

Contribution

It presents a new nullary parametric type theory with nominal data types, recovering pattern matching and name abstraction capabilities in a formal, type-theoretic setting.

Findings

Recovered nominal pattern matching in the type theory

Extended nullary PTT with name abstraction and freshness features

Illustrated use of nullary parametricity in syntax representation

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.