types - OCaml 中的类型推断

Question

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

例如:

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

对我来说很有意义。 val f 接受一个函数 x，该函数接受 'a 类型的列表并返回 'b 类型的东西。然后 f 也返回一个 '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的类型:

1. 您知道 n 的类型为 'a，因此您也可以派生 (m n x) 具有类型 'a
2. 你知道 ls 有类型 'b list，所以你可以派生 x 有 输入'b
3. m 接受两个类型为 'a 和类型为 'b 的参数，并产生类型为 'a 的结果>。因此，m 的类型为 'a -> 'b -> 'a

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