为什么 OCaml 在包含通用值时会在首次使用时修改值的类型？

Question

为什么OCaml在包含通用值时更改首次使用值的类型？例如，如果我们为元组定义 Church 编码，我们有：

# let pair x y z = z x y;;
val pair : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>
# let first p = p (fun x y-> x);;
val first : (('a -> 'b -> 'a) -> 'c) -> 'c = <fun>
# let second p = p (fun x y -> y);;
val second : (('a -> 'b -> 'b) -> 'c) -> 'c = <fun>
# let foo = pair 1.2 "bob";;
val foo : (float -> string -> '_a) -> '_a = <fun>
# first foo;;
- : float = 1.2
# foo;;
- : (float -> string -> float) -> float = <fun>
# second foo;;
Error: This expression has type (float -> string -> float) -> float
       but an expression was expected of type
         (float -> string -> string) -> 'a
       Type float is not compatible with type string 
# let foo = pair 1.2 "bob";;
val foo : (float -> string -> '_a) -> '_a = <fun>
# second foo;;
- : string = "bob"
# foo;;
- : (float -> string -> string) -> string = <fun>
# first foo;;
Error: This expression has type (float -> string -> string) -> string
       but an expression was expected of type
         (float -> string -> float) -> 'a
       Type string is not compatible with type float

基本上，foo 的类型为 val foo : (float -> string -> '_a) -> '_a = <fun>，但这会在我们第一次投影出第一个或第二个元素时发生变化。为什么会这样？

Answer 1

这称为弱多态类型。对此提出并回答了很多问题。随意使用 SO 搜索工具或阅读 OCaml FAQ。但简而言之，这是由于值限制，通常在您具有部分应用程序或可变值时发挥作用。在前一种情况下，您可以使用所谓的 eta 表达式（通俗地说，通过用正常函数调用替换部分应用程序）来增强您的类型。后一种情况，什么也做不了。

Answer 2

正如@ivg所说，这是价值限制。如果你使用 eta 扩展，事情是这样的：

# let pair x y z = z x y;;
val pair : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>
# let first p = p (fun x y -> x);;
val first : (('a -> 'b -> 'a) -> 'c) -> 'c = <fun>
# let second p = p (fun x y -> y);;
val second : (('a -> 'b -> 'b) -> 'c) -> 'c = <fun>
# let foo x = pair 1.2 "bob" x;;
val foo : (float -> string -> 'a) -> 'a = <fun>
# first foo;;
- : float = 1.2
# second foo;;
- : string = "bob"

为什么 OCaml 在包含通用值时会在首次使用时修改值的类型？

Why does OCaml modify the type of a value on first use when it contains a universal?

ocaml