OCaml 中的类型推断

Question

我正在努力思考 OCaml 的类型推断符号。

例如：

# let f x = x [];; 
val f : ('a list -> 'b) -> 'b = <fun>

对我来说很有意义。 val f 接受一个函数 x，该函数接受 'a 类型和 returns 某种 'b 类型的列表。然后 f returns a 'b 类型也是如此，因为它只调用 x。

然而，一旦我们得到更多的争论，我就会更加困惑。

# let g a b c = a b c;;
val g : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>

我可以假设如果函数有参数，那么类型推断的第一个参数将始终是参数吗？如果我调用 a b c，顺序是 ((a b) c) 还是 (a (b c))？

# let rec h m n ls = match ls with
  | [] -> n
  | x::t -> h m (m n x) t;;
val h : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = <fun>

至于这个，我对 ('a -> 'b -> 'a) -> 'a 的派生方式感到困惑。可以看到'b列表对应ls变量，最后一个'a对应终端符号n的类型

Answer 1

Can I assume that if the function has arguments, then the first parameters of the type inference will always be the arguments?

是的，函数类型的第一个参数是它的第一个参数的类型。

And if I call a b c, is the order ((a b) c) or (a (b c))?

顺序是((a b) c)（你可以这么简单的想）

As for this one I'm confused as to how ('a -> 'b -> 'a) -> 'a was derived. I can see that 'b list corresponds to the ls variable and the last 'a corresponds to the type of the terminal symbol n.

你是对的。 ls 的类型为 'b list，n 的类型为 'a.

让我们考虑一下m的类型：

你知道 n 有类型 'a，所以你也可以派生 (m n x) 类型为 'a
你知道 ls 有类型 'b list，所以你可以导出 x 有输入 'b
m 接受类型 'a 和类型 'b 的两个参数，并产生类型 'a 的结果。所以，m 的类型是 'a -> 'b -> 'a

因此，整个函数的类型为 ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a

OCaml 中的类型推断

Type Inference in OCaml

types

functional-programming

ocaml

ml