ocaml - 在 OCaml 中键入推理帮助

Question

我将如何继续证明这两个函数的类型正确？我对这个问题有点迷茫。

  let rec reduce f lst u =
     match lst with
     | [] -> u
     | (h::t) -> f h (reduce f t u) 

 let rec forall2 p l1 l2 =
     match (l1,l2) with
     | ([],[]) -> true
     | ([],_) -> false
     | (_,[]) -> false
     | ((h1::t1),(h2::t2)) ->
          (p h1 h2) && (forall2 p t1 t2)

Answer 1

我不会给出一个成熟的解决方案，因为这个问题看起来像一个作业。

要自己进行类型推断，您所要做的就是查看来源并进行推断。然后，从你的推论中，推导出越来越多的类型，直到知道所有类型，或者直到你发现了差异。

为了让你开始：

• 在reduce中，您正在lst对 type 的模式进行模式匹配'a list。因此，lst必须键入为'a list。
• 每个模式之后的值必须具有相同的类型，因此u具有与 相同的类型f h (reduce f t u)。

等等等等等等...