generics - 为什么编译器会将两个具有不同名称的等效签名的泛型类型变量识别为不同类型？

Question

问题

为什么

val of_bindings : (key * '_a) list -> '_a t
val of_bindings : (key * 'a) list -> 'a t

不同的签名？

上下文

我有一些 map 扩展实现:

MAPEXT.ml:

module type T = sig
    include Map.S    
    val of_bindings : (key * 'a) list -> 'a t
  end 

ma​​pExt.mli:

module Make (Key : Map.OrderedType)
     : MAPEXT.T with type key = Key.t

ma​​pExt.ml:

module Make (Key : Map.OrderedType) = struct
    include Map.Make (Key)
    let of_bindings =
      let rec of_bindings acc =
        function | (k, v) :: t -> of_bindings (add k v acc) t
                 | []          -> acc in
      of_bindings empty
  end

编译器给了我一个错误，因为 ocamlopt -c MAPEXT.ml mapExt.mli mapExt.ml

Error: The implementation mapExt.ml does not match the interface mapExt.cmi: ... At position module Make(Key) : Values do not match: val of_bindings : (key * '_a) list -> '_a t is not included in val of_bindings : (key * 'a) list -> 'a t File "mapExt.ml"

我认为泛型类型变量的名称并不重要，只是用于表示不同的类型。但从我现在看来，它们似乎有不同的含义。

如何避免编译此代码时出现此问题？

相关:What is the difference between 'a and '_l?

Answer 1

这不仅仅是一个不同的名称(你是对的，类型变量的名称并不重要)。如果类型变量名称以 '_ 序列开头，则编译器表示该类型变量是弱多态的。简单来说，它根本不是多态的，它表明你的值不是通用的。基本上，类型变量表示您的值具有一系列类型，例如，'a list 是可能属于一系列类型的值，例如，int list、字符串列表等。换句话说，类型变量表示无限范围的类型，即，它是 for all 表示法。弱类型变量则相反，因为它的范围不涵盖多种类型，而仅涵盖一种类型，即，如果您有一个 '_a list 类型的值，则意味着存在一种类型x (一个且仅有一个)，这样您的值的类型就是 x list。只是编译器还不知道类型。出于礼貌，编译器给了我们额外的自由度，并且不会给出类型错误。

类型变量没有被推广到 for all 概念而是坚持存在表示法的原因，隐藏在 OCaml 和函数应用的可变性中。一般规则是，如果编译器无法证明值计算没有任何可观察到的副作用，则该值不会被泛化，并且所有类型变量仍然是弱的。由于从部分函数应用程序获得的值是任意计算的结果，因此编译器保守地假设该计算可能具有副作用，并且不会概括该类型。这称为 value restriction这是 OCaml 类型系统的一个特性。处理它的通常方法是添加所有参数，以便该值不是由部分应用程序生成的，而是成为语法值 - 在编译期间计算(确定)的一类值。这个机制的奇特名字是 Eta Expansion 。