Полиморфный вариант -> GADT?
Я пишу систему на Прологе и использую полиморфные варианты для представления терминов Пролога.
В частности, я использую полиморфные варианты (вместо обычных), поэтому я могу создавать подтипы, обеспечивая при этом превосходную проверку полноты соответствий по подтипам в OCaml.
Все идет нормально!
Я много раз читал о GADT (на Discussion.ocaml.org и на realworldocaml.org). Мне кажется, что GADT предлагают аналогичные функции, но с меньшим объемом памяти: полиморфные варианты с вариантами, имеющими более одного аргумента, требуют дополнительного указателя, который не нужен обычным вариантам.
Пока мне не удалось успешно использовать GADT, поэтому вот мой вопрос:
Есть ли простой и понятный способ преобразовать код, использующий полиморфные варианты, в GADT? Возможно ли это в общем случае?
Заранее спасибо!
1 ответ
Есть ли простой и понятный способ преобразовать код, использующий полиморфные варианты, в GADT? Возможно ли это вообще в общем случае?
Нет, потому что они, в общем, служат совершенно разным целям.
Полиморфные варианты обеспечивают выделение подтипов для типов суммы. GADT включает ограничения для вариантов типа суммы.
Однако вы можете использовать оба метода для разделения типа суммы на частный набор типов, составляющих ваш супертип. Вы даже можете использовать фантомные полиморфные варианты в качестве типа свидетеля для каждого подмножества.
Давайте сделаем код, представим, что у нас есть набор фигур, который мы хотели бы разделить на два непересекающихся подмножества кругов и прямоугольников.
Используя полиморфные варианты,
type circle = [ `circle of int]
type rectangle = [`rectangle of int * int]
type figure = [circle | rectangle]
и то же самое с использованием GADT
type circle = Is_circle
type rectangle = Is_rectangle
type _ figure =
| Circle : int -> circle figure
| Rectangle : int * int -> rectangle figure
Обратите внимание, как ограничение явно выражается с помощью
circle и
rectangleтип. Мы могли бы даже использовать полиморфные варианты, чтобы засвидетельствовать ограничение. Все будет работать до тех пор, пока средство проверки типов может различать два типа в ограничении (т. Е. Абстрактные типы не будут работать, поскольку их реализация может быть одинаковой).
Теперь давайте сделаем несколько операций, связанных с выделением подтипов. Начнем с полиморфных вариантов
let equal_circle (`circle r1) (`circle r2) = r1 = r2
let equal_rectangle (`rectangle (x1,y1)) (`rectangle (x2,y2)) =
x1 = x2 && y1 = y2
let equal_figure x y = match x,y with
| (#circle as x), (#circle as y) ->
equal_circle x y
| (#rectangle as x), (#rectangle as y) ->
equal_rectangle x y
| #rectangle, #circle
| #circle, #rectangle -> false
Все идет нормально. Небольшая оговорка в том, что наши
equal_circle и
equal_rectangle функции слишком полиморфны, но это можно легко решить, добавив правильное ограничение типа или имея подпись модуля (мы всегда используем подписи модулей, верно?).
Теперь давайте проделаем то же самое с GADT, медленно,
let equal_circle (Circle x) (Circle y) = x = y
let equal_rectangle (Rectangle (x1,y1)) (Rectangle (x2,y2)) =
x1 = x2 && y1 = y2
Выглядит так же, как и пример с поли, с небольшими синтаксическими различиями. Тип также выглядит красиво и аккуратно,
val equal_circle : circle figure -> circle figure -> bool. Нет необходимости в дополнительных ограничениях, программа проверки типов делает нашу работу за нас.
Хорошо, теперь попробуем написать супер метод, с первой попытки не получится:
(* not accepted by the typechecker *)
let equal_figure x y = match x,y with
| (Circle _ as x), (Circle _ as y) ->
equal_circle x y
| (Rectangle _ as x), (Rectangle _ as y) ->
equal_rectangle x y
В GADT средство проверки типов по умолчанию выбирает конкретный индекс типа, поэтому вместо того, чтобы приписывать
'a figure -> 'b figure -> bool type, проверка типов выберет произвольный индекс, в нашем случае это
circle и жалуются, что
rectangle figure это не
circle figure. Нет проблем, мы можем прямо сказать, что хотим разрешить сравнение произвольных фигур,
let equal_figure : type k. k figure -> k figure -> bool =
fun x y -> match x,y with
| (Circle _ as x), (Circle _ as y) ->
equal_circle x y
| (Rectangle _ as x), (Rectangle _ as y) ->
equal_rectangle x y
Этот
type kговорит контролеру типов: "обобщить все вхождения k". Итак, теперь у нас есть метод, типизация которого немного отличается от типизации соответствующего метода, реализованного с полиморфными вариантами. Он может сравнивать фигуры одного вида, но не цифры разных типов, т. Е. Имеет тип
'a figure -> 'a figure -> bool. То, что вы не можете выразить с помощью полиморфных вариантов, действительно, та же реализация с поливариантами не является исчерпывающей,
let equal_figure x y = match x,y with (* marked as non-exhaustive *)
| (#circle as x), (#circle as y) ->
equal_circle x y
| (#rectangle as x), (#rectangle as y) ->
equal_rectangle x y
Конечно, мы можем реализовать более общий метод, который позволяет сравнивать произвольные цифры с помощью GADT, например, следующее определение имеет тип
'a figure -> 'b figure -> bool
let equal_figure' : type k1 k2. k1 figure -> k2 figure -> bool =
fun x y -> match x,y with
| (Circle _ as x), (Circle _ as y) ->
equal_circle x y
| (Rectangle _ as x), (Rectangle _ as y) ->
equal_rectangle x y
| Rectangle _, Circle _
| Circle _, Rectangle _ -> false
Мы сразу видим, что для наших целей GADT - более мощный инструмент, который дает нам больше контроля над ограничениями. А учитывая, что мы можем использовать полиморфные варианты и типы объектов в качестве индексов типов для выражения ограничений, мы можем получить лучшее из двух миров - детализированные ограничения и подтипы.
Честно говоря, вы можете добиться того же результата, что и с GADT, но без GADT, используя стиль без тегов-final. Но это деталь реализации, которая иногда важна на практике. Основная проблема GADT в том, что они не сериализуемы. Действительно, фантомный тип нельзя хранить.
В заключение, независимо от того, используете ли вы GADT или стиль без тегов, у вас гораздо больше контроля над ограничениями типа и вы можете более четко выразить свое намерение (и позволить средству проверки типов обеспечить его соблюдение). Мы часто используем его в BAP, чтобы выразить сложные ограничения правильно сформированных программ, например, что операции с битовыми векторами применяются к векторам одинаковой длины. Это позволяет нам игнорировать плохо сформированные программы в нашем анализе и экономит несколько строк кода и несколько часов отладки.
Ответ, даже на этом простом примере, уже стал слишком большим, поэтому я должен остановиться. Я бы посоветовал вам посетить Discaml.org и поискать там GADT и полиморфные варианты. Помню, там было еще несколько обстоятельных обсуждений.