pattern-matching - 使用 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 写了 a great answer今天早些时候针对类似问题对此进行了解答。

编辑:

要将此函数限制为案例的子集，我认为您必须应用两种不同的类型签名。一种用于多态变体的外部签名，一种用于局部抽象类型的内部签名。然而，由于该函数是递归的，因此当我们对其进行递归时，我们还需要局部抽象类型是外部的。否则我们可以只注释模式匹配的值。

我可以想出几种方法来做到这一点:

选项 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