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

发布于 2024-10-19 13:20:28 字数 126 浏览 2 评论 0原文

我是第一次研究 OCaml,对 F# 和 Haskell 有一些背景知识。因此,很多内容看起来很熟悉,但有一点不熟悉,那就是“开放”和“封闭”联合的概念(使用反引号和 [< 语法)。

这些有什么用处以及使用频率如何?

I'm looking into OCaml for the first time, having a bit of background with F# and Haskell. As such, a lot is familiar-looking, but one thing that isn't is the concept of "open" and "closed" unions (with the backtick and [< syntax).

What are these useful for and how often are they used?

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(2

‘画卷フ 2024-10-26 13:20:29

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

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

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

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

You need to read Jacques Garrigue's "Code reuse with polymorphic variants":

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

The problem with polymorphic variants is that they are so flexible that type inference cannot help you a lot with errors in polymorphic variants code. For example, if you mistype one constructor name, the compiler won't be able to flag an error, it will only infer a slightly different types with the usual constructors, plus the misspelled one. Errors will only be spotted later, when you try to combine the faulty code with a function with strict assumptions on the variants (closed pattern matching), with an unwieldy error message.

My advice for polymorphic variant users is to massively use annotations to control type-checking : every time you take a polymorphic variant as input, or output one, the function should be annotated with a precise type for the variant part. This will shield you from most inference issues, and force you to build an expressive set of type definitions that can be composed and help reasoning about your program.

千紇 2024-10-26 13:20:28

gasche 的回答提供了很好的建议。我将进一步解释开放式联合和封闭式联合。

首先,您需要区分两种联合:基本变体(无反引号)和多态变体(带反引号)。

  • 基本变体是生成的:如果您在不同模块 M1M2 中定义具有相同构造函数名称的两个类型,则您将拥有不同的类型。 M1.FooM2.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 只能处理 FooBar,因此输入类型可能不允许其他构造函数;但在只允许 Foo 的类型上调用 h 是可以的。相反,h 可能返回 FooBar,并且使用 h 的任何上下文都必须允许 FooBar (并且可能允许其他)。

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

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

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

我建议阅读并完成(即重新输入顶层的示例,稍微尝试一下以确保您理解每个步骤)Ocaml 手册中的多态变体教程

gasche's answer has good advice. I'm going to explain open and closed unions a bit more.

First, you need to distinguish the two kinds of unions: basic variants (no backtick) and polymorphic variants (with backtick).

  • Basic variants are generative: if you define two types with the same constructor names in different modules M1 and M2, you have different types. M1.Foo and M2.Foo are different constructors. `Foo is always the same constructor no matter where you use it.
  • Apart from this, polymorphic variants can do everything basic variants can do and more. But with great power comes great complexity, so you should use them only when necessary and carefully.

A polymorphic variant type describes what constructors the type may have. But many polymorphic variant types are not fully known — they contain (row) type variables. Consider the empty list []: its type is 'a list, and it can be used in many contexts that assign more specific types to 'a. For example:

# 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]

The same holds for the row type variables. An open type, written [> … ], has a row variable that can be instantiated to cover more constructors each time the value is used.

# 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]

Just because a constructor appears in a type doesn't mean every use of that type has to allow all constructors. [> …] says that a type must have at least these constructors, and dually [< …] says that a type must have at most these constructors. Consider this function:

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

h is only capable of handling Foo and Bar, so the input type may not allow other constructors; but it's ok to call h on a type that only allows Foo. Conversely, h may return Foo or Bar, and any context where h is used must allow both Foo and Bar (and may allow others).

Closed types arise when there are matching minimum and maximum constructor requirements on a type. For example, let's add the constraint that h must have the same input and output type:

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

Closed types rarely arise naturally from type inference. Most of the time, like here, they are a consequence of a user annotation. When you use polymorphic annotations, it's a good idea to define named types and use them at least on every toplevel function. Otherwise the inferred type is likely to be a little more general than you thought. While this rarely opens the way to bugs, it often means that any type error will be diagnosed later than it could have been, and will generate a very long error message where it will be hard to find the helpful bits.

I recommend reading and working through (i.e. retype the examples in the toplevel, play around a bit to make sure you understand each step) the polymorphic variant tutorial in the Ocaml manual.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文