记录的值限制

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
  

我觉得奇怪的是函数应用程序用于初始化类型为int 的字段，它与类型为t 的类型变量'a 完全没有链接。而且我也不明白为什么将'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。