logo标签列表

`'a.` and `type a.`之间有什么区别？何时使用每个？

polymorphismocamltype-inferencealgebraic-data-types
17

OCaml有几种不同的语法用于多态类型注释：

let f :         'a -> 'a = … (* Isn’t this one already polymorphic? (answer: NO) *)
let f : 'a.     'a -> 'a = …
let f : type a.  a ->  a = …

在使用高级代数数据类型（通常是GADTs）时，我们经常看到它们，似乎它们是必需的。

这些语法之间有什么区别？何时以及为什么必须使用每个语法？

3个回答
15
以下是不同细节程度的替代解释，取决于您有多急。 ;-)
我将使用以下代码（来自那个问题）作为运行示例。在这里，对reduce定义的类型注释实际上是必需的，以使其通过类型检查。
(* The type [('a, 'c) fun_chain] represents a chainable list of functions, i.e.
 * such that the output type of one function is the input type of the next one;
 * ['a] and ['c] are the input and output types of the whole chain.
 * This is implemented as a recursive GADT (generalized algebraic data type). *)
type (_, _) fun_chain =
  | Nil  : ('a, 'a) fun_chain
  | Cons : ('a -> 'b) * ('b, 'c) fun_chain -> ('a, 'c) fun_chain

(* [reduce] reduces a chain to just one function by composing all
 * functions of the chain. *)
let rec reduce : type a c. (a, c) fun_chain -> a -> c =
  fun chain x ->
    begin match chain with
    | Nil              -> x
    | Cons (f, chain') -> reduce chain' (f x)
    end

简短故事

在let-definitions中，注释如: 'a -> 'a并不会强制多态：类型检查器可以将统一变量'a细化为其他内容。这个语法有点误导人，因为在val-declaration中即在模块签名中使用相同的注释会强制多态。

: type a. …是一个具有显式（强制）多态的类型注释。您可以将其视为全称量词（∀a，“对于所有a”）。例如，

let some : type a. a -> a option =
  fun x -> Some x

意味着“对于所有”的类型a，您可以将a提供给some，然后它将返回一个a option。
本答案开头的代码利用了类型系统的高级功能，即多态递归和不同类型的分支，这使得类型推断无法解决。为了使程序在这种情况下能够通过类型检查，我们需要像这样强制使用多态性。请注意，在此语法中，a是类型名称（没有引号），而不是类型统一变量。 : 'a. …是另一种强制多态性的语法，但实际上被: type a. …所包含，因此您几乎不需要使用它。
实用故事 : type a. …是一种简写语法，结合了两个特性：
  1. 明确的多态注释: 'a. …
    • 用于确保定义与预期一样通用
    • 当使用与初始调用的类型参数不同的类型参数进行递归（即“多态递归”，即非“常规”ADT上的递归）时必需的
  2. 局部抽象类型(type a) …
    • 当不同分支具有不同类型时（即在“广义”ADT上进行模式匹配时）必需的
    • 允许您从定义内部引用类型a，通常是构建一流模块时（我不会再多说了）
在这里，我们使用组合语法，因为我们对reduce的定义符合粗体字中的两种情况。

  1. 我们拥有多态递归，因为Cons从(b, c) fun_chain构建了一个(a, c) fun_chain：第一个类型参数不同（我们称fun_chain为“非正则”ADT）。

  2. 我们有不同类型的分支，因为Nil构建了一个(a, a) fun_chain，而Cons构建了一个(a, c) fun_chain（我们称fun_chain为“广义”ADT或GADT）。

只是为了明确：: 'a. ...和: type a. ...对于定义来说产生相同的签名。选择其中一种语法只会影响其体的类型检查方式。对于大多数意图和目的而言，您可以忘记: 'a. ...并记住组合形式: type a. ...。可惜的是，后者并不能完全取代前者，有些罕见的情况下编写: type a. ...不起作用，您需要: 'a. ...（请参见@octachron的答案），但希望您不经常遇到这些情况。

长篇故事

显式多态

OCaml类型注释有一个不为人知的秘密：写let f : 'a -> 'a = ...并不会强制f在'a上是多态的。编译器将提供的注释与推断出的类型统一，并可以在此过程中实例化类型变量'a，导致比预期更少的通用类型。例如，let f : 'a -> 'a = fun x -> x+1是一个被接受的程序，并导致val f : int -> int。为确保函数确实是多态的（即使编译器拒绝定义如果它不够通用），您必须使用以下语法来使多态性显式：

let f : 'a. 'a -> 'a = …

对于非递归定义，这只是人类程序员添加了一个约束条件，使得更多的程序被拒绝。
但在递归定义的情况下，这有另一个含义。在类型检查函数体时，编译器将提供的类型与正在定义的函数的所有出现的类型进行统一。未标记为多态的类型变量将在所有递归调用中相等。但是多态递归恰好是我们使用不同的类型参数进行递归的情况；没有显式的多态性，这要么会失败，要么推断出比预期更少的一般类型。为了使其工作，我们明确标记哪些类型变量应该是多态的。
请注意，OCaml不能单独完成多态递归的类型检查是有充分理由的：这里有不可判定性的问题（参见维基百科的参考资料）。
作为示例，让我们来看一下这个错误的定义，在其中没有明确指定多态性时，类型检查器的工作：
(* does not typecheck! *)
let rec reduce : ('a, 'c) fun_chain -> 'a -> 'c =
  fun chain x ->
    begin match chain with
    | Nil              -> x
    | Cons (f, chain') -> reduce chain' (f x)
    end

我们从 reduce : ('a, 'c) fun_chain -> 'a -> 'c 和 chain : ('a, 'c) fun_chain 开始，其中 'a 和 'c 是一些类型变量。

  • 在第一个分支中，chain = Nil，所以我们了解到实际上 chain : ('c, 'c) fun_chain 并且 'a == 'c。我们统一两个类型变量。（暂时不需要关注这一点。）

  • 在第二个分支中，chain = Cons (f, chain')，因此存在一个任意类型 b，使得 f : 'a -> b 并且 chain' : (b, 'c) fun_chain。然后我们必须对递归调用 reduce chain' 进行类型检查，因此预期的参数类型 ('a, 'c) fun_chain 必须与提供的参数类型 (b, 'c) fun_chain 统一；但是没有什么告诉我们 b == 'a。因此，我们拒绝这个定义，最好（按传统方式）带有一个神秘的错误消息：

Error: This expression has type ($Cons_'b, 'c) fun_chain
       but an expression was expected of type ('c, 'c) fun_chain
       The type constructor $Cons_'b would escape its scope

如果现在我们明确表明多态性：

(* still does not typecheck! *)
let rec reduce : 'a 'c. ('a, 'c) fun_chain -> 'a -> 'c =
  …

然后对递归调用进行类型检查就不再是问题了，因为我们现在知道reduce是带有两个“类型参数”（非标准术语）的多态函数，并且这些类型参数在每个reduce出现时独立实例化；即使封闭调用使用'a和'c，递归调用也使用b和'c。
局部抽象类型
但是我们还有第二个问题：构造函数Nil的另一个分支已经将'a与'c统一。 因此，我们推断出的类型比注释要求的类型更不通用，并报告错误：
Error: This definition has type 'c. ('c, 'c) fun_chain -> 'c -> 'c
       which is less general than 'a 'c. ('a, 'c) fun_chain -> 'a -> 'c

解决方法是将类型变量转换为本地抽象类型，这些类型不能被统一（但我们仍然可以对它们进行类型方程）。这样，类型方程会在每个分支中局部推导，并且不会泄露到match with结构之外。
非常有趣的答案！谢谢。现在我想知道为什么这个错误如此晦涩，它实际上意味着什么“类型构造器$Cons_'b将逃离其范围”。 - David 天宇 Wong
1
@David天宇Wong，这只是一个猜测，但我认为它的意思是：$Cons_'b 是在 Cons ... -> ... 分支的类型检查中引入的任意类型，但其约束条件要求将其与未在 Cons ... -> ... 的类型检查范围内引入的类型变量统一，这是不合法的，原因在答案中已经给出。我认为错误信息并不好，因为它没有告诉你出了什么问题，而是“泄漏”了编译器不变式失败的信息，告诉你“我无法编译那个，一定有问题”。 - jthulhu
哦，是的，那很有道理！我同意，但我还没有看到OCaml编译器产生过好的编译错误，所以我想这并不是什么特别的事情 :P - David 天宇 Wong
我有这样的印象，当您解释显式多态语法 type a. 时，您的意思是 a 是一个“真正”的类型变量，而不是可以进行统一的东西。但是，在“局部抽象类型”部分下，您说即使是显式多态也最终将 'a 与 'c 统一起来，我们应该使用局部抽象类型。因此，我真的不明白显式多态注释和局部抽象类型之间的区别在哪里。 - Hirrolot
6
在选择使用. ..和. ..时，实际上更好的做法是始终使用后者：
  • . ..与以下内容兼容：
    • 多态递归
    • GADTs
    • 提前抛出类型错误

而：

  • 'a. ..
    • 与以下内容兼容：
    • 多态递归
    • 行类型变量的多态量化

因此，. ..通常是 . .. 的严格优化版本。

除了最后一个奇怪的点。为了详尽无遗，让我举一个行类型变量量化的例子：

let f: 'a. ([> `X ] as 'a) -> unit = function
  | `X -> ()
  | _ -> ()

这里的全称量词使我们能够精确控制行变量类型。例如，

let f: 'a. ([> `X ] as 'a) -> unit = function
  | `X | `Y -> ()
  | _ -> ()

产生以下错误。 
Error: This pattern matches values of type [? `Y ]
      but a pattern was expected which matches values of type [> `X ]
      The second variant type is bound to the universal type variable 'a,
      it may not allow the tag(s) `Y

由于本地抽象类型、GADTs类型细化和类型约束的交互尚未形式化，因此表单type a....不支持这种用例。因此，这种第二种奇特的用例不受支持。

最后一个奇怪的点来自于局部抽象类型是一个普通类型，所以你不能将多态类型与普通类型合一。在某种程度上，局部抽象多态类型是个矛盾之语，因为你正在将类型注释为多态类型，但要求它是普通的，即非多态的。高阶多态性的优点)) 因此不是绝对优越的版本，'a. 'a 是比 type a. a 更通用的类型。它的范围让它感觉更强大。 - ivg
5

简而言之，在您的问题中，只有最后两种形式是多态类型注释。这两种形式中的后者除了将类型注释为多态之外，还引入了一个局部抽象类型1。这是唯一的区别。

更长的故事

现在让我们稍微谈一下术语。以下内容不是类型注释（或更准确地说，不包含任何类型注释），

let f :         'a -> 'a = …

这被称为 类型约束。类型约束要求定义的值的类型与指定的类型架构相兼容。

在此定义中，

let f : 'a.     'a -> 'a = …

我们有一个类型约束，其中包括一个"类型注释(type annotation)"。在OCaml语境中，"类型注释"这个短语的意思是"用一些信息对类型进行注释"，即将某些属性或属性附加到类型上。在本例中，我们将类型'a标记为多态类型（polymorphic）。我们既不将值"f"标记为多态，也不将值"f"标记为类型"'a -> 'a" 或 "'a. 'a -> 'a"。我们是通过约束值"f"与类型"'a -> 'a"兼容，并将"'a"注释为多态类型变量。
长期以来，语法"'a."是注释类型为多态的唯一方式，但后来OCaml引入了局部抽象类型。它们具有以下语法，您也可以将其添加到您的集合中。
let f (type t) : t -> t = ...

这将创建一个新的抽象类型构造器，您可以在定义的范围内使用。尽管如此它不会将t标注为多态的，所以如果你想将其明确标注为多态的话，可以这样写：

let f : 'a. 'a -> 'a = fun (type t) (x : t) : t -> ...

这包括一个显式类型注释 'a作为多态和引入局部抽象类型。毋庸置疑，编写这样的构造非常麻烦，因此稍后（OCaml 4.00）引入了语法糖，使上述表达式可以像简单表达式一样书写：

let f : type t. t -> t = ...

因此，这个语法只是两个相对独立的特性的结合：局部抽象类型和显式多态类型。
然而，这种结合并不比其各自的部分更强大。它更像是一个交集。虽然生成的类型既是局部抽象的又是多态的，但它被限制为基础类型。换句话说，它限制了类型的种类，但这是高阶多态的完全不同问题。
最后要说的是，尽管语法相似，以下内容不是类型注释。
val f : 'a -> 'a

这被称为值规范，它是签名的一部分，并表示值f具有类型'a -> 'a。

1))本地抽象类型有两个主要用途。首先，您可以在表达式中使用它们，在不允许类型变量的地方使用，例如在模块和异常定义中。其次，局部抽象类型的作用域超出了函数的作用域，您可以通过将局部创建的类型与抽象类型统一来扩展其作用域。基本思想是表达式不能超出其类型的范围，由于在OCaml中类型可以在运行时创建，因此我们必须小心类型的范围。通过函数参数将本地创建的类型与本地抽象类型进行统一，可以保证该类型将与函数应用的位置中的某个现有类型统一。直观地说，这就像传递类型的引用，以便从函数返回类型。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接