A Relationally Parametric Model of Dependent Type Theory
A Relationally Parametric Model of Dependent Type Theory
复制标题
DOI：
10.1145/2535838.2535852
复制
发表时间：
2014-01-01
影响因子：
--
通讯作者：
Johann, Patricia
中科院分区：
文献类型：
--
作者：
Atkey, Robert;Ghani, Neil;Johann, Patricia
雷诺兹的关系参数理论抓住了多态类型程序在数据表示变化下的不变性。Reynolds的原始工作利用了多态类型λ演算系统F的类型原则，但现在有相当大的兴趣将关系参数扩展到比系统F更丰富和更具表现力的类型系统。本文构建了谓词和非谓词依赖类型理论的参数模型。我们的模型具有双重意义。首先，在不可预变量中，我们能够推导出所有索引函子的初始代数的存在性。据我们所知，我们的是第一个关于依赖类型的参数化的解释，它能够将F系统参数模型中初始代数存在的有用演绎提升到依赖类型的设置。其次，我们的模型通过用自反图统一表达依赖类型的关系参数来提供概念清晰度，这使我们能够统一类型和种类的解释，而不是将类型的关系解释作为原始概念。用自反图来表达我们的模型，确保了它对依赖类型理论的标准类型构造函数的解释有规范的选择，除了对小类型的解释，在小类型的解释中，我们为关系参数制定了一个精致的解释。此外，我们的自反图模型为关系参数化的推广打开了大门，例如高维关系参数化。
Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F.This paper constructs parametric models of predicative and impredicative dependent type theory. The significance of our models is twofold. Firstly, in the impredicative variant we are able to deduce the existence of initial algebras for all indexed functors. To our knowledge, ours is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric models of System F to the dependently typed setting. Secondly, our models offer conceptual clarity by uniformly expressing relational parametricity for dependent types in terms of reflexive graphs, which allows us to unify the interpretations of types and kinds, instead of taking the relational interpretation of types as a primitive notion. Expressing our model in terms of reflexive graphs ensures that it has canonical choices for the interpretations of the standard type constructors of dependent type theory, except for the interpretation of the universe of small types, where we formulate a refined interpretation tailored for relational parametricity. Moreover, our reflexive graph model opens the door to generalisations of relational parametricity, for example to higher-dimensional relational parametricity.