Моделирование грамматики с помощью GADT, но параметр типа не унифицируется

Question

Я подумал, что нашел изящный способ моделирования грамматик с использованием GADT, предоставив каждому конструктору (например, Char) параметр возвращаемого типа, который является полиморфным вариантом (например, [`Char] t), а затем с помощью функции унификации полиморфных вариантов, чтобы ограничить допустимые конструкторы следующими (например, [<`Minus | `Char] t).

(* Grammar ::= Open (Minus? Char)+ Close *)

type _ t =
  | Open:  [<`Minus | `Char] t -> [`Open] t
  | Minus: [<`Char] t -> [`Minus] t
  | Char:  [<`Minus | `Char | `Close] t -> [`Char] t
  | Close: [`Close] t

Это работает по назначению, разрешая только те последовательности, которые соответствуют грамматике:

let example =
  Open (Minus (Char (Char (Minus (Char (Close))))))

(* let counter_example =
  Open (Minus (Char (Minus (Minus (Char (Close)))))) *)

Однако написать какую-либо тривиальную функцию для этого типа невозможно:

let rec to_list = function
  | Open rest -> "(" :: to_list rest
  | Minus rest -> "-" :: to_list rest
  | Char rest -> "a" :: to_list rest
  | Close -> [")"]

File "./tmp.ml", line 21, characters 4-14:
21 |   | Minus rest -> "-" :: to_list rest
         ^^^^^^^^^^
Error: This pattern matches values of type [ `Minus ] t
       but a pattern was expected which matches values of type [ `Open ] t
       Type [ `Minus ] is not compatible with type [ `Open ]

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

Answer 1

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

let rec to_list : type a. a t -> string list = function
  | Open rest -> "(" :: to_list rest
  | Minus rest -> "-" :: to_list rest
  | Char rest -> "a" :: to_list rest
  | Close -> [")"]

Для объяснения, @octachron написал отличный ответ на аналогичный вопрос ранее сегодня.

Редактировать:

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

Я могу придумать несколько способов сделать это:

Вариант 1, оберните его в модуль (или поместите внешнюю подпись в.mli):

module M : sig
  val to_list : [<`Minus | `Char | `Close] t -> string list
end = struct
  let rec to_list : type a. a t -> string list = function
    | Open rest -> "(" :: to_list rest
    | Minus rest -> "-" :: to_list rest
    | Char rest -> "a" :: to_list rest
    | Close -> [")"]
end

Вариант 2, используйте локально определенную функцию, чтобы поставить "внутреннюю" подпись:

let to_list : [<`Minus | `Char | `Close] t -> string list =
  let rec aux : type a. a t -> string list = function
    | Open rest -> "(" :: aux rest
    | Minus rest -> "-" :: aux rest
    | Char rest -> "a" :: aux rest
    | Close -> [")"]
  in
  aux