使用具有更高阶函数的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

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

这个表达式有类型块节点 - >一个节点选项但是表达式需要类型块节点 - >一个节点选项这个块的实例是不明确的:它会逃避它的等式范围

或者,如果我改变的类型f来'a node -> 'a node option我得到这个错误,而不是

此表达式具有类型的节点,但是表达式需要类型为节点类型构造函数a将转义其范围

很明显,我并不完全理解本地抽象类型(或GADT真的,就此而言),但从我所理解的这些错误似乎出现,因为类型是,顾名思义,"本地",并且虽然多态在外面,传递它会"泄漏"它,我想？

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

游乐场里有所有代码

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;;

产生一个更直接的错误:

错误:此表达式具有类型内联节点,
但表达式类型为节点
类型内联与类型a不兼容

因此问题在于我们需要确保f适用于任何类型a而不仅仅是原始类型的类型检查器a.换句话说,类型f应该是'a. 'a node -> 'a node option(aka forall 'a. 'a -> 'a node option).不幸的是,显式多态注释只能在OCaml的第一个位置(prenex)中使用,因此我们不能只改变fin 的类型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

但随后弹出第二个问题:此replaceNode函数具有类型 mapper -> inline node -> inline node.内联类型来自哪里？这个问题的时间是多重递归.如果没有明确的多态注释,则replaceNode在递归定义中将类型视为常量.换句话说,类型检查器认为对于给定replaceNode类型具有类型.在和分支中,列表是一个列表.因此,对于类型检查器意味着= 并且因此类型变为.mapper -> 'elt node -> 'elt node 'eltparagraphstrongchildreninline nodeList.map (replaceNode {f}) children'eltinlinereplaceNodemapper -> 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有正确的类型,可以包装在mapper记录中:

let f = { f }

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