OCaml类型错误：期望(string * terme) list却得到((terme->terme)*(terme->terme)) list

错误根源 #

错误出现在unif函数处理变量与项匹配的分支中：

• 环境e的类型是(string * terme) list，每个元素是变量名到项的绑定
• 原代码里的List.map处理把绑定的key（string类型的变量名）当成terme传入sub函数，直接触发类型不兼容；你后来的修改方向对，但漏传了sub的一个参数——sub是柯里化的三元函数，需要传入「要替换的变量名」「替换目标项」「被替换的项」三个参数。

修正后的代码 #

type terme =
  | Var of string
  | Sym of string
  | Func of terme * terme

exception Echec

let rec sub v t = function 
  | Var v' when v = v' -> t
  | Func (t1, t2) -> Func (sub v t t1, sub v t t2)
  | t -> t

let rec occ_check v = function
  | Var v' when v'=v -> true
  | Func (t1,t2) -> occ_check v t1 || occ_check v t2
  | _ -> false

let rec unif e (t1, t2) =
  match (t1, t2) with
  | Var v1, Var v2 when v1 = v2 -> e
  | Var v, t | t, Var v ->
      if List.mem_assoc v e then unif e (List.assoc v e, t)
      else if occ_check v t then raise Echec
      // 核心修正：对环境中每个绑定的项执行替换，变量名保持不变
      else (v, t) :: List.map (fun (s, t') -> (s, sub v t t')) e
  | Func (f1, a1), Func (f2, a2) ->
      let e' = unif e (f1, f2) in
      unif e' (a1, a2)
  | Sym s1, Sym s2 when s1 = s2 -> e
  | _ -> raise Echec

修正说明 #

• List.map的lambda函数正确遍历环境中的每个(s, t')绑定：
  • 变量名s保持不变（我们只修改绑定的项，不改动绑定的变量名）
  • 对绑定的项t'调用sub v t t'，把t'中所有的变量v替换为t，保证环境中所有绑定的一致性

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