程序语言中的共归纳数据类型及其应用

Coinductive Data Types and their Applications in Programming Languages

归纳数据类型利用代数方法从构造的角度归纳地描述数据类型的有限语法结构,但在描述动态行为方面存在一定的不足。作为归纳数据类型的范畴对偶概念,共归纳数据类型利用共代数方法从观察的角度共归纳地描述了数据类型的动态行为。首先,从范畴论和代数的角度给出程序语言中的归纳数据类型定义,并分析了相应的递归操作;接着,利用共代数给出共归纳数据类型的范畴论定义,并根据共归纳数据类型的终结性分析了相应的共递归操作;最后,指出如何利用λ-双代数及分配律将归纳与共归纳数据类型有机地融合起来,探讨数据类型的语法构造与动态行为关系。

Inductive data types mainly focus on the finite syntactic structures inductively in terms of algebras from the construction perspective,but have some disadvantages in describing dynamic behaviors.As their categorical dual notions,coinductive data types aim to coinductively describe the observable behaviors of data types in terms of coalgebras from the observation perspective.We firstly gave the definitions of inductive data types in programming languages from the categorical and algebraic viewpoints.After that,we continued to present the definition of coinductive data types with coalgebras and analyze the corresponding corecursion operations according to the finality of coinductive data types.Finally,we pointed out how to use λ-bialgebras and distributive laws to combine inductive and coinductive data types and discuss the relations between syntactic constructions and dynamic behaviors of data types.