Открытые и закрытые типы соединений в Ocaml

Ответ 1

Ответ на газ дает хороший совет. Я собираюсь объяснить открытые и закрытые союзы немного больше.

Во-первых, вам нужно различать два типа союзов: базовые варианты (без обратного хода) и полиморфные варианты (с обратным ходом).

• Основные варианты являются генеративными: если вы определяете два типа с одинаковыми именами конструкторов в разных модулях 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]

Просто потому, что конструктор появляется в типе, не означает, что каждое использование этого типа должно разрешать все конструкторы. [> …] говорит, что тип должен иметь по крайней мере эти конструкторы, а dually [< …] говорит, что тип должен иметь не более этих конструкторов. Рассмотрим эту функцию:

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

h способен обрабатывать Foo и Bar, поэтому тип ввода может не разрешать другие конструкторы; но это нормально, чтобы вызвать h для типа, который разрешает только Foo. И наоборот, h может возвращать Foo или Bar, и любой контекст, в котором используется h, должен допускать как Foo, так и Bar (и может допускать другие).

Закрытые типы возникают, когда требуются минимальные и максимальные требования к конструктору для типа. Например, добавьте ограничение, что h должно иметь один и тот же тип ввода и вывода:

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

Закрытые типы редко возникают, естественно, из вывода типа. В большинстве случаев, как и здесь, они являются следствием аннотации пользователя. Когда вы используете полиморфные аннотации, полезно определить именованные типы и использовать их по крайней мере на каждой функции верхнего уровня. В противном случае предполагаемый тип, вероятно, будет немного более общим, чем вы думали. Хотя это редко открывает путь к ошибкам, это часто означает, что любая ошибка типа будет диагностирована позже, чем это могло бы быть, и создаст очень длинное сообщение об ошибке, где будет трудно найти полезные биты.

Я рекомендую читать и работать (т.е. повторять примеры в верхнем слое, немного поиграть, чтобы убедиться, что вы понимаете каждый шаг) полиморфный вариант учебника в руководстве Ocaml.

Ответ 2

Вам нужно прочитать Жак Гарригу "Повторное использование кода с полиморфными вариантами":

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

Проблема с полиморфными вариантами заключается в том, что они настолько гибки, что вывод типа не может сильно помочь вам с ошибками в коде полиморфных вариантов. Например, если вы ошибочно используете одно имя конструктора, компилятор не сможет помечать ошибку, он будет выводить несколько разные типы с помощью обычных конструкторов, а также с ошибкой. Ошибки будут обнаружены позже, когда вы попытаетесь совместить неисправный код с функцией со строгими предположениями по вариантам (закрытое сопоставление шаблонов) с неудобным сообщением об ошибке.

Мой совет для пользователей с полиморфными вариантами - это массовое использование аннотаций для управления проверкой типов: каждый раз, когда вы принимаете полиморфный вариант в качестве входного или выходного, функция должна быть аннотирована с точным типом для варианта. Это защитит вас от большинства проблем вывода и заставит вас создать выразительный набор определений типов, которые могут быть скомпонованы и помочь в определении вашей программы.