多态递归

递归经常让问题规模变小，但“变小”不一定保持元素类型原封不动。一种非规则数据结构把相邻两个元素先配成一对，再把这些对子作为下一层的元素。向下递归时结构更浅，元素类型却从a变成a×a。

多态递归给函数一个承诺：无论这一层的元素类型是什么，都能处理。每走下一层，重新使用这个承诺，而不是强迫所有层共用同一个元素类型。

非规则Perfect类型 ​

定义代数数据类型公理库代数数据类型Algebraic data type · Algebraic datatype以有限构造子的和、每个构造子字段的积以及可选递归组合数据形状的类型。

data Perfect a = Leaf a | Node (Perfect (a × a))

构造器签名为

Node的递归参数不是Perfect a，而是Perfect(a×a)，所以该类型不是保持参数不变的规则递归类型。定义深度：

depth : ∀a. Perfect a → Int
depth (Leaf _) = 0
depth (Node t) = 1 + depth t

逐分支检查时，设外层任意类型为刚性α。

• 输入是Perfect α，Leaf分支得到元素α；返回0具有Int类型
• Node分支得到 $t:\mathrm{Perfect}(\alpha \times \alpha )$
• 递归使用depth时，把其独立量化的a实例化为α×α，得到 $\mathrm{Perfect}(\alpha \times \alpha )\to \mathrm{Int}$
• 所以 depth t:Int，加一仍为Int；外层α没有被改写

递归调用实例化的是f方案里的绑定变量，绝不是把当前外层α解成α×α。

单态递归假设为何失败 ​

若先假设 $depth:\mathrm{Perfect}(\beta )\to \mathrm{Int}$，而递归体的所有出现共享这一个β，那么Node分支要求

在有限类型树的一阶合一公理库一阶统一First-order unification · Syntactic unification寻找使若干一阶项在替换后相等的最一般替换。中，β出现在右侧内部，occurs check拒绝。这次失败不是发现程序会在运行时出错，而是指出单态递归假设太窄。已给定全称签名的检查不需要这个方程。

单写 depth:Perfect a→Int、却把a解释为一个待求解变量，也不等于显式声明 $\mathrm{\forall }a$。是否带量词、量词在哪里生效，是检查器需要的实质信息。

一条有具体类型的执行 ​

取

t = Node (Node (Leaf ((1,2),(3,4))))

最内层Leaf的元素类型是 $(\mathrm{Int}\times \mathrm{Int})\times (\mathrm{Int}\times \mathrm{Int})$。内层Node把它收成Perfect(Int×Int)，外层Node再收成Perfect Int。执行为

三次调用的元素参数依次为Int、Int×Int、(Int×Int)×(Int×Int)，结果类型一直是Int。递归沿一个真正的子结构前进，所以这个depth还可以独立证明终止；多态递归规则本身并不保证所有递归定义终止。

多态递归常见于嵌套数据类型、类型化语法树及携带不同索引实例的遍历。程序员给出一个对各层统一成立的接口，检查器在每次递归使用时选择合适实例。

不带注解的一般多态递归类型推断不可判定；这不是说任何具体程序都无法检查，也不是说必须进行运行时类型测试。实践中常要求递归签名，再在明确的系统限制下检查定义体。与完全自动的HM主类型推断相比，责任从“算法猜出最一般接口”转成“程序员提供接口，算法验证每个分支”。

本例提供了一个可重复诊断方法：先列出递归实参类型，再问它是否必须与外层实参共享同一实例。若结构递归使类型参数由a变成a×a，强行共享会生成自包含方程；若参数始终不变，普通单态递归往往足够。不能见到任何occurs-check失败都归因于需要多态递归，例如自应用 x x在别的假设下仍可能真正无类型。