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

Inductive data types mainly focus on the finite syntactic structures inductively in terms of algebras from the construction perspective and have disadvantages in describing dynamic behavior. As its categorical dual notions, coinductive data types aim to coinductively describe the observable behavior of data types in terms of coalgebras from the observation perspective. Both of them are complementary to each other, which as a result can improve the abilities of behavioral description and verification of programming languages. In this paper, we firstly analyze inductive data types in programming languages from categorical and algebraic perspectives. After that, we continue to present the definition of coinductive data types with coalgebras and analyze the applications of coinductive principles. Finally, we point out how to use suitable distributive laws to combine inductive and coinductive data types.