OCaml中的键入推理帮助

问题描述：

我将如何继续证明这两个函数的输入是否正确？我对这个问题有点失落。OCaml中的键入推理帮助

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)

你说的 “证明使用类型推断功能” 是什么意思？你有任务来证明这些功能是手工打印的吗？ – camlspotter

是的，我需要证明他们是否打得很好，但我很难从哪里开始，或者需要一个例子来解决问题。 – user3460123

从基础案例和已知类型开始，然后从那里往回走。 – glennsl

答

因为这个问题看起来像一个任务，我不会给一个完全成熟的解决方案。

要自己做类型推理，你所要做的就是查看源代码并作出扣除。然后，从你的推论中，推断出越来越多的类型，直到所有类型都是已知的，或者直到你找到了差异。

为了让你开始：

在reduce，你的模式匹配lst对'a list型的模式。因此，lst必须键入为'a list。
每个图案之后的值必须具有相同的类型，因此u与f h (reduce f t u)具有相同的类型。

的Etcætera等cætera...

OCaml中的键入推理帮助

相关推荐