Ocaml 中的开放和封闭联合类型

Question

我是第一次研究 OCaml，对 F# 和 Haskell 有一点背景。因此，很多东西看起来很熟悉，但不熟悉的是“开放”和“封闭”联合的概念（带有反引号和 [

这些有什么用？使用频率如何？

Answer 1

gasche's answer has good advice。我将进一步解释开放和封闭工会。

首先，您需要区分两种联合：基本变体（无反引号）和多态变体（带反引号）。

• 基本变体是生成的：如果您在不同的模块M1 和M2 中定义了两个具有相同构造函数名称的类型，则您有不同的类型。 M1.Foo 和 M2.Foo 是不同的构造函数。 `Foo 始终是同一个构造函数，无论您在哪里使用它。
• 除此之外，多态变体可以做任何基本变体可以做的事情，甚至更多。但强大的力量带来了巨大的复杂性，因此您应该仅在必要时谨慎使用它们。

多态变体类型描述了该类型可能具有的构造函数。但是许多多态变体类型并不完全为人所知——它们包含（行）类型变量。考虑空列表[]：它的类型是'a list，它可以在许多将更具体的类型分配给'a 的上下文中使用。例如：

# let empty_list = [];;
val empty_list : 'a list = []
# let list_of_lists = [] :: empty_list;;
val list_of_lists : 'a list list = [[]]
# let list_of_integers = 3 :: empty_list;;
val list_of_integers : int list = [3]

同样适用于行类型变量。一个开放类型，写成[> … ]，有一个行变量，可以在每次使用该值时实例化更多的构造函数。

# let foo = `Foo;;
val foo : [> `Foo ] = `Foo
# let bar = `Bar;;
val bar : [> `Bar ] = `Bar
# let foobar = [foo; bar];;
val foobar : [> `Bar | `Foo ] list = [`Foo; `Bar]

仅仅因为构造函数出现在一个类型中并不意味着每次使用该类型都必须允许所有构造函数。 [> …] 说一个类型必须至少有这些构造函数，而双重[< …] 说一个类型必须最多有这些构造函数。考虑这个函数：

# let h = function `Foo -> `Bar | `Bar -> `Foo;;
val h : [< `Bar | `Foo ] -> [> `Bar | `Foo ] = <fun>

h只能处理Foo和Bar，所以输入类型可能不允许其他构造函数；但是可以在只允许Foo 的类型上调用h。相反，h 可能返回 Foo 或 Bar，并且使用 h 的任何上下文必须同时允许 Foo 和 Bar（并且可能允许其他人）。

当一个类型有匹配的最小和最大构造函数要求时，就会出现封闭类型。例如，让我们添加h必须具有相同输入和输出类型的约束：

# let hh : 'a -> 'a = function `Foo -> `Bar | `Bar -> `Foo;;
val hh : [ `Bar | `Foo ] -> [ `Bar | `Foo ] = <fun>

封闭类型很少从类型推断中自然产生。大多数时候，就像这里一样，它们是用户注释的结果。当您使用多态注释时，最好定义命名类型并至少在每个顶级函数上使用它们。否则推断的类型可能比你想象的更一般。虽然这很少会导致错误，但它通常意味着任何类型错误都将被诊断得晚，并且会生成很长的错误消息，很难找到有用的信息。

我建议阅读并完成工作（即在顶层重新键入示例，试一试以确保您理解每个步骤）polymorphic variant tutorial in the Ocaml manual。

Answer 2

您需要阅读 Jacques Garrigue 的“使用多态变体的代码重用”：

http://www.math.nagoya-u.ac.jp/~garrigue/papers/fose2000.html

多态变体的问题在于它们非常灵活，以至于类型推断无法帮助您解决多态变体代码中的错误。例如，如果您输入错误的构造函数名称，编译器将无法标记错误，它只会推断出与通常构造函数略有不同的类型，以及拼写错误的类型。只有在您尝试将错误代码与对变体有严格假设的函数（封闭模式匹配）结合起来时，才会发现错误，并带有笨拙的错误消息。

我对多态变体用户的建议是大量使用注释来控制类型检查：每次将多态变体作为输入或输出时，都应该为函数部分使用精确的类型进行注释。这将使您免受大多数推理问题的影响，并迫使您构建一组富有表现力的类型定义，这些定义可以组合并帮助推理您的程序。