为什么编译器将不同名称的泛型类型变量的两个等价签名标识为不同的类型?

问题描述:

问题为什么编译器将不同名称的泛型类型变量的两个等价签名标识为不同的类型?

为什么

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

不同的签名?

语境

我有一些地图扩展实现:

MAPEXT.ml:

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

mapExt.mli:

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

mapExt.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?

+1

请阅读“通过部分应用程序获得的函数不够多态”以及https://ocaml.org/learn/faq.html#Typing – camlspotter

这不只是一个不同的名称(你是对一个类型变量的名称并不重要)。如果一个类型变量名以'_序列开头,那么这是一种编译器方式来说这个类型变量是弱多态的。简而言之,它根本不是多形的,它表示你的价值不是通用的。基本上,类型变量表示您的值具有多种类型,例如,'a list是可能属于一系列类型的值,例如int list,string list等。换句话说,类型变量表示无限范围类型,即它是所有符号。弱类型变量是相反的,因为它不包含多种类型,但仅限于一种类型,即如果您有类型为'_a list的值,则表示存在类型为x(只有一个),例如您的值的类型是x list。只是编译器还不知道类型。出于礼貌的考虑,编译器给了我们一个额外的纬度,并且不给出类型错误。

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