Используя варианты GADT в полиморфном, составном типе, как я бы нормальных типов алгебраических вариантов? - PullRequest
Новая
       60

Используя варианты GADT в полиморфном, составном типе, как я бы нормальных типов алгебраических вариантов?

0 голосов
/ 21 ноября 2018

Допустим, у меня есть этот простой тип варианта: 

type flag = {
  name: string;
  payload: string option;
}

type word =
 | Arg of string
 | Flag of flag

let args = [|
  Arg "hello";
  Flag {name = "foo"; payload = Some "world"};
|]

Если, однако, я хочу добавить GADT-ограничения к этому типу word, 

type _ word =
 | Arg : string -> string word
 | Flag : flag -> flag word

…компилятор больше не может выводить общий тип для членов args: 

Line 12, 3:
  This expression has type flag word
       but an expression was expected of type string word
       Type flag is not compatible with type string

Это просто ограничение GADT?

Ответы [ 3 ]

0 голосов
/ 22 ноября 2018

Это не столько ограничение GADT, сколько одно из их желаемых свойств.Когда вы пишете 

type _ word =
| Arg : string -> string word
| Flag : flag -> flag word

, вы просите, чтобы типограф проверял, чтобы типы Arg _ и Flag _ были разными и несовместимыми.

Чтобы мотивировать это поведение, лучшим примером может бытьсписок со статической длиной: 

 type zero = Zero
 type 'a succ = Succ
 type ('elt,'size) nlist =
 | []: ('elt, zero) nlist
 | (::): 'elt * ('elt, 'size) nlist ->  ('elt, 'size succ) nlist

С этим определением значение типа ('n, 's) nlist содержит кодирование его длины внутри этого типа.Это позволяет написать общую функцию hd 

  let hd (a::q) = a

Поскольку наш экзотический тип списка имеет длину в своем типе, средство проверки типов может выразить тот факт, что hd принимает список только с одним или несколькимиаргумент (т.е. тип hd ('elt,_ succ) nlist -> 'elt).Таким образом, функция hd всегда возвращает (когда проверяется ее тип).

Но это также означает, что средство проверки типов теперь должно принудительно применять, чем всегда работает функция hd.Другими словами, нельзя проверять тип длины смешивания массива различного размера 

  [| []; [1]; [1;2] |]

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

Возвращаясь к своему примеру с определением типа, вы сделали возможным различение между Flag _ и Int _.Таким образом, я могу написать следующую общую функцию 

 let empty (Arg _) = ""
 let map_empty = Array.map empty

и ожидать, что map_empty работает на всех типизированных массивах.Но я не могу применить эту функцию к вашему смешанному массиву 

 let args = [|
   Arg "hello";
   Flag {name = "foo"; payload = Some "world"};
 |]

Другими словами, этот массив не может быть хорошо типизирован.

0 голосов
/ 23 ноября 2018

Обычный способ справиться с этой ситуацией с помощью GADT - это ввести экзистенциальные оболочки (здесь any_word): 

type flag = {
  name : string;
  payload : string option;
}

type _ word =
  | Arg : string -> string word
  | Flag : flag -> flag word

type any_word = Word : _ word -> any_word [@@unboxed]

let args = [|
  Word (Arg "hello");
  Word (Flag {name = "foo"; payload = Some "world"});
|]

args содержит word s индекса неизвестного типа, этот индекс являетсяспрятан внутри any_word оболочки.Напротив, 

let flag_args = [|
  Flag {name = "zonk"; payload = None};
  Flag {name = "splines"; payload = Some "reticulate"};
|]

flag_args содержит flag word с конкретно.string word исключены системой типов, которая является одной из достопримечательностей GADT.(Если вам это не нужно, GADT вряд ли будут вам полезны.)

0 голосов
/ 21 ноября 2018

Я, конечно, не эксперт по GADT, но это больше похоже на ограничение переменных обычного типа, чем на GADT.flag word и string word - это отдельные типы, которые не будут вписываться в один и тот же массив независимо от того, что.

Я предполагаю, что вам нужна переменная с квантифицированным типом.Если это так, переменная экзистенциального типа должна появляться только в левой части стрелки.Кажется, это работает: 

type word =
 | Arg : string -> word
 | Flag : flag -> word

Или словами руководство :

Переменные становятся экзистенциальными, когда они появляются внутри аргумента конструктора, ноне в типе возвращаемого значения.

Редактировать: Нет, поскольку @octachron указывает в комментарии, это не то, как работают экзистенциальные типы.Или скорее экзистенциальный тип переменные , которых в моем примере нет.Причина та же, но я не совсем понимаю, какое свойство GADT здесь желательно и каково будет решение.

...