types - 使用具有高阶函数的 GADT

Question

我正在尝试建模“异构树”，即。一棵树，其中节点具有不同的“种类”，并且每个“种类”都被限制在它们可能包含的子“种类”中:

type id = string
type block
type inline

type _ node =
  | Paragraph : id * inline node list -> block node
  | Strong : id * inline node list -> inline node
  | Text : id * string -> inline node

然后可以像这样定义树:

let document =
    Paragraph ("p1", [
      Text ("text1", "Hello ");
      Strong ("strong1", [
        Text ("text2", "Glorious")
      ]);
      Text ("text3", " World!")
  ])

通常这将使用每种“类型”节点的单独变体来完成，但我试图将其定义为 GADT，以便能够使用模式匹配每种节点的高阶函数来操作树:

function
  | Text ("text2", _) ->
    Some (Text ("text2", "Dreadful"))
  | _ ->
    None

我遇到的问题是定义接受上述高阶函数并将其应用于每个节点的函数。到目前为止，我有这个:

let rec replaceNode (type a) (f: a node -> a node option) (node: a node): a node =
匹配 f 节点
|一些其他节点 -> 其他节点
|无 ->
匹配节点
|段落(id，children)->
段落 (id, (List.map (replaceNode f) children))
|强(id， child )->
强 (id, (List.map (replaceNode f) children))
|文本 (_, _) -> 节点

但是编译器在突出显示的行上给了我以下错误

This expression has type block node -> a node option but an expression was expected of type block node -> a node option This instance of block is ambiguous: it would escape the scope of its equation

或者如果我更改 f 的类型至 'a node -> 'a node option我得到了这个错误

This expression has type a node but an expression was expected of type a node The type constructor a would escape its scope

显然，我并不完全理解本地抽象类型(或真正的 GADT，就此而言)，但据我所知，这些错误似乎出现了，因为该类型，顾名思义，是“本地的”，而在在外面，传递它会“泄漏”它，我猜？

所以 我的问题是 ，首先:这甚至可能做到吗(并且“这个”我认为我的意思是在高阶函数中对 GADT 进行模式匹配，但我什至不确定这是否是实际问题)？

Playground with all the code here

Answer 1

这里有两个根本问题(由于 GADT 的存在而有些困惑)。第一个问题是 replaceNode是二阶多态函数。确实，在第一场比赛中，f应用于 a node 类型的节点, 但在 Paragraph 内分支，它应用于类型为 inline node 的节点. List.map 这里的类型检查器错误有点复杂调用，但将函数重写为

let rec replaceNode (type a) (f:a node -> a node option) 
(node:a node): a node =
  match f node with
  | Some otherNode -> otherNode
  | None ->
    match node with
    | Paragraph(id, []) -> Paragraph(id,[])
    | Paragraph (id, a :: children) -> 
      Paragraph (id, f a :: (List.map (replaceNode f) children))
    | Strong (id, children) ->
      Strong (id, (List.map (replaceNode f) children))
    | Text (_, _) -> node;;

产生一个更直接的错误:

Error: This expression has type inline node
but an expression was expected of type a node
Type inline is not compatible with type a

因此问题是我们需要向类型检查器保证 f适用于任何类型 a不仅是原始类型 a .换句话说， f 的类型应该是 'a. 'a node -> 'a node option (又名 forall 'a. 'a -> 'a node option)。不幸的是，显式多态注释只能在 OCaml 中的第一个位置(prenex)，因此我们不能只更改 f 的类型在 replaceNode .但是，可以通过使用多态记录字段或方法来解决此问题。

例如，使用记录路径，我们可以定义记录类型 mapper :

type mapper = { f:'a. 'a node -> 'a node option } [@@unboxed]

其中字段 f具有正确的显式多态符号(又名通用量化)，然后在 replaceNode 中使用它:

let rec replaceNode (type a) {f} (node: a node): a node =
  match f node with
  | Some otherNode -> otherNode
  | None ->
    match node with
    | Paragraph (id, children) -> 
      Paragraph (id, (List.map (replaceNode {f}) children))
    | Strong (id, children) ->
      Strong (id, (List.map (replaceNode {f}) children))
    | Text (_, _) -> node

但随后弹出第二个问题:this replaceNode函数具有类型 mapper -> inline node -> inline node .内联类型从何而来？这次问题是多态递归。如果没有明确的多态注释， replaceNode 的类型在其递归定义中被认为是常数。换句话说，类型检查器认为 replaceNode具有类型 mapper -> 'elt node -> 'elt node对于给定的 'elt .在 paragraph和 strong分支， children list 是 inline node 的列表.因此 List.map (replaceNode {f}) children 'elt 对类型检查器意味着= inline因此 replaceNode 的类型变成 mapper -> inline node -> inline node .

为了解决这个问题，我们需要添加另一个多态注释。好在这一次，我们可以直接添加:

let rec replaceNode: type a. mapper -> a node -> a node =
  fun {f} node -> match f node with
  | Some otherNode -> otherNode
  | None ->
    match node with
    | Paragraph (id, children) -> 
      Paragraph (id, (List.map (replaceNode {f}) children))
    | Strong (id, children) ->
      Strong (id, (List.map (replaceNode {f}) children))
    | Text (_, _) -> node;;

最后，我们得到一个类型为 mapper -> 'a node -> 'a node的函数。 .
请注意 let f: type a.…是结合局部抽象类型和显式多态注释的快捷表示法。

完成解释，本地摘要 (type a)在这里需要，因为在 GADT 上进行模式匹配时，只能细化抽象类型。换句话说，我们需要精确的类型 a在 Paragraph , Strong和 Text服从不同的等式: a = block在段落分支中， a = inline在 Strong和 Text分支。

编辑:如何定义映射器？

这个局部抽象类型位实际上在定义映射器时很重要。
例如，定义

let f = function
  | Text ("text2", _) -> Some (Text ("text2", "Dreadful"))
  | _ -> None

产生一个类型 inline node -> inline node option对于 f , 因为匹配构造函数 Text产生等式 'type_of_scrutinee=inline .

为了纠正这一点，需要添加一个本地抽象类型注释
使类型检查器能够逐个分支细化检查者的类型:

 let f (type a) (node:a) : a node option= match node with
 | Text ("text2", _) -> Some (Text ("text2", "Dreadful"))
 | _ -> None

然后这个 f 具有正确的类型，并且可以包装在映射器记录中:

let f = { f }

广告:从 4.06 版本开始的 OCaml 手册中详细介绍了所有这些内容。