记录的值限制

Question

我遇到这样一种情况，记录被赋予弱多态类型，我不确定为什么。

这是一个最小化的例子

module type S = sig
  type 'a t
  val default : 'a t
end

module F (M : S) = struct
  type 'a record = { x : 'a M.t; n : int }

  let f = { x = M.default; n = (fun x -> x) 3 }
end

此处 f 的类型为 '_weak1 record.

有（至少）两种方法可以解决这个问题。

第一个是为功能应用程序使用辅助定义。
```
let n = (fun x -> x) 3
let f = { x = M.default; n }
```

第二个是将 t 的类型参数声明为协变的。

module type S = sig
   type +'a t
   val default : 'a t
end

我觉得奇怪的是函数application是用来初始化根本没有link的int类型的字段，用[=17=类型的变量'a 15=]。而且我也不明白为什么将 'a 声明为协变突然允许在这个不相关的字段中使用任意表达式而不会丢失多态性。

Answer 1

对于你的第一点，只要在任何子表达式中发生任何计算，就会触发放宽的值限制。因此都没有

{ x = M.default; n = (fun x -> x) 3 }

也不

let n = Fun.id 3 in { x = M.default; n }

被认为是一个值，值表达式适用于它们。

关于你的第二点，这是放宽的值限制在起作用：如果一个类型变量只出现在严格协变的位置，它总是可以被泛化。例如

的类型

let none = Fun.id None

是 'a. 'a option 而不是 '_weak1 option 因为 option 类型构造函数在其第一个参数中是协变的。

这次放宽取值限制的简单解释是协变类型参数对应一个正的不可变数据，例如

type !+'a option = None | Some of 'a

或

type +'a t = A

因此，如果我们有一个只出现在严格协变位置的类型变量，我们知道它没有绑定到任何可变数据，因此可以安全地泛化它。

然而，需要注意的重要一点是，如果 t 协变在其第一个参数中的类型 'a t 的唯一值恰好是那些不包含任何 'a 的值。因此，如果我有一个 'a. 'a option 类型的值，我知道我实际上有一个 None。事实上，我们可以在类型检查器的帮助下检查这一点：

type forall_option = { x:'a. 'a option }
type void = |
let for_all_option_is_none {x} = match (x: void option) with
| None -> ()
| _ -> . (* this `.` means that this branch cannot happen *)

这里通过将类型 'a. 'a option 限制为 void option，我们让类型检查器知道 x 实际上是 None.

记录的值限制

Value restriction for records

ocaml