When Is a Type Refinement an Inductive Type?
When Is a Type Refinement an Inductive Type?
复制标题
类型细化何时是归纳类型？
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Neil Ghani
中科院分区：
文献类型：
--
作者：
R. Atkey;Patricia Johann;Neil Ghani
依赖类型的编程语言允许在类型系统中表示数据的复杂属性。在依赖类型编程中特别使用的是通过计算上有用的信息来精炼数据的索引类型。例如，以n为索引的向量类型根据它们的长度来优化列表。其他数据类型可能以类似的方式进行细化，但是程序员必须在特定的基础上生成特定目的的细化，开发人员必须预测在库中包含哪些细化，并且实现通常存储有关数据及其细化的冗余信息。本文展示了如何一般地推导归纳类型的细化的归纳特征，并认为这些特征可以减轻与特定细化相关的一些上述困难。这些特征也确保了使用归纳类型进行编程和推理的标准技术适用于细化，并且细化本身可以进一步细化。
Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the N-indexed type of vectors refines lists by their lengths. Other data types may be refined in similar ways, but programmers must produce purposespecific refinements on an ad hoc basis, developers must anticipate which refinements to include in libraries, and implementations often store redundant information about data and their refinements. This paper shows how to generically derive inductive characterisations of refinements of inductive types, and argues that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. These characterisations also ensure that standard techniques for programming with and reasoning about inductive types are applicable to refinements, and that refinements can themselves be further refined.
轻柔的悬浮艺术
影响因子：
--
作者：
Chapman J
通讯作者：
Chapman J