针对归纳数据类型上的递归操作可能包含固定参数且产生计算副作用的问题,结合函数式程序语言中的monads及范畴论中的伴随关系给出monadic强归纳数据类型的定义及monadic强初始性的证明;在此基础上,进一步提出一种带固定参数且产生计算副作用的递归操作的定义,证明了它比一般的递归具有更好的抽象性和封装性,同时分析了相应的范畴论性质和计算律.
Aiming at the possible fixed parameters and computational side-effects of the recursive operations on inductive data types , the authors define the strong monadic inductive data type and presents proofs of strong monadic initiality by combining the notions of monads in functional programming languages with the adjoint in the category theory.Furthermore, we propose a kind of recursion with fixed parameters and computational side-effects.It is proved that this kind of recursion can provide better abstraction and encapsulation in comparison with normal recur -sions.Meanwhile, we discuss the corresponding categorical properties and calculation laws .