16

我正在浏览 ocaml 的标准库，并在 map.ml 文件中遇到了这段代码。

module type S =
  sig
    type key
    type +'a t
    val empty: 'a t'

我想知道为什么有type +'a t，为什么作者使用它而不是简单地使用它'a t。
它的行为很奇怪，我无法推断出它的用法。

# type +'a t = 'a list;;
type 'a t = 'a list
# type +'a t = +'a list;;
Characters 13-14:
  type +'a t = +'a list;;
               ^
Error: Syntax error

谢谢

4

2 回答 2

16

为了建立 Jeffrey 的回答，开发人员在这里将抽象类型标记为协变的原因可能不会帮助您使用子类型（基本上没有人在 OCaml 中使用子类型，因为通常首选参数多态），而是使用类型系统中更鲜为人知的方面称为“宽松的值限制”，这要归功于协变抽象类型允许更多的多态性。

你可以放心地忽略这些细微之处，直到有一天，你遇到了一个抽象类型的问题，它不像你想要的那样多态，然后你应该记住，签名中的协方差注释可能会有所帮助。

几个月前，我们在 reddit/ocaml 上讨论过这个问题：

考虑以下代码示例：

module type S = sig
  type 'a collection
  val empty : unit -> 'a collection
end

module C : S = struct
  type 'a collection =
    | Nil
    | Cons of 'a * 'a collection
  let empty () = Nil
end

let test = C.empty ()

您获得的类型test是'_a C.collection，而不是'a C.collection您期望的类型。它不是多态类型（'_a是尚未完全确定的单态推理变量），在大多数情况下您不会对它感到满意。

这是因为C.empty ()不是一个值，所以它的类型不是泛化的（~变成了多态的）。要从放宽的值限制中受益，您必须标记抽象类型'a collection协变：

module type S = sig
  type +'a collection
  val empty : unit -> 'a collection
end

当然，这只是因为模块C是用签名密封的S: module C : S = ...。如果模块C没有给出明确的签名，类型系统会推断出最普​​遍的方差（这里是协方差），而人们不会注意到这一点。

针对抽象接口进行编程通常很有用（在定义函子、执行幻像类型规则或编写模块化程序时），所以这种情况肯定会发生，然后了解放宽的值限制很有用。

如果您想了解该理论，价值限制及其放松在 2004 年的研究文章中讨论了Jacques Garrigue 的放松价值限制，其前几页是对该主题和主要思想的相当有趣且易于理解的介绍。

于 2013-03-09T06:55:55.040 回答
13

这将类型标记为相对于模块类型是协变的。假设您有两个键是相同类型的映射。这+表示如果一个映射 A 的值是另一个映射 B 的值的子类型，则映射 A 的整体类型是映射 B 的类型的子类型。我在Jane Street 博客中找到了一个很好的描述。

于 2013-03-09T00:30:17.983 回答