Dualizing Generalized Algebraic Data Types by Matrix Transposition
Dualizing Generalized Algebraic Data Types by Matrix Transposition
复制标题
通过矩阵转置对偶广义代数数据类型
DOI：
10.1007/978-3-319-89884-1_3
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Julian Jabs
中科院分区：
文献类型：
--
作者：
Klaus Ostermann;Julian Jabs
我们描述了在构造函数上具有模式匹配的广义代数数据类型（GADTs）和在析构函数上具有模式匹配的广义代数协数据类型（GAcoDTs）之间的关系：gadt可以通过再功能化机械地转换为gacodt， gacodt可以通过去功能化机械地转换为gadt，去功能化和再功能化都对应于矩阵的转置，其中（共）数据类型的每个构造函数/析构函数对的方程都被组织起来。我们已经定义了一个微积分，它以这样一种方式统一了gadt和gacodt，即gadt和gacodt仅仅是划分程序的不同方式。我们在Coq证明助手中形式化了类型系统和操作语义，并对以下结果进行了机械验证：(1)类型系统是健全的，(2)去功能化和再功能化可以将gadt转换为gacodt，(3)这两种转换都是类型和语义保持的，并且彼此相反，(4)（共）数据类型可以用矩阵表示，上述转换对应于矩阵转置，(5)gadt可以以对偶方式扩展到gacodt；由此厘清民俗学关于“表达问题”的知识。我们相信，这种关系的识别可以指导未来的语言设计对数据和协数据的“双重特性”。
We characterize the relation between generalized algebraic datatypes (GADTs) with pattern matching on their constructors one hand, and generalized algebraic co-datatypes (GAcoDTs) with copattern matching on their destructors on the other hand: GADTs can be converted mechanically to GAcoDTs by refunctionalization, GAcoDTs can be converted mechanically to GADTs by defunctionalization, and both defunctionalization and refunctionalization correspond to a transposition of the matrix in which the equations for each constructor/destructor pair of the (co-)datatype are organized. We have defined a calculus,, which unifies GADTs and GAcoDTs in such a way that GADTs and GAcoDTs are merely different ways to partition the program.We have formalized the type system and operational semantics ofin the Coq proof assistant and have mechanically verified the following results: (1) The type system ofis sound, (2) defunctionalization and refunctionalization can translate GADTs to GAcoDTs and back, (3) both transformations are type- and semantics-preserving and are inverses of each other, (4) (co-)datatypes can be represented by matrices in such a way the aforementioned transformations correspond to matrix transposition, (5) GADTs are extensible in an exactly dual way to GAcoDTs; we thereby clarify folklore knowledge about the “expression problem”.We believe that the identification of this relationship can guide future language design of “dual features” for data and codata.
登录
查看更多内容
具有共同模式的有根据的递归：终止和生产力的统一方法
DOI：
--
发表时间：
2013
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Andreas Abel;B. Pientka
通讯作者：
B. Pientka
用户定义的类型和过程数据结构作为数据抽象的补充方法
DOI：
--
发表时间：
1994
期刊：
影响因子：
--
作者：
J. C. Reynolds
通讯作者：
J. C. Reynolds
GADT 的主要类型推断
DOI：
10.1145/2837614.2837665
发表时间：
2016
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Sheng Chen;Martin Erwig
通讯作者：
Martin Erwig
DOI：
--
发表时间：
2006
期刊：
European Conference on Object-Oriented Programming
影响因子：
--
作者：
B. Emir;A. Kennedy;Claudio V. Russo;Dachuan Yu
通讯作者：
Dachuan Yu
编程语言的二元性
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
Martin Hirzel;P. Nagpurkar
通讯作者：
P. Nagpurkar