2

我认为我找到了一种使用 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 类型参数不能有差异。这是否意味着这种方法完全没用？

4

1 回答 1

2

您只需要使用本地抽象类型就可以为每个分支细化类型：

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
于 2019-11-21T23:37:35.277 回答