Сопоставление с образцом в GADT не удается

Question

Я немного поигрался с ReasonML и нашел сопоставление с образцом на type t из следующего примера, чтобы не работать с ошибкой

Ошибка: этот шаблон соответствует значениям типа t(float), но ожидался шаблон, который соответствует значениям типа t(int) Тип float несовместим с типом int

  type t('a) =
    | One: t(int)
    | Two: t(float);

  let x =
    fun
    | One => None
    | Two => None;

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

Я нашел ответ (думаю) на равноценный вопрос. Для второго раздела ответ, похоже, заключается в игнорировании привязанного типа конструктора. Возможно ли то же самое в ReasonML?

Ps: поправьте пожалуйста меня педантично по терминологии, пока учусь что к чему.

Pps: Я знаю, что могу обойти исходную проблему, явно набрав x но мне очень нравится fun синтаксис, потому что это весело.

Answer 1

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

let one = (One) => None
let two = (Two) => None

Вы можете проверить их общее количество, добавив пункт явного опровержения в синтаксисе OCaml (синтаксис Reason еще не обновлен, чтобы включить его):

let one = function
| One -> None
| _ -> .

Вот точка . означает, что шаблон, описанный в левой части предложения, синтаксически действителен, но не относится к какому-либо фактическому значению из-за некоторых ограничений типа.

Следовательно, вам необходимо сообщить средству проверки типов, что вы собираетесь сопоставить значение типа t(a) для любого a, это нужно делать с локально абстрактными типами:

let x (type a, (x:t(a))) = switch(x){
| One => None
| Two => None
}

С этой локально абстрактной аннотацией средство проверки типов знает, что не предполагается заменять эту переменную. a конкретным типом глобально (он же должен учитывать, что локально a неизвестный абстрактный тип), но он может уточнить его локально при сопоставлении с GADT.

Строго говоря, аннотация нужна только на выкройке, поэтому вы можете написать

let x (type a) = fun
| (One:t(a)) => None
| Two => None

Обратите внимание, что для рекурсивных функций с GADT вам может потребоваться использовать полные явно полиморфные локально абстрактные обозначения типов:

type t(_) =
| Int(int): t(int)
| Equal(t('a),t('a)):t(bool)

let rec eval: type any. t(any) => any = fun
| Int(n) => n
| Equal(x,y) => eval(x) = eval(y)

где разница в том, что e val рекурсивно полиморфен. См. https://caml.inria.fr/pub/docs/manual-ocaml-4.09/polymorphism.html.

РЕДАКТИРОВАТЬ: аннотирование возвращаемого типа

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

let zero (type a, (x:t(a)) = switch (x){
| One => 0
| Two => 0.
}

Здесь есть двусмысленность, потому что внутри ветки One, проверка типов знает, что int=aно выходя из этого контекста, он должен выбрать ту или иную сторону уравнения. (В этом конкретном случае, оставленный на собственном устройстве, проверка типов решает, что(0: int) это более логичный вывод, потому что 0 является целым числом, и этот тип никоим образом не контактировал с локально абстрактным типом a.)

Этой неоднозначности можно избежать, используя явную аннотацию, либо локально

let zero (type a, (x:t(a))) = switch (x){
| One => ( 0 : a )
| Two => ( 0. : a )
}

или в целом функция

let zero (type a): t(a) => a = fun
| One => 0
| Two => 0.

Answer 2

Кто-то, вероятно, скоро придет и даст правильное объяснение, но краткий ответ заключается в том, что вам нужно использовать локально абстрактный тип вместо переменной типа.

let x: type a. t(a) => option(a) =
  fun
  | One => None
  | Two => None;

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

Вывод типа для GADT, как известно, сложен. Это связано с тем, что некоторые типы могут стать неоднозначными при выходе из ветки. Например, в приведенном выше случае Int, n может иметь тип int или a, и они не эквивалентны вне этой ветви. В первом приближении вывод типа будет всегда работать, если сопоставление с образцом аннотировано типами, не содержащими переменных свободного типа (как для проверяемого, так и для возвращаемого типа). Так обстоит дело в приведенном выше примере благодаря аннотации типа, содержащей только локально абстрактные типы.