types - 为什么函数参数在 Ocaml 中不能是多态的？

Question

假设我有以下功能:

let rejected f = (f 1, f "hi");;

它被类型检查器拒绝了，我真的不明白为什么类型检查器拒绝它。由于 f 可以是一个多态函数(例如 id)，并且类型检查器应该允许它。有人可以解释一下吗？

Answer 1

这是由于“let 多态性”，又名“prenex 多态性”，又名“ML 风格多态性”。搜索此术语将为您提供一些相关信息。

通俗地说，这就是类型推断的工作原理，有些时候你需要停止泛化，并修复你的类型变量。在 ML 风格的多态性中，这是在 let 级别上完成的。因此，let 绑定(bind)中的函数应该统一使用，即使用相同的参数。如果这对你来说是个问题，那么你可以使用记录、对象或(也许)语言的其他一些特性来克服它。这是 OCaml 的摘录 FAQ :

How to write a function with polymorphic arguments? In ML, an argument of a function cannot be polymorphic inside the body of the function; hence the following typing:

let f (g : 'a -> 'a) x y = g x, g y 
val f : ('a -> 'a) -> 'a -> 'a -> 'a * 'a = <fun> 

The function is not as polymorphic as we could have hoped. Nevertheless, in OCaml it is possible to use first-order polymorphism. For this, you can use either records or objects; in the case of records, you need to declare the type before using it in the function.

let f (o : <g : 'a. 'a -> 'a>) x y = o#g x, o#g y
type id = { g : 'a. 'a -> 'a; }
let f r x y = r.g x, r.g y