强类型玩具函数式语言中Hindley Milner互递归函数类型推断问题

这个问题绝对是Hindley-Milner（HM）类型推断里处理函数式语言的经典坑——当你碰到f和g这种互相调用的互递归函数时，常规的“先定义、后检查”的线性流程直接失效了。不过别担心，业界已经有成熟的处理方案，核心思路就是先占位、再收集约束、最后统一求解，下面我一步步给你拆解：

1. 识别互递归组，给所有成员分配类型占位符 #

首先你得先做一轮依赖分析：遍历所有函数定义，找出哪些函数互相引用，形成一个“连通分量”（也就是互递归组）。比如f调用g，g又调用f，那它们俩就是一个组；如果还有h调用f，但f不调用h，那h不属于这个组。

对每个互递归组里的函数，不管它们的定义顺序，先给每个函数分配一个新鲜的未知类型变量作为占位符。比如给f分配α，g分配β，相当于告诉类型检查器：“这些函数存在，它们的类型暂时未知，后面会确定”。

2. 批量收集所有互递归函数的类型约束 #

有了占位符之后，就可以同时对组内每个函数的体进行类型检查了。这时候遇到对组内其他函数的引用，直接用之前分配的占位符类型来生成约束：

• 检查f的函数体时，遇到调用g，就用g的占位符β来推导约束（比如g接收一个Int参数，那就能得到β ~ Int -> τ，其中τ是g的返回类型）；
• 检查g的函数体时，遇到调用f，就用f的占位符α来推导约束（比如f返回一个Bool，那就能得到α ~ σ -> Bool，其中σ是f的参数类型）。

举个具体的代码例子：

f x = if x then g 0 else True
g y = f (y > 5)

• 给f分配α，g分配β；
• 检查f：x必须是Bool（因为if的条件是布尔值），所以α的输入是Bool；g 0的类型要和True（Bool）一致，所以β Int ~ Bool → β = Int -> Bool；f的返回值是Bool，所以α = Bool -> Bool；
• 检查g：y > 5的类型是Bool，所以f的输入是Bool（和之前的约束一致）；g的返回值是f的返回值Bool，所以β = Int -> Bool（也和之前一致）。

3. 统一求解约束集，得到最终类型 #

把所有从互递归函数体里收集到的约束放在一起，用HM的**合一算法（unification）**来求解。如果约束之间没有矛盾，就能得到每个函数的具体类型；如果有矛盾（比如f要求g是Int->Bool，但g要求f是String->Int），就抛出类型错误。

比如上面的例子，约束集是α ~ Bool->Bool、β ~ Int->Bool，合一后直接得到：

• f : Bool -> Bool
• g : Int -> Bool

额外的实现小贴士 #

• 语法层面可以加标记：很多函数式语言（比如ML、OCaml）用let rec块来标记互递归函数，这其实是给类型检查器递信号：“这些函数是互递归的，按组处理”。你的玩具语言也可以借鉴这个设计，这样就不用自己做复杂的依赖分析，用户明确指定互递归组，实现起来更简单。
• 注意类型变量的作用域：分配占位符时要确保是新鲜的、未被使用过的类型变量，避免和函数体内的局部类型变量冲突，不然会导致合一错误。

如果你在具体实现合一算法、依赖分析或者处理多参数函数的约束时碰到细节问题，随时可以再细化提问～

内容的提问来源于stack exchange，提问作者suhdonghwi