范畴论框架下的共归纳数据类型可以看成是某个共代数函子下的终结共代数中的载体，针对该特点，结合范畴论给出程序语言中共归纳数据类型的共代数描述，并根据终结共代数的终结性给出相应的共递归操作的定义及其共代数计算定律; 同时，利用双函子及类型函子对参数化共归纳数据类型进行抽象描述，并结合自然转换给出类型函子上的单元和融合等计算定律，证明这些计算定律可用于简化共递归数据类型上的计算，从而提高程序语言对数据类型的动态行为描述能力．

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.