Nominal Type Theory by Nullary Internal Parametricity
For researchers in programming languages and type theory, this provides a new foundation for nominal frameworks that unifies previously separate approaches.
This work shows that nominal features like pattern matching on name abstractions are recovered in a type theory combining nullary internal parametricity, a type of names with a novel induction principle, and nominal data types. The resulting framework supports both universal and existential name abstractions, freshness types, and restricted name swapping.
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, has a closed induction principle and is well-behaved w.r.t. weakening. It is known that name abstraction types can be presented either as an existential or as a universal quantification on names. Existential name abstractions support matching on name-binding patterns but have cumbersome typing rules; universal ones have clean rules but apparently no such nominal matching. In this work we show that this matching ability and other nominal features 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 type theory is a legitimate nominal framework: it has universal and (non-primitive) existential name abstractions, a freshness type former, restricted name swapping and local-scope operations. Nominal pattern matching is recovered via term-relevant nullary parametricity. We provide an example involving synthetic Kripke parametricity.