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.

翻译：表示带有绑定器的语言语法有多种方式。其中，名义框架是一种元语言，它特别包含名称抽象类型，可用于指定绑定器的类型。由此产生的语法表示——名义数据类型——使得阿尔法等价项相等，具有封闭的归纳原理，并且在弱化方面表现良好。已知名称抽象类型既可以表示为名称上的存在量化，也可以表示为全称量化。存在名称抽象支持名称绑定模式的匹配，但具有繁琐的类型规则；全称名称抽象具有简洁的规则，但显然不支持这种名义匹配。在本文中，我们展示了这种匹配能力及其他名义特征可以在包含以下内容的类型理论中恢复：(1) 空元（0-元）内部参数化类型理论（空元 PTT），(2) 名称类型及一种新颖的名称归纳原理，(3) 名义数据类型。该类型理论是一个合法的名义框架：它拥有全称和（非原始的）存在名称抽象、新鲜类型构造子、限制性名称交换以及局部作用域操作。名义模式匹配通过项相关的空元参数化得以恢复。我们提供了一个涉及综合克里普克参数化的示例。