递归类型

普通有限类型只能描述固定深度的结构，递归类型把“剩余部分仍是同一种结构”写进类型本身。列表不是某个最大长度的嵌套积，而是“空，或一个元素加另一条列表”的方程。fold 和 unfold 像在抽象类型与展开一层的表示之间开关，iso-recursive 语义让每次展开都在程序中可见。方程可以描述良基数据、无限结构或负位置递归；选择最小/最大解释以及允许哪些出现位置，需要另行指定。

列表可写为

空表对应 fold(inl(unit))，非空表对应 fold(inr(a,xs))；每次模式匹配先 unfold 一层。二叉树可类似写成 $\mu X.1+A\times X\times X$。

边界是方程 $X=X$，它没有提供任何可观察构造，不能凭符号自动得到有用数据。某些演算允许 $\mu X.X\to A$ 一类负位置递归，并可能由此给自应用定型、破坏强正规化理路简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个良类型简单 λ 项都强正规化：任意完整 β-归约路径都在有限步后结束。；用于良基数据的严格正限制及反例分析见归纳类型，本页不把该限制强加给所有递归方程。

递归类型是链表、树、流、对象自引用和递归模块的核心表示。与和类型理路和类型Sum type · Variant type其值从若干带标签分支中选择一个的类型。、积类型理路积类型Product type其值由两个分量组成并支持投影的类型。组合可得到代数数据类型理路代数数据类型Algebraic data type · Algebraic datatype以有限构造子的和、每个构造子字段的积以及可选递归组合数据形状的类型。的常见方程；这项汇总不改变 fold/unfold 的递归类型核心。

在编译器中，显式 fold/unfold 帮助证明表示安全。证明助理通常改用严格正、最小生成的归纳类型，并由消去子与归纳原理理路消去子、递归子与归纳原理Eliminator · Recursor · Induction principle由归纳类型的构造器导出消费数据、定义递归函数和证明依赖性质的规则。消费有限构造数据；无限流等对象则需要最大不动点与共归纳观察。类型方程、归纳生成和共归纳生产性是相邻层次，不可仅凭同一个 $\mu$ 记号互换。

对闭合、可观察的equi-recursive类型，正则递归类型等价理路正则递归类型等价Regular recursive type equality · Equi-recursive type equality把有μ绑定的闭合类型压成有限构造图，检查相同无限展开并交出互模拟对集或有限区分路径，拒绝纯别名循环。把词法绑定压成有限构造图，交互模拟对集或有限区分路径；单周期与双周期可以等价，纯别名环则先按该接口拒绝。若问题改为一个递归接口能否替代另一个，递归结构子类型判定理路递归结构子类型判定Recursive structural subtyping · Equi-recursive subtyping algorithm在有限递归类型图上展开有方向的替代义务，以只读记录宽度和函数域逆变生成闭合证书，并返回带方向的有限失败路径。返回有方向的闭合义务，函数参数处必须交换两端。