记录的值限制

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 用于初始化与 type 的类型int变量完全没有链接的'atype字段t。而且我也不明白为什么声明'a为协变突然允许在这个不相关的领域使用任意表达式而不丢失多态性。

Answer 1

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

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

也不

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

被视为一个值，并且值表达式适用于它们两者。

对于第二点，这是工作中宽松的值限制：如果类型变量仅出现在严格协变的位置，则它始终可以被泛化。例如，类型

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

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

放宽值限制的简单解释是，协变类型参数对应于正的不可变数据块，例如

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

或者

type +'a t = A

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

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

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

在这里，通过将类型限制'a. 'a option为void option，我们使类型检查器意识到x实际上是 a None。