OCaml 中的 eta 扩展万无一失吗？

Question

在 OCaml 中，最好始终将 eta 扩展作为万无一失的经验法则吗？

  type 'x recordx = { x : int }
  type 'y recordy = { y : int }

  let rec ok : type n a. n recordx -> a recordy -> int =
   fun algebrah x -> ok algebrah x

  let rec ok : type a. a recordy -> int =
   fun x ->
    let go : type b. b recordy -> int = ok in
    go x

  let rec ok : type n a. n recordx -> a recordy -> int =
   fun x y ->
    let go : type b. b recordy -> int = fun y -> ok x y in
    go y

  let rec ok : type n a. n recordx -> a recordy -> int =
   fun x y ->
    let go = ok x in
    go y

  (* This definition has type 
          'b recordy -> int which is less general than
    'b0. 'b0 recordy -> int 
  *)
  let rec ko : type n a. n recordx -> a recordy -> int =
   fun x y ->
    let go : type b. b recordy -> int = ko x in
    go y

Answer 1

放宽的值限制将 eta 扩展形式分类fun y -> f x y为一个值，因此可以通过 let 绑定进行泛化，这与非值相反f y。请参阅https://ocaml.org/manual/polymorphism.html#s%3Aweak-polymorphism。

此外，在像 OCaml 这样的 eager 语言中，eta 扩展确实改变了函数的语义。考虑

let print x =
  Format.printf "x=%s@." x;
  fun y -> Format.printf "y=%s@."

和

let print1 = print "x"
let print2 y = print "x" y

因此，eta扩展是一种语义改变的转换，而不是“万无一失”的转换。