形式陈述

递归类型把类型变量在自身定义中再次出现，常写为

$$ \mu\alpha.\,T(\alpha). $$$$\mu \alpha .T(\alpha ).$$

在等递归解释中，$\mu\alpha.T$$\mu \alpha .T$ 与 $T(\mu\alpha.T)$$T(\mu \alpha .T)$ 按定义相等；在同构递归解释中，两者仅由显式的 $\operatorname{fold}$$\mathrm{fold}$ 与 $\operatorname{unfold}$$\mathrm{unfold}$ 构成同构，并满足相应计算规则。例如列表可写为 $\mu\alpha.\,1+(A\times\alpha)$$\mu \alpha .1+(A\times \alpha )$。具体系统常要求守卫性、正性或其他良构条件，以维持类型检查、归纳原理或归一化性质。

直觉

递归类型为“数据中还包含同种数据”的形状求一个类型方程不动点；fold 把展开的一层封装回来，unfold 则观察一层结构。

例子与边界

二叉树可表示为 $\mu\alpha.\,1+(A\times\alpha\times\alpha)$$\mu \alpha .1+(A\times \alpha \times \alpha )$。等递归系统中编译器隐式识别展开，使用方便但类型等价判定更复杂；同构递归系统把边界写入程序。无限展开只是理解图像，不是要求运行时实际构造无限值。允许任意负位置递归或把一般递归混入逻辑时，可能破坏强归一化与一致性。

推论与应用

递归类型支持列表、树、对象编码、循环数据结构和递归模块。其不动点视角连接域论、代数数据类型与余代数数据类型，也要求区分有限归纳数据和潜在无限的余递归数据。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 20–21, iso-recursive and equi-recursive types。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Ch. 16, recursive types。