Arantium Maestum

プログラミング、囲碁、読書の話題

OCamlでの相互再帰的なPolymorphic Variantに関するメモ

OCaml

発端は@dico_lequeさんのこのツイート

そしてこのツイート

後者に関しては「何が起きてるのかまったくわからん」となってショックだったので、色々調べたりいじったりしてみて少しわかってきたのでメモ。

何が問題なのか

S式をうまくOCamlの代数的データ型で表現する場合の考えどころの一つとしてDotted Listをどう扱うかという問題がある。

Dotted Listとは例えば(a b c . d)のようなもので、分解すると(cons a (cons b (cons c d)))という、consセルから作られるリストの最後の要素がnilではないもののことを指す。

このdに当たる要素は任意の値をとることができないのが難しいポイント。というのも(a b c . (d e f))や(a b c . (d e . f))という式はあり得ない。それらを正しく表現しようとするなら(a b c d e f)や(a b c d e . f)となるからだ。（consセルに直してみればわかりやすいと思う）

つまり

type t =
Int of int
Str of string
Symbol of string
List of t list
DottedList of t list * t

という定義にしてしまうとDottedList of t list * tの最後のtが受け入れてはいけない値（ListやDottedList）も受け入れてしまう問題が出てくる。

これを解決するための一案としてPolymorphic Variantを使ってみる：

type atom =
[ `Int of int
| `Str of string
| `Symbol of string
]

type t =
[ atom
| `List of t list
| `DottedList of t list * atom
]

Polymorphic variantというのは「バリアントのケース（例えば`Str）が一つ以上の型のメンバになりえる」という型機能である。Int、Str、Symbolはatomとtのどちらにも属する事になる。そしてDottedListの最後の要素はatom型に属する値のみ許容される。

さて、上記の定義だとatomの定義のなかにtは出てこないので再帰性はない。のでPolymorphic Typeだけで比較的簡単に実装できる。

しかしatomの定義に| Vector of t arrayのようなtを要素として持ちえるバリアントを追加すると問題が起きる。atomとtで相互再帰の形になり、@dico_lequeさんの最初のツイートのようにError: The type constructor atom is not yet completely definedと怒られてしまう。つまりこういう型定義は受け入れられない：

type atom =
[ `Int of int
| `Str of string
| `Symbol of string
| `Vector of t array
]
and t =
[ atom
| `List of t list
| `DottedList of t list * atom
]

これには簡単な解決法があって、tの定義時にatomのバリアントのケースを明示的に書いてしまえばいい：

type atom =
[ `Int of int
| `Str of string
| `Symbol of string
| `Vector of t array
]
and t =
[ `Int of int
| `Str of string
| `Symbol of string
| `Vector of t array
| `List of t list
| `DottedList of t list * atom
]

これだとエラーは起きないので、元々のコードでError: The type constructor atom is not yet completely definedと怒られているのはtype t =[ atom | ...]の部分に関してで、DottedList of t list * atomの部分は問題ないことがわかる。

ただ、これは例えばNilなどの新しいバリアントケースを追加したいときに必ずatomとtの両方を変更しないといけない上に、うっかり片方しか変えてない場合に型検査で引っかからないので微妙である。

じゃあどうするか、というのが今回の「解決したい問題」。

type variableとtype constraintとobject type

それではその解決法である以下のコード（@dico_lequeさんの二つ目のツイートをフォーマットしたもの）について見ていく：

type 'd atom = 
[ `Int of int
| `Vector of 't
] constraint 'd = <t : 't; atom : 'atom>

type 'd s =
[ 'd atom
| `List of 't list
| `DottedList of 't list * 'atom
] constraint 'd = < t : 't; atom : 'atom>

type d = <t : d s; atom : d atom>

type t = d s

まずtを定義するのに別の型sを使っているのがわかる。その上でsとatomはどちらも型変数'dを取る形になっている。

型変数を使うことによってatomの定義ではsやtを使わず、型変数から持ち込まれた'tという型を使ってVectorが定義されている。

sの方は'd atomという形で型変数ではなく定義されたatom自体を使っていて、これは型変数に入れ替えることはできない。というわけで定義の順は変更できないが、少なくとも相互再帰は崩せていて、その結果エラーはなくなっている。

このコードの面白いところはconstraint 'd = <t : 't; atom : 'atom>で、冒頭でも書いたとおりここは初見では私はまったく理解できなかった。

まず<t : 't; atom : 'atom>はOCamlのオブジェクト型で、これ自体私は初めて見た。OCamlのドキュメントのオブジェクト関連の部分でもこのフォーマットについてはあまり詳しく解説していなかった（1行だけ言及はあった）上に今までオブジェクト使ってるコード読んだことなかったから・・・

type 'a b = .... constraint 'a = ...という構文は'aという型変数の形を束縛するもので、つまりconstraint 'd = <t : 't; atom : 'atom>は'dというのはオブジェクト型で't型のtと'atom型のatomというデータメンバを持つ、と束縛しているわけだ。これによりtype 'd atomの定義の中で'atomと'tという型変数が使えるようになる。

簡略化

ここまでは「あのコードって何が起きてるんだろう」という疑問に答えるためのものだったが、それをベースに「このケースに関してはより簡潔な記述が可能」という話をする。

まず、Object typeを使うことで型変数にデータメンバとしての明示的な名前が付けられることがメリットのようだが、単に複数の型変数を導入したいだけならタプルや関数でも良い：

type 'd atom = 
[ `Int of int
| `Vector of 't
] constraint 'd = 't *  'atom

type 'd s =
[ 'd atom
| `List of 't list
| `DottedList of 't list * 'atom
] constraint 'd = 't *  'atom

type d = d s * d atom

type t = d s

さて、type 'd sの定義では'atom型変数を使っているが、よく見ると必要ないことがわかる：

type 'd s =
[ 'd atom
| `List of 't list
| `DottedList of 't list * 'd atom
] constraint 'd = 't *  'atom

'atomではなく'd atomにしてしまえば良い。この時点で'atomという型変数はどこにも使われていないので取り除くことができる：

type 'd atom = 
[ `Int of int
| `Vector of 't
] constraint 'd = 't

type 'd s =
[ 'd atom
| `List of 't list
| `DottedList of 't list * 'd atom
] constraint 'd = 't

そうするとconstraint 'd = 'tの部分も冗長になる（そもそも型変数一つしか使わないのでconstraintを使う必要がない）：

type 't atom = 
[ `Int of int
| `Vector of 't
]

type 't s =
[ 't atom
| `List of 't list
| `DottedList of 't list * 't atom
]

type t = t s

そして最終的にsという型を定義せずとも直接tが定義できる（tの定義自体は再帰的にできるため）：

type 't atom = 
[ `Int of int
| `Vector of 't
]

type t =
[ t atom
| `List of t list
| `DottedList of t list * t atom
]

このように相互再帰的な型が二つだけの場合はconstraintを持ち出すまでもなく解決できることがわかった。

元の解法はより多くの相互再帰により型変数を複数用意しなくてはいけない時に真価を発揮する。例えばatomとlistとvectorとvalueを用意して、どこにどの型が含まれうるかが複雑だったりする場合は、すべての相互再帰的な型の数だけ型変数をconstraintで用意する必要が出てくる。それだけ複雑な型の集まりを定義する機会があるかどうかはわからないが・・・

ちなみにネタの大元はこのissue：

github.com