摘要：

As the coinductive data types in the framework of the category theory can be regarded as the carriers of final coalgebras for some coalgebraic functors,this paper presents the coalgebraic descriptions of the coinductive data types in programming languages from the viewpoint of the category theory and proposes the definitions and coalgebraic calculation laws of corecursion operations based on the finality of final coalgebras. Meanwhile,bifunctors and type functors are used to abstractly describe parametric coinductive data types,and such calculation laws on type functors as unit and fusion ones are put forward via natural transformations. It is proved that these laws can be used to simplify the calculations on coinductive data types,thus improving the dynamic behavior description ability of programming languages for various data types.

展开