Ornamental Algebras, Algebraic Ornaments
Ornamental Algebras, Algebraic Ornaments
复制标题
装饰代数、代数装饰品
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
J. Coetzee
中科院分区：
文献类型：
--
作者：
N. Gumede;A. Young;J. Coetzee
本文重新研究了依赖类型语言中数据类型的表示，特别是解决了这样一个问题：一种数据类型以各种方式比另一种数据类型提供更多信息意味着什么。非正式的人类观察，如“列表是带有额外装饰的自然数”和“向量是按长度索引的列表”，都是用一流的装饰语言表达的--基于普通旧类型的奇特新类型的呈现--既包括装饰，也包括在Tim Freeman和Frank Pfenning(1991)意义上的精炼。每个装饰品都增加了信息，所以它有一个从花哨的数据到简单的数据的遗忘功能，可以表达为它的装饰性代数的折叠：由数字建立的列表获得了“长度”代数。相反，数据类型的每个代数都归纳出一种索引该数据类型的方法--一个代数装饰。列表的长度代数导致聚合依赖向量类型的构造。因此，依赖类型不仅为数据结构提供了一个新的“多样性轴”--索引，而且还提供了管理和利用这种多样性的新抽象。在“新规划”(McBride&McKinna，2004)的精神下，重合工程被结果的传播所取代。
This paper re-examines the presentation of datatypes in dependently typed languages, addressing in particular the issue of what it means for one datatype to be in various ways more informative than another. Informal human observations like ‘lists are natural numbers with extra decoration’ and ‘vectors are lists indexed by length’ are expressed in a first class language of ornaments — presentations of fancy new types based on plain old ones — encompassing both decoration and, in the sense of Tim Freeman and Frank Pfenning (1991), refinement. Each ornament adds information, so it comes with a forgetful function from fancy data back to plain, expressible as the fold of its ornamental algebra: lists built from numbers acquire the ‘length’ algebra. Conversely, each algebra for a datatype induces a way to index it — an algebraic ornament. The length algebra for lists induces the construction of the paradigmatic dependent vector types. Dependent types thus provide not only a new ‘axis of diversity’ — indexing — for data structures, but also new abstractions to manage and exploit that diversity. In the spirit of ‘the new programming’ (McBride & McKinna, 2004), the engineering of coincidence is replaced by the propagation of consequence.