Containers: Constructing strictly positive types
Containers: Constructing strictly positive types
复制标题
DOI：
10.1016/j.tcs.2005.06.002
复制
发表时间：
2005-09-06
影响因子：
1.1
通讯作者：
Ghani, N
中科院分区：
文献类型：
--
作者：
Abbott, M;Altenkirch, T;Ghani, N
我们介绍了Martin-lof类别的概念 - 本地笛卡尔封闭类别，具有不相交的共同体和容器函子的初始代数（W-types的分类类似物） - 然后确定我们称之为嵌套的严格积极的感应类型，我们称之为这些类型严格的积极类型，存在于任何马丁 - 洛夫类别中。我们的开发中的中分是容器和容器函子的概念。这些通过利用依赖类型理论作为定义Martin-Lof类别中的构造的一种方便方式来对数据结构和多态性函数进行新的概念分析。我们还表明，容器之间的形态可以充分而忠实地解释为多态性功能（即自然转化），并且在存在W型的情况下，所有严格的阳性类型（包括嵌套的电感和共同感应类型）都会引起容器。 （c）2005 Elsevier B.V.保留所有权利。
We introduce the notion of a Martin-Lof category-a locally cartesian closed category with disjoint coproducts and initial algebras of container functors (the categorical analogue of W-types)-and then establish that nested strictly positive inductive and coinductive types, which we call strictly positive types, exist in any Martin-Lof category.Central to our development are the notions of containers and container functors. These provide a new conceptual analysis of data structures and polymorphic functions by exploiting dependent type theory as a convenient way to define constructions in Martin-Lof categories. We also show that morphisms between containers can be full and faithfully interpreted as polymorphic functions (i.e. natural transformations) and that, in the presence of W-types, all strictly positive types (including nested inductive and coinductive types) give rise to containers. (c) 2005 Elsevier B.V. All rights reserved.