高次関数を持つ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

に次のエラーを与えるか、私は'a node -> 'a node optionへfの種類を変更する場合、私は

代わりにこのエラーが出ます

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の存在によって混乱ビットです）ここでは2つのルートの問題があります。第1の問題は、replaceNodeが第2位の多型関数であることである。実際、最初の試合ではa nodeのノードにfが適用されますが、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）である必要があります。 Unfortunalety、明示的な多型アノテーションは、OCamlの最初の位置（prenex）でのみ可能であるため、replaceNodeのfの型を変更することはできません。ただし、この問題を回避するには、多態的なレコードフィールドまたはメソッドを使用することができます。

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

フィールド f右明示的多型表記（別名ユニバーサル定量）を有するの

、次いでreplaceNodeでそれを使用する：

例えば、レコードのパスを使用して、我々は、レコード・タイプmapperを定義することができます。

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の場合、が'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.…は、ローカル抽象型と明示的多型アノテーションを組み合わせるためのショートカット表記であることに注意してください。

GADTでのパターンマッチングで抽象タイプのみを洗練することができるため、ここでは説明を完了するためにローカル抽象的(type a)が必要です。言い換えれば、我々は正確にそれを必要とするParagraph、StrongとTextでタイプaが異なる等式に従うこと：段落のブランチで= blocka、a = inlineStrongとTextブランチに。

EDIT：マッパーを定義する方法は？

このローカル抽象型ビットは、マッパーを定義するときに実際に重要です。

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

を定義例えば は、平等'type_of_scrutinee=inlineをもたらすTextコンストラクタ上に一致するので、fの型inline node -> inline node optionをもたらします。

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

はその後、このfがあります

この点を修正するには、1つの必要がscrutinee系統別の種類を絞り込むことが型チェッカができ作るために、ローカルに抽象型注釈 を追加します右のタイプとマッパーレコード内にラップすることができます。

let f = { f } 

広告：このすべては、バージョン4.06で始まるOCamlのマニュアルの詳細です。