使用具有更高階函數的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版本詳述。