OCaml でも採用されているレベルベースの多相型型推論とは

型推論 OCaml

言語実装 Advent Calendar 2017 の16日目の記事です． GoCaml という OCaml のサブセットな言語を実装していて，多相型の型推論を実装するために論文を読んだり OCaml の実装をちょっと追ったりしていたので，その知識を整理する意味でこのエントリを書いています．

この記事では OCaml の型推論器のベースになっている「レベルベースの多相型型推論アルゴリズム」について概略を直感的に説明しようと思います． 理論的になぜこのアルゴリズムで正しく動作するのかについてはこの記事で概要を把握した上で論文 のほうを読んでいただければ理解が速いと思います．

また，この記事では最もシンプルな単相型のHM型推論については知っている前提で書きます． ご存知でない場合は，

あたりに分かりやすい解説がありますので，そちらを先に読むことをおすすめします．

TL;DR

単相型と多相型

この記事で紹介する多相型型推論の多相的 (polymorphic)というのは単相的（monomorphic）に対してそもそもどう違うのかについて説明します．

単相的な型システムでは全ての値は1つの型を取ります．なので，

let id = fun x -> x in id 42

とすると引数を1つ取りそのまま返す関数 id の型は int -> int になります．なので，別の箇所で id true のように bool 型の値を引数に取ろうとすると，引数の型は int なので bool の値は渡せないとコンパイルエラーになってしまいます．

また，

let id = fun x -> x in ()

のように id が未使用だと引数および戻り値の型が確定しないためコンパイルエラーになってしまいます．これは関数だけでなく option などについても同様で，

let o = None in
o = Some 42; (* o は option int 型 *)
o = Some true; (* エラー，int v.s. bool *)

let o2 = None in ()
(* エラー，o2 の型（option の中身の型）が不明 *)

一方多相型な型システムでは値が任意の型を持つことが許されています．任意の型を取ることができる型変数（型スキームと呼ばれています）は，他の型と区別するために頭にクォートを付けて ('a, 'b, ...）のように書きます．

let id = fun x -> x in (* id の型は 'a -> 'a *)
id 42; (* ここで id の型は int -> int *)
id true; (* ここで id の型は bool -> bool *)

let id2 = fun x -> x in ();
(* id2 の型は 'a -> 'a に確定しているので未使用でも OK *)

let o = None in ()
(* o の型は option 'a *)

単相的な型システムでは id の型は定義した時点では引数と戻り値の型が同じであることしか分からず，後の id の使われ方によって型が確定します． 一方で多相的な型システムでは id を定義した時点で任意の型の引数1つを取りその型の戻り値を返す関数として型が確定します． id 関数は使われる際の引数の型によって int -> int や bool -> bool などとして扱うことができますし，定義時に型が確定しているので定義した後に使用しなくてもエラーになりません．

多相型型推論アルゴリズム

単相型HM型推論を多相に拡張したものはざっと調べただけでも3種類ほどあって，

  1. Algorithm W: 最もオーソドックス，型の集合と束縛された型変数の置換表を使って単一化する
  2. Algorithm M: Algorithm W を改善（高速化）したもの．Algorithm W が構文木をトップダウンに見て推論していく一方，Algorithm M はボトムアップに推論していく．W の逆なので M
  3. Level-based HM: level という値を導入することで置き換え表を使わず多相型を扱えるようにしたもの．アルゴリズムがシンプルになり実行効率も高い

どれも ML の let 式（変数への代入式）の右辺でのみ値が多相になります．なので let f = fun x -> x in ... の f の型は多相的ですが，(fun x -> x) 42 の fun x -> x の型はそうではありません．

今回は GoCaml で 3. のアルゴリズムを実装したので，その解説をします．

レベルベースの多相型HM型推論アルゴリズム

OCaml の型推論のベースにもなっているアルゴリズムです．論文を読んでみてもかっこいい名前とかはついていないので，ここでは単にレベルベースの Hindley-Milner 型推論アルゴリズムと呼んでいます（正式名称ではないです）．

詳細については 論文 にあります．論文内ではアルゴリズムが正しいことの証明と，Caml-Light という小さい ML のサブセットを用いた実装例が載っています． 論文内ではレベルのことを rank と呼んでいますが，この記事では OCaml の実装に合わせてレベルと呼んでいます（rank だと Rank N 多相などの他の用語と紛らわしかったのかもしれません）．

解説はいいから Real World な実装が読みたいというマッチョな方は OCaml の ctype.ml あたりを読むと良いと思います．

具体例で見てみる（関数 id）

難しい話は抜きにして，まずは具体例を見ていきたいと思います．

let id =
    fun x -> x
in
id 42;
id true

まずは解説内で用いる凡例について説明します．

  • 'まだ型が不明である'ことを表す型変数は頭に ? をつけて ?a, ?b のように表します
  • '任意の型を取れる'ことを表す型変数は頭に ' をつけて 'a, 'b のように表します
  • レベルを型変数のあとに括弧を付けて表します．たとえば ?a(1) はレベル1，'b(2) はレベル2であることを表します

基本的には単相型のHM型推論と同じで，コードを上から順に（構文木をトップダウンで）見ていきます．

まずレベルは 0 からスタートし，let 式の右辺に入った時にレベルが 1 上がります． そして右辺から戻ってきて次の式に入る時にレベルはもとの値（ここではレベル 0）に戻ります． なので，今回の例でのレベルは次のようになります．

(* level 0 *)
let id =
    (* level 1 *)
    fun x -> x
in
(* level 0 *)
id 42;
id true

それでは型推論の処理を順に見ていきます．

(* level 0 *)
let id =

まずは最初の let 式を見ます．この時点ではまだ代入の右辺の型が分からないので，id の型は ?a(0) となります．

    (* level 1 *)
    fun x -> x

次に右辺に入ります．ここでは関数を1つ定義しています．引数は1つなのでまずは ?b(1) -> ?c(1) という型になり，その戻り値が x そのままであることから ?c に ?b が代入（単一化; unification）されて fun 式の型は ?b(1) -> ?b(1) となります． ここまで（レベルという値を導入した以外は）単相型のHM型推論と同じです．

let 式の右辺を出た直後で右辺の型の 汎化(Generalization) を行います． 汎化とは，型が不明な型変数（ここでは ?b）のうち，右辺に入る前のレベルより高いレベルの型変数のみを任意の型を取れる型変数 'a に書き換える処理です． ここでは，右辺の型は ?b(1) -> ?b(1) であり，let 式のレベルは 0 ですので，?b(1) が 'a に書き換わり，右辺の型は 'a -> 'a となります．

これを id の型 ?a(0) に代入（単一化）して，id の型は 'a -> 'a となります．

(* level 0 *)
id 42

id を定義する側が型付けできたので，次は id を使う側を見ていきます．ここでは関数 id に引数 42 を適用しています．

変数が参照されるタイミングで，その変数に対してインスタンス化(Instantiation)という処理が入ります． インスタンス化は汎化と逆の処理で，型の中にある任意の型を取れる型変数 'a を型が不明な型変数 ?c に変換しながら新しい型を生成します． ここでは id の型 'a -> 'a から 'a を置き換えながら新しい型 ?c(0) -> ?c(0) を生成します．

さらに引数に 42 という int の型を与えているので ?c に int が代入（単一化）され，この関数適用式における id の型は int -> int に確定し，id 42 の型は int になります．

id true

最後の行についても同様に，'a -> 'a から 'a を置き換えながら新しい型 ?d(0) -> ?d(0) が生成され，引数 true から，この関数適用式における id の型は true -> true となります．

このようにして，任意の型を取れる型変数を含んだ変数 id に複数種類の型を与えて適用した場合でもうまく扱うことができます．

具体例で見てみる（option 型の値）

let o =
    None
in
o = Some 42;
o = Some true

前回同様にレベルをつけていきます．

(* level 0 *)
let o =
    (* level 1 *)
    None
in
(* level 0 *)
o = Some 42;
o = Some true

流れは前回とほぼ同様です．

    None

右辺の型は None 式から option ?b(1)（option の値であることは分かるが，中身の型は不明）になります．

これを汎化して，o の型は let 式のレベル 0 より高い ?b(1) を 'a に置き換えて option 'a となります．

(* level 0 *)
o = Some 42;

o を使う側の流れも大体同じです．

o を参照した時点で o の型のインスタンス化が行われ，この等値式の左辺における o の型は 'a が新しい型変数 ?c(0) に置き換わって option ?c(0) になります．さらに等値式の右辺が option int であることから，ここでの o の型は option int となります．

o = Some true

についても同様にここでの左辺 o の型は option ?d(0) になって，等値式の右辺から ?d は bool であると確定します．

もう少し複雑なケース

上記の2つのケースでは簡単すぎて，汎化する際の「レベルより高いレベルの型変数のみを任意の型を表す型変数に置換する」というのがどう効いてくるのか分からないため，もう少し複雑なケースを見てみます．

let make_pair =
    fun x ->
        let f =
            fun y -> (x, y)
        in
        f
in
let pair_with_42 = make_pair 42 in
let pair = pair_with_42 3.14 in
let pair_with_true = make_pair true in
let pair2 = pair_with_true "foo" in

make_pair は引数 xを取って，'引数y を取ってタプル x, y を返す関数' を返す関数です． 例えば，((make_pair 42) true) は int * bool な型の値 42, true を生成します． 引数を2つ取ってそのペアを返す関数がカリー化されているとも見られると思います．

ネストが深くなりちょっと複雑に見えますが，まずはレベルを明示してみます． let 式の右辺の中ではレベルが1上がるのでした． let 式が2つネストしているので，レベルは最大で2まで上がるはずです．

(* level 0 *)
let make_pair =
    (* level 1 *)
    fun x ->
        (* level 1 *)
        let f =
            (* level 2 *)
            fun y ->
                (* level 2 *)
                (x, y)
        in
        (* level 1 *)
        f
in
(* level 0 *)
let pair_with_42 =
    (* level 1 *)
    make_pair 42
in
(* level 0 *)
let pair =
    (* level 1 *)
    pair_with_42 3.14
in
(* level 0 *)
let pair_with_true =
    (* level 1 *)
    make_pair true
in
(* level 0 *)
let pair2 =
    (* level 1 *)
    pair_with_true "foo"
in
pair2

一行ずつ見ていきます．

(* level 0 *)
let make_pair =

この時点では makr_pair の型は不明なので，型は ?a(0) となります．右辺に入るのでレベルが上がります．

    (* level 1 *)
    fun x ->

この時点で引数1つであることが分かるので，外側の fun 式の型が ?b(1) -> ?c(1) となります．

        (* level 1 *)
        let f =

ここで2つ目の let 式が現れました．同様に，f の型は ?d(1) となります．ここで右辺に入るとレベルが上がります．

            (* level 2 *)
            fun y ->

さらに1引数の内側の fun 式が現れました．これもこの時点では戻り値型，引数の型ともに不明なので，同様に ?e(2) -> ?f(2) となります．

                (* level 2 *)
                (x, y)

内側の fun 式の body 部分は2要素のタプル生成式になっています．ここで外側の関数の引数と内側の関数の引数をペアにしているので，その型は ?b(1) * ?e(2) となります．

ここから，内側の関数の戻り値型 ?f に代入して 内側の fun 式の型は ?e(2) -> (?b(1) * ?e(2)) となりました．

内側の fun 式を抜けたところで内側の let 式の右辺を抜けるので，右辺の型 ?e(2) -> (?b(1) * ?e(2)) を汎化します．let 式のレベルは 1 ですすから，1 より 大きいレベルの型変数を任意の型を取れる型変数に置き換えます． 結果として，内側の let 式の右辺の型は ?e(2) が 'a に置き換わり，'a -> (?b(1) * 'a) になります．?b はレベル1なのでまだそこに何の方が来るかは不明なままです．

これによって内側の関数 f の型は ?d に代入（単一化）して 'a -> (?b(1) * 'a) となりました．

        (* level 1 *)
        f

次に外側の fun 式に戻ってきました．ここでは戻り値が f となっています． これによって，外側の fun 式の型は ?b(1) -> ?c(1) の ?c に f の型である 'a -> (?b(1) * 'a) を代入（単一化）し，?b(1) -> 'a -> (?b(1) * 'a) となります．

外側の fun 式を抜けると，ようやく外側の let 式を抜けることができたので，ここで外側の let 式の右辺の型 ?b(1) -> 'a -> (?b(1) * 'a) を汎化します． 外側の let 式のレベルは 0 なので，?b(1) が任意の型を取れる型変数に置き換わり，'b -> 'a -> ('b * 'a) となります．

これを make_pair の型 ?a に代入（単一化）して make_pair の型は 'b -> 'a -> ('b * 'a) となりました．

次に使われている箇所を見ていきます．

(* level 0 *)
let pair_with_42 =
    (* level 1 *)
    make_pair 42
in

let 式の右辺の内側で make_pair を参照しています．変数が参照される箇所ではインスタンス化が起こるのでした． make_pair の型の中の任意の型を取れる型変数を型が不明な型変数に置き換えて，'b -> 'a -> ('b * 'a) が ?g(1) -> ?h(1) -> (?g(1) * ?h(1)) となります．

ここに引数 42 を適用しているので，適用された make_pair の型は ?g(1) に int を代入して int -> ?h(1) -> (int * ?h(1)) となります． よってこの関数適用の結果の型は ?h(1) -> (int * ?h(1)) となります．

ここで let 式を抜けるのでレベル0で ?h(1) が汎化され，pair_with_42 の型が 'c -> (int * 'c) となりました． ちゃんと最初の引数が int であったことが反映された型になっています．

(* level 0 *)
let pair =
    (* level 1 *)
    pair_with_42 3.14
in

次の let 式もほぼ同様ですが，変数参照 pair_with_42 の型は 'c -> (int * 'c) をインスタンス化して ?i(1) -> (int * ?i(1)) となり，float 型で関数適用されているので，関数適用の結果は (int * float) となります． ここで let 式を抜けて，型変数は右辺の中になくなったので汎化では特に何も起こらず，pair の型は (int * float) となり正しく型を付けることができました．

これとまったく同様にして，pair_with_true と pair2 の型はそれぞれ 'd -> (bool * 'd) と (bool * string) となります． よって，多相な関数を返す多相な関数についても呼び出しごとに正しく型が付けられている（引数の型を変えて呼び出しても正しく型を付けられている）ことが分かりました．

そもそもレベルとは何か

今まで特に深くは言及せずレベルを使ってきましたが，つまるところこのレベルとは何を表すのでしょうか．

レベルは実は 'freshness' を表しています．ある型変数 '?a' が導入された時に，型変数の数値が大きいほど，その型変数が新しいことを示しています． これと「let 式のレベルより高いレベルの型変数のみを任意の型を表す型変数に置換する」という汎化の条件をあわせることで，let 式よりも外の変数由来の型変数 ?a が，その let 式で汎化されて 'a になることを防ぎ，let 式の中で定義された変数由来の型変数のみを任意の型を取れる型変数として汎化するようにしています．

例えば直前の少し複雑な例で，外側のfun 式の戻り値を f から x = y; f にしてみましょう． x と y を比較している（= は等値式）ことから，x と y は同じ型であることが期待されています． 上記の例の x の型 ?bは内側の let 式では汎化されず ?b のまま残っていますので，x = y の時点で y の型 'a を代入（単一化）することができ，x の型は正しく 'a となります． もし ?b が内側の let 式の時点で 'b となってしまったら，x の型が y の型と同じという情報は反映されなくなってしまうでしょう．

再帰

このアルゴリズムを実装していく上で少しハマったので，ここで紹介しておきます．再帰の場合です．

(* level 0 *)
let rec foo =
    (* level 1 *)
    fun x -> if true then 42 else (foo 10)
in

問題なのは if 式の中で foo が再帰的に呼ばれているところです．

順を追って見ていきます．

まず foo の型は ?a(0) として定義され，let の右辺に入ります．

次に fun 式の型を ?b(1) -> ?c(1) とし，関数の本体に入ります．

ここで foo は int 1引数の関数であることが判明するので foo の型 ?a(0) は int -> ?d(1) となります．

さらに if 式の then 節が int なことから，foo の型は int -> int となり，fun 式の型は ?b(1) -> int となります．

最後に let 式を抜け，汎化されて 'a -> int となりますが，すでに foo の式は int -> int だと判明しているので，単一化により foo は int -> int になってしまいます．

つまり，foo は一見 'a -> int となっても良さそうに見えますが，実際は再帰していて引数の型が関数本体内で判明している場合は，その関数は多相になりません． なので，foo 3.14 のように呼び出そうとするとコンパイルエラーになります．

OCaml では let rec foo: 'a -> int のように型を明示してやることでこれを回避できるようです．

エッジケースをカバーするためのレベルの調整

ここまで説明したアルゴリズムで概ねうまく動きますが，実はうまく動かないエッジケースがあり，それを解消するために型変数のレベルを調節する処理が単一化をする際の occur check の中にあります． occur check は単一化しようしている2つの型のうち一方が他方に含まれていないかをチェックする処理ですが，チェックする2つの型が両方とも型変数だった場合に特別な処理を行います．

具体的には，もし右辺側の型変数のレベルのほうが左辺側の型変数より大きい時，右辺側のレベルを左辺側のレベルに合わせます． なので，

e1 = e2
(* e1 の型は ?a(1) -> int *)
(* e2 の型は ?b(2) -> int *)

という等値式があった場合，e1 と e2 の型は同じであるはずなので単一化を行いますが，この時 e2 の型は ?b(1) -> int に書き換わります．これによって汎化が正しく行われます．

型推論が実装できた次に待っているもの

ここまででレベルベースの多相型型推論は終わりです．しかし，型推論を実装しただけでは多相型は実装できません． 実際には任意の型を取れる型の値をどうアセンブラに落とすかや，後から変更できる値の扱いをどうするかなどの問題が残っています． 本当はそこまで書きたかったのですが，実装が終わっていないので概略のみを書きます．

汎化された値のコード生成

let f = fun x -> x in f 10; f true

というコードがあった時，x の値は実際はどのようなアセンブリコードに落とせば良いでしょうか．やり方は大きく3つあります．

1. 任意の型の値を1ワードで表現する

任意の型の値が1ワード（数値は64bit整数や浮動小数点数，それ以外はポインタ）とすれば，f は単に1ワードの引数を取る関数としてコード生成できます．値の型によって処理を分岐する必要があるので，アクセスする時にオーバーヘッドが発生します．

2. 'a が取りうる型ごとに型を具体化してしまう

let f_int = fun (x:int) -> x in
let f_bool = fun (x:bool) -> x in
f_int 10;
f_bool true

のように，取りうる型ごとに別の関数を定義してしまいます．バイナリサイズが大きくなったり分割コンパイルが困難になりますが，オーバーヘッドは値にアクセスする際にオーバーヘッドが発生しません．

3. 型クラスを定義できるようにし，引数が実装している型クラスの処理に対応する辞書を f に別途渡す

Haskell などで採用されている方式です．足し算ができることを表す型クラス Add があって下記のように f を定義したとき，

let f = fun (x: Add) -> x + x in f 10; f 3.14

コード生成では int や float の Add 実装（足し算処理）を辞書として f の隠し引数に渡してやり，それを関数内で使って + の処理を行います．

値制約

例で説明したケースでは問題ありませんでしたが，実は多相型型推論は変数が可変な場合にうまく行きません．

(* 空の配列を可変な変数 a に束縛 *)
let a = ref [| |] in
(* true を要素に持つリストを代入し直す *)
a := [| true |];
(* 最初の要素は true であるはずなのに 42 と足せてしまう *)
42 + a.(0)

これを避けるために，値制約（value restriction）を導入します．let 式の右辺に特定の式が来た場合は汎化を行わないという制限を加えることで，これを回避します． 上記の例では ref があるときは汎化を行わず，a は array ?a になって後の代入式で array bool が確定するので a.(0) の型は bool となり，無事 42 と足すところでエラーになります．

まとめ

レベルベースな多相型型推論のアルゴリズムについて順を追って詳細に説明してみました． 初めてこのアルゴリズムを見る人にも理解しやすいようにしたつもりです． 自作言語などで単相型の型システムから多相型に拡張する際などに参考にしていただけると幸いです．