使用具有更高阶函数的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 = 
    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 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真的，就此而言），但从我的理解来看，这些错误似乎是由于t顾名思义，他的类型就是“本地”，虽然外部是多态的，但通过它会“泄漏”它，我猜？

所以我的问题是，首先是：这甚至可能做（和“本”我想我的意思是就在高阶函数一个GADT模式匹配，但我甚至不知道这是真正的问题）？

Playground with all the code here

Answer 1

这里有两个根本问题（这是一个位由GADTs的存在混乱）。第一个问题是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）中进行，因此我们不能只改变replaceNode中的f的类型。但是，通过使用多态记录字段或方法可以解决此问题。

例如，使用记录路径，我们可以定义一个记录类型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 

但随后的第二个问题弹出：此replaceNode功能有 mapper -> inline node -> inline node类型。内联类型从哪里来？这个问题的时间是polymorhpic递归。如果没有明确的多态注释，其递归定义中认为replaceNode的类型是常量。换言之，类型检查器认为replaceNode对于类型为mapper -> 'elt node -> 'elt node具有'elt。在paragraph和strong分支中，children列表是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上进行模式匹配时进行细化。换句话说，我们需要它的精确，在Paragraph，Strong和Text类型a遵循不同的等式：a = block段落分支，a =在Strong和Text分支inline。

编辑：如何定义一个映射器？

这个本地抽象类型位在定义映射器时非常重要。 例如，限定

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

产生了一个类型为inline node -> inline node optionf，由于在构造Text匹配产生了平等'type_of_scrutinee=inline。

要纠正这一点，一个需要添加本地抽象类型注释 使类型检查能够细化scrutinee分支的分支类型：

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

那么这f有正确的类型和可以包裹映射器记录内部：

let f = { f } 

广告：所有这一切都在OCaml的手动起动4.06版本详述。