You need to enable JavaScript to run this app.
优惠活动
大模型
产品
解决方案
定价
更多

基于Hindley-Milner算法的类型推断:如何为递归函数推断类型?

HM算法中递归/相互递归的类型推断实现方案

要解决你遇到的两类场景冲突,核心是基于依赖图强连通分量的绑定分组策略,配合HM标准的泛型推广、类型实例化机制,既不需要全模块一次性推导,也不会在相互递归场景缺失类型信息。

1. 为什么两种极端做法都行不通

  • 逐个顺序推导绑定的问题:遇到f = g/g = f这类相互递归场景时,推导f的时候g还没有进入类型环境,推导g的时候f还没有进入环境,收集不到完整的类型约束,无法得到正确的类型。
  • 全模块一次性统一求解约束的问题:没有区分“泛型签名的延迟实例化”和“单态约束的即时统一”,会把本该可以独立实例化的泛型函数,被不同调用点的具体类型强行约束,比如把h :: forall a. a -> Int被h 0和h "str"的约束统一成Int = String的假错误。

2. 核心实现步骤

第一步:给所有绑定划分递归分组

首先遍历模块里所有的顶层绑定,构建有向依赖图:

  • 图的节点是每个顶层绑定的名称
  • 如果绑定A的定义里引用了绑定B,就画一条从A指向B的边
  • 对这个依赖图做强连通分量(SCC)分解,每个独立的SCC就是一个需要单独处理的绑定组
  • 把所有SCC按照拓扑序排序:被依赖越靠底层的SCC,越先被处理

举两个例子的分组结果:

  • 互相递归的f = g/g = f:f指向g,g指向f,二者属于同一个SCC,作为递归组一起处理
  • f = h 0/g = h "str"/h _ = 0:f指向h,g指向h,h没有指向任何其他绑定,三个节点分属三个独立的SCC,拓扑排序后先处理h所在的SCC,再处理f和g的SCC

这种分组方式从根源上避免了把无递归依赖的绑定强行塞进同一个求解流程的问题。

第二步:按组完成类型推导

对每个SCC组内的绑定,按递归组的流程处理:

  1. 给组内的每个绑定生成一个全新的、未绑定的占位类型变量
  2. 把这些占位变量作为绑定的临时签名,全部加入当前的类型环境(也就是外层已经处理完的SCC提供的带泛型签名的绑定集合)
  3. 依次推导组内每个绑定的定义表达式,收集所有类型约束:
    • 表达式里如果引用了外层环境的绑定,对带forall量化的泛型签名,每次引用都要把量化变量替换成全新的自由类型变量(实例化),避免不同调用点的约束互相干扰
    • 表达式和绑定的临时占位类型做匹配,收集所有需要统一的等式约束
  4. 对收集到的所有约束做统一求解(Robinson归一算法),得到每个占位类型变量对应的实际类型
  5. 对每个绑定的实际类型做泛型推广:把类型中不依赖外层环境的自由类型变量,绑定为forall量化的泛型变量
  6. 把这些带正式泛型签名的绑定,替换掉之前的临时占位,加入外层类型环境,再处理下一个拓扑序的SCC

3. 两个典型场景的实际推导流程

  • 相互递归场景(f = g/g = f):
    1. 二者同属一个SCC,给f分配占位类型t_f,g分配占位类型t_g,加入临时环境
    2. 推导f的定义f = g:收集约束t_f = t_g
    3. 推导g的定义g = f:收集约束t_g = t_f
    4. 求解约束后得到t_f = t_g = a(未约束的自由变量)
    5. 泛化后两个绑定的签名都是forall a. a,推导完成
  • 泛型函数调用场景(f = h 0/g = h "str"/h _ = 0):
    1. 三个绑定分属三个独立SCC,先处理h的SCC:
      • 给h分配占位类型t_h,推导定义h _ = 0,收集约束t_h = a -> Int
      • 求解后泛化得到h的签名forall a. a -> Int,加入环境
    2. 处理f的SCC:
      • 推导表达式h 0时,把h的泛型签名实例化,把量化变量a替换成新的自由变量a1,得到临时类型a1 -> Int
      • 匹配参数0(类型Int),收集约束a1 = Int
      • 求解得到f的类型是Int
    3. 处理g的SCC:
      • 推导表达式h "str"时,把h的泛型签名重新实例化,把量化变量a替换成新的自由变量a2,得到临时类型a2 -> Int
      • 匹配参数"str"(类型String),收集约束a2 = String
      • 求解得到g的类型是Int,全程没有跨调用点的类型冲突

4. 关键注意点

  • 不要把递归组的泛型推广提前到约束求解之前,否则会导致约束收集不完整
  • 泛型实例化必须是每次引用时重新生成全新的类型变量,不能复用之前实例化过的类型变量,否则会破坏泛型的多态性
  • 泛型推广的判定规则:只有不被外层环境引用的自由类型变量才能被量化,否则会导致作用域类型错误

内容的提问来源于stack exchange,提问作者Смирнов Илья

相关产品推荐
方舟 Agent Plan

超全模态模型 × Harness 升级,最新支持 Deepseek-V4.1-Flash、GLM-5.3 系列、Doubao-Seedream-5.0-pro、Kimi-K3 (部分), 限时 9.9 元起

最近更新时间:2026.10.23 20:57:04