“a.”和“type a.”有什么区别以及何时使用它们？

Question

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

\n

let f :         \'a -> \'a = \xe2\x80\xa6 (* Isn\xe2\x80\x99t this one already polymorphic? (answer: NO) *)\nlet f : \'a.     \'a -> \'a = \xe2\x80\xa6\nlet f : type a.  a ->  a = \xe2\x80\xa6\n

\n

当使用奇特的代数数据类型（通常是 GADT）时，我们经常会看到它们，它们似乎是必要的。

\n

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

\n

Answer 1

以下是具有不同详细程度的替代解释，具体取决于您\xe2\x80\x99 的匆忙程度。;-)

\n

我将使用以下代码（取自另一个问题）作为运行示例。这里，定义上的类型注释reduce实际上是需要进行类型检查的。

\n

(* The type [(\'a, \'c) fun_chain] represents a chainable list of functions, i.e.\n * such that the output type of one function is the input type of the next one;\n * [\'a] and [\'c] are the input and output types of the whole chain.\n * This is implemented as a recursive GADT (generalized algebraic data type). *)\ntype (_, _) fun_chain =\n  | Nil  : (\'a, \'a) fun_chain\n  | Cons : (\'a -> \'b) * (\'b, \'c) fun_chain -> (\'a, \'c) fun_chain\n\n(* [reduce] reduces a chain to just one function by composing all\n * functions of the chain. *)\nlet rec reduce : type a c. (a, c) fun_chain -> a -> c =\n  fun chain x ->\n    begin match chain with\n    | Nil              -> x\n    | Cons (f, chain\') -> reduce chain\' (f x)\n    end\n

\n

短篇故事

\n

在let定义上，像这样的注释:\xc2\xa0\'a\xc2\xa0->\xc2\xa0\'a不会强制多态性：类型检查器可以将统一变量细化\'a为某种东西。这段语法确实具有误导性，因为 val 声明上的相同注释（即模块签名中的注释）确实强制执行多态性。

\n

: type a. \xe2\x80\xa6是具有显式（强制）多态性的类型注释。您可以将其视为全称量词（\xe2\x88\x80\xc2\xa0 a、 \xe2\x80\x9c 对于所有a \xe2\x80\x9c）。例如，

\n

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

\n

意味着 \xe2\x80\x9c 对于所有 \xe2\x80\x9d 类型a，您可以给一个a，some然后它将返回一个a\xc2\xa0option。

\n

本答案开头的代码利用了类型系统的高级功能，即多态递归和不同类型的分支，这使得类型推断不知所措。为了在这种情况下进行程序类型检查，我们需要像这样强制多态性。请注意，在此语法中，a是类型名称（无前导引号）而不是类型统一变量。

\n

: \'a. \xe2\x80\xa6是另一种强制多态性的语法:\xc2\xa0type\xc2\xa0a.\xc2\xa0\xe2\x80\xa6，但它实际上被包含在，所以你几乎不需要它。

\n

务实的故事

\n

: type a. \xe2\x80\xa6是一种结合了两个功能的简写语法：

\n

\n
1. 显式多态注释 \ : \'a. \xe2\x80\xa6n
   \n
   • 对于确保定义具有预期的通用性很有用
   \n
   • 当使用与初始调用不同的类型参数完成递归时需要（ \xe2\x80\x9c 多态递归 \xe2\x80\x9d即 \xe2\x80\x9cnon-regular\xe2\x80\x9d ADT 上的递归）
   \n
   \n
\n
2. 局部抽象类型 \ (type a) \xe2\x80\xa6n
   \n
   • 当不同分支具有不同类型时需要（即在\xe2\x80\x9cgeneralized\xe2\x80\x9d ADT上进行模式匹配时）
   \n
   • 允许您从定义内部引用类型a，通常是在构建一流模块时（我不会\xe2\x80\x99t对此进行更多说明）
   \n
   \n
\n

\n

这里我们使用组合语法，因为我们的定义reduce属于两种情况，以粗体显示。

\n

\n

1. 我们有多态递归，因为从 aCons构建 a ：第一个类型参数不同（我们说这是一个 \xe2\x80\x9cnon-regular\xe2\x80\x9d ADT）。(a,\xc2\xa0c) fun_chain(b,\xc2\xa0c) fun_chainfun_chain

   \n
\n

2. 我们有不同类型的分支，因为Nil构建 a(a,\xc2\xa0a) fun_chain而Cons构建 a (a,\xc2\xa0c) fun_chain（我们说这fun_chain是一个 \xe2\x80\x9cgeneralized\xe2\x80\x9d ADT，简称 GADT）。

   \n
\n

\n

需要明确的是：:\xc2\xa0\'a.\xc2\xa0\xe2\x80\xa6并:\xc2\xa0type\xc2\xa0a.\xc2\xa0\xe2\x80\xa6为定义生成相同的签名。选择一种语法或另一种语法只会影响其主体的类型检查方式。对于大多数意图和目的，您可以忘记:\xc2\xa0\'a.\xc2\xa0\xe2\x80\xa6并只记住组合形式:\xc2\xa0type\xc2\xa0a.\xc2\xa0\xe2\x80\xa6。唉，后者并没有完全包含前者，在极少数情况下，写入:\xc2\xa0type\xc2\xa0a.\xc2\xa0\xe2\x80\xa6无法\xe2\x80\x99工作，而你需要:\xc2\xa0\'a.\xc2\xa0\xe2\x80\xa6（参见@octachron\xe2\x80\x99s答案），但希望你不会\xe2\ x80\x99t 经常偶然发现它们。

\n

故事很长

\n

显式多态性

\n

OCaml 类型注释有一个肮脏的小let f\xc2\xa0: \'a\xc2\xa0-> \'a = \xe2\x80\xa6秘密：在 . 编译器将提供的注释与推断的类型统一起来，并且可以在执行此操作时自由地实例化类型变量，从而导致类型比预期的不太通用。例如是一个被接受的程序并导致. 为了确保该函数确实是多态的（即，如果定义不够通用，则让编译器拒绝该定义），您必须使用以下语法使多态性显式化：f\'a\'alet f\xc2\xa0: \'a -> \'a = fun x -> x+1val f\xc2\xa0: int -> int

\n

let f : \'a. \'a -> \'a = \xe2\x80\xa6\n

\n

对于非递归定义，这只是人类程序员添加了一个约束，使得更多的程序被拒绝。

\n

然而，在递归定义的情况下，这还有另一个含义。在对主体进行类型检查时，编译器会将提供的类型与所定义函数的所有出现的类型统一起来。未标记为多态的类型变量在所有递归调用中将变得相等。但多态递归正是当我们使用不同类型参数进行递归时；如果没有显式的多态性，这要么会失败，要么会推断出比预期不太通用的类型。为了使其工作，我们明确标记哪些类型变量应该是多态的。

\n

请注意，OCaml 无法自行对多态递归进行类型检查是有充分理由的：即将出现不可判定性（请参阅维基百科以获取参考资料）。

\n

举个例子，let\xe2\x80\x99s 在这个错误的定义上完成类型检查的工作，其中多态性没有明确表示：

\n

let f : \'a. \'a -> \'a = \xe2\x80\xa6\n

\n

我们从一些类型变量和reduce\xc2\xa0: (\'a,\xc2\xa0\'c) fun_chain -> \'a -> \'c开始。chain\xc2\xa0: (\'a,\xc2\xa0\'c) fun_chain\'a\'c

\n

\n

• 在第一个分支 中chain\xc2\xa0=\xc2\xa0Nil，所以我们实际上了解到chain\xc2\xa0: (\'c,\xc2\xa0\'c) fun_chain和\'a\xc2\xa0==\xc2\xa0\'c。我们统一这两种类型变量。（不过，现在\xe2\x80\x99并不重要。）

  \n
\n

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

  \n
\n

\n

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

\n

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

\n

(* does not typecheck! *)\nlet rec reduce : (\'a, \'c) fun_chain -> \'a -> \'c =\n  fun chain x ->\n    begin match chain with\n    | Nil              -> x\n    | Cons (f, chain\') -> reduce chain\' (f x)\n    end\n

\n

那么对递归调用进行类型检查就不再是问题了，因为我们现在知道它reduce是具有两个 \xe2\x80\x9ctype 参数\xe2\x80\x9d （非标准术语）的多态，并且这些类型参数在每次出现时都是独立实例化的的reduce; 递归调用使用band ，\'c即使封闭调用使用\'aand \'c。

\n

局部抽象类型

\n

但我们有第二个问题：构造函数的另一个分支Nil已经\'a与 统一\'c。因此，我们最终推断出一个比注释所要求的不太通用的类型，并且我们报告一个错误：

\n

Error: This definition has type \'c. (\'c, \'c) fun_chain -> \'c -> \'c\n       which is less general than \'a \'c. (\'a, \'c) fun_chain -> \'a -> \'c\n

\n

解决方案是将类型变量转换为局部抽象类型，这些类型无法统一（但我们仍然可以有关于它们的类型方程）。这样，类型方程就可以在每个分支本地导出，并且不会在构造之外发生match with。

\n

Answer 2

'a . ...在and之间犹豫时，实际的答案type a. ... 是始终使用后一种形式：

• type a. ...适用于：
  • 多态递归
  • GADT
  • 尽早引发类型错误

然而：

• 'a. ...与
  • 多态递归
  • 行类型变量的多态量化

因此type a. ... 通常是 的严格高级版本'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

该用例不受表单支持，type a. ... 主要是因为本地抽象类型、GADT 类型细化和类型约束的交互尚未形式化。因此，不支持第二个奇异用例。

Answer 3

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

\n

更长的故事

\n

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

\n

let f :         'a -> 'a = \xe2\x80\xa6\n

\n

它称为类型约束。类型约束要求定义值的类型与指定的类型模式兼容。

\n

在这个定义中，

\n

let f : 'a.     'a -> 'a = \xe2\x80\xa6\n

\n

我们有一个包含类型注释的类型约束。OCaml 术语中的“类型注释”一词的意思是：用一些信息注释类型，即将某些属性或特性附加到类型上。在这种情况下，我们将类型注释'a为多态。我们不会将值注释f为多态，也不会使用f类型'a -> 'a或类型注释值'a. 'a -> 'a注释该值。我们限制 的值与类型和注释f兼容'a -> 'a'a为多态类型变量。

\n

长期以来，语法'a.是将类型注释为多态的唯一方法，但后来 OCaml 引入了本地抽象类型。它们具有以下语法，您也可以将其添加到您的集合中。

\n

let f (type t) : t -> t = ...\n

\n

这将创建一个新的抽象类型构造函数，您可以在定义的范围内使用它。它没有注释t为多态，因此如果您希望将其显式注释为多态，您可以编写，

\n

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

\n

其中包括 ' 作为多态的显式类型注释a和本地抽象类型的引入。不用说，编写这样的结构很麻烦，所以稍后（OCaml 4.00）他们为此引入了语法糖，以便上面的表达式可以写成简单的，

\n

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

\n

因此，这种语法只是两个相当正交的特征的合并：局部抽象类型和显式多态类型。

\n

然而，这种合并的结果并不比它的各个部分更强大。它更像是一个十字路口。虽然生成的类型既是局部抽象的又是多态的，但它被限制为基本类型。换句话说，它限制了类型的种类，但这是一个完全不同的高级多态性问题。

\n

总结一下这个故事，尽管语法相似，但以下不是类型注释，

\n

val f : 'a -> 'a\n

\n

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

\n\n

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

\n