『プログラミング言語の基礎概念』で型推論を実装する

出版社のページ

プログラマーとして働いておきながらいまさら「基礎」かと思われそうなタイトルの本書ですが, 「プログラミングの基礎」ではなく「プログラミング言語の基礎」であることがポイントです.
プログラミング言語を数学的に厳密に扱う意味論や, エラーを事前に検知するための型システムについての本で, プログラミングの入門本ではありません.

本書では序盤中盤に書けて, プログラミング言語分析のための枠組みについての説明がされていますが, メインは型システム, 型推論だと思います.
プログラムの実行や型推論の仕組みについて厳密に扱う方法を知りたい方におすすめです. 対象としている言語は OCaml なので, ある程度 OCaml についての知識があったほうが理解がスムーズだと思います. 分析については基礎から解説してあるので, 前提知識は不要です.

導出システムについて

本書ではプログラムを厳密に扱うための枠組みとして導出システムを使います. 導出システムとは, 定義されたいくつかの規則に従って定理を導出する記述体系です.

本書の流れに沿って, 実際のプログラミング言語を扱う前に, 自然数の加算乗算を対象とした導出システムの例を見ていきます.
自然数を対象とした導出システム (natural numbers から Nat と名付けられている) では簡単のために S(...S(Z)...) のような記法で自然数を表します. 例えば以下のような感じです.

1
2
3

0 -> Z
1 -> S(Z)
2 -> S(S(Z))

導出システムによって導出される結論を「判断」と言います. Nat での判断は以下の 2 つの形です.
n1, n2, n3 は自然数で, 2 つの判断はそれぞれ加算と乗算に対応しています.

1
2

n1 plus n2 is n3
n1 times n2 is n3

式を変形するための規則「推論規則」は以下の 4 つです.

1
2
3
4
5
6
7

plus のための推論規則
P-Zero: Z plus n is n
P-Succ: n1 plus n2 is n3 ならば S(n1) plus n2 is S(n3)

times のための推論規則
T-Zero: Z times n is Z
T-Succ: n1 times n2 is n3 かつ n2 plus n3 is n4 ならば S(n1) times n2 is n4

この推論規則を使って S(S(Z)) times S(Z) is S(S(Z)) を導出してみましょう (2 * 1 = 2 に相当する判断).

1
2
3
4
5
6
7
8

S(S(Z)) times S(Z) is S(S(Z))   [T-Succ]
1 S(Z) times S(Z) is S(Z)       [T-Succ]
  1.1 Z times S(Z) is Z         [T-Zero]
  1.2 S(Z) plus Z is S(Z)       [P-Succ]
    1.2.1  S plus Z is Z        [P-Succ]
      1.2.1.1 Z plus Z is Z     [P-Zero]
2 S(Z) plus S(Z) is S(S(Z))     [P-Succ]
  2.1 Z plus S(Z) is S(Z)       [P-Zero]

S(S(Z)) times S(Z) is S(S(Z)) を導出するには T-Succ を適用して 1. S(Z) times S(Z) is S(Z)」 と 「2 S(Z) plus S(Z) is S(S(Z)) が言えれば良いことがわかります.
1. S(Z) times S(Z) is S(Z) を導出するには T-Succ を適用して 1.1 Z times S(Z) is Z と 1.2 S(Z) plus Z is S(Z) が言えれば良いです. このように, 導出に必要な判断を導出する, という操作を繰り返して, 最後には P-Zero や T-Zero に行き着きます. 木構造ですね.

1
2
3
4
5
6
7

    1
  /   \
1.1   1.2
       |
     1.2.1
       |
    1.2.1.1

2 * 1 = 2 なんだから, わざわざ面倒な導出をしなくても明らかじゃないかと思うかもしれませんが, そうではありません. Nat は現実の自然数の加算乗算をモデルにしていますが, 推論規則は加算乗算の意味を持つわけではなく, あくまでも規則に従って判断を導出して良いということのみを意味しています. Nat においてルールは P-Zero, P-Succ, T-Zero, T-Succ の 4 つしかないので, これらの規則を適用して導かれたものでなければ判断とは認められません.

OCaml を導出システムで扱う

式と値の定義

Nat で雰囲気がつかめたところで, 本題の OCaml に進みます. Ocaml は多機能ですが, 簡単のためにその中核のみを対象とした導出システムを用います. 名前は Ocaml の元であるプログラミング言語 ML から取って, ML1 とされています (後々 ML2, ML3…と拡張されます).

まず, Nat での値や式に相当するものを定義します. Nat では値を S(...S(Z)...) の形式, 式を値と +, *を組み合わせたものとしましたがやや曖昧です. 対象とする OCaml は Nat よりも複雑なので厳密な定義が必要です. 定義にはバッカス・ナウア記法 (Backus-Naur form: BNF) を使います.

1
2
3
4
5
6
7
8
9

ML1 における式 Exp と値 Value(=式の評価結果) の定義.

i  ∈ int
b  ∈ bool
v  ∈ Value := i | b
e  ∈ Exp   := i | b | e op e | if e then e else e
op ∈ Prim  := + | - | * | <

int は整数の集合, bool は true または false である.

v ∈ Value := i | b の意味を解説すると, ML1 での値 Value とは, int または bool だということです.

BNF は最初戸惑いましたが, しばらく考えると非常によくできた記法だと感じます. 再帰的に式を定義しているところ (e の定義の中に e が出てくる) がきれいにプログラムの構造を表していると思います.
BNF は導出システム専用のものと言うわけではなく, プログラミング言語の構文定義に一般的に用いられるものです (『コンピュータシステムの理論と実装』を読んだ際 にも見ました). どんなプログラムでもこれだけで表現できるというところに美しさを感じます.

式の評価

「3 + 1 * 4」は計算すると 7 になります. 「if 1 < 5 then 9 else 2」は 9 です. このように, 式を計算して値を求めることを「評価」といいます. 評価も推論規則を定義して, 規則に従って導出します.
「e が v に評価される」ということを「e evalto v」のように evalto を使って表記します. 見た目は少し複雑ですが, 規則は普通の OCaml の通りなので意味はわかると思います.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

E-Int:  i evalto i
E-Bool: b evalto b

E-IfT: e1 evalto true ∧ e2 evalto v ⇒ if e1 then e2 else e3 evalto v
E-IfF: e1 evalto false ∧ e3 evalto v ⇒ if e1 then e2 else e3 evalto v

E-Plus:  (e1 evalto i1) ∧ (e2 evalto i2) ∧ (i1 plus i2 is i3) ⇒ e1 + e2 evalto i3
E-Minus: (e1 evalto i1) ∧ (e2 evalto i2) ∧ (i1 minus i2 is i3) ⇒ e1 - e2 evalto i3
E-Times: (e1 evalto i1) ∧ (e2 evalto i2) ∧ (i1 times i2 is i3) ⇒ e1 * e2 evalto i3
E-Lt:    (e1 evalto i1) ∧ (e2 evalto i2) ∧ (i1 less than i2 is b3) ⇒ e1 < e2 evalto b3

オンライン演習システム

私はこういう説明を読むだけだと分かったような分からないような, 微妙に自信が持てない状態になるのですが, 具体例を見たり自分の手で問題を解いたりすると理解が進むことが多いです.

本書の大きな特徴に, 導出の練習ができるオンラインの演習システムがあります. 出版社の本書のページ 右上にある「演習システムへのログイン」からログインすると演習システムを利用できます (初回は新規ユーザ登録してください).

詳細は本書や上記のページなどを参照して欲しいのですが, 例えば「8 - 2 - 3 evalto 3 を導出せよ」というような問題が合計で 160 問載っています (もちろん ML1 での式の評価以外の分野も含めてです).
答えは以下のようになります. Nat の導出で例に出したような書き方を{}を使って構造化したものです.

1
2
3
4
5
6
7
8
9

8 - 2 - 3 evalto 3 by E-Minus {
  8 - 2 evalto 6 by E-Minus {
    8 evalto 8 by E-Int {};
    2 evalto 2 by E-Int {};
    8 minus 2 is 6 by B-Minus {}
  };
  3 evalto 3 by E-Int {};
  6 minus 3 is 3 by B-Minus {};
}

気になるかもしれないので補足しておくと, ML1 では「-」は左結合です. つまり「8 - 2 - 3」は「(8 - 2) - 3」として解釈されます.
これを演習システムで提出すると, 正解かどうか, 間違っている場合は間違いの箇所を教えてくれます.

例示によって理解が深まるというのはいつも感じていることですが, 本書の内容を理解するに当たっても演習は非常に役立ちました. 無料で利用できますし, 本書を読まれる方にはおすすめです.

ぜんぶ解くのは大変すぎましたし, 飽きたら次に行くことが推奨されていたので遠慮なく飛ばしました.
実際にやると分かると思うのですが, 複雑な導出になるとものすごく大変です. 導出を生成するプログラムを作ってくださいということだと思うので一部はコードを書いてみました.

しかし, きちんとやろうとすると一筋縄では行かないと感じ, 適当なところで諦めています. 式を演算子の結合を考慮して構文木に分解するのは難しいと思ってしまいましたが, 将来の宿題にしようと思います.

ML1 の拡張

ML1 は演算と if を持っていましたが, 徐々に機能を追加していきます. 変数定義の let はどのように導出システムで扱うことができるでしょうか.

OCaml での変数定義は以下のような形式です.

1

let x = 2 in x * 5

let で値に名前をつけて, それを in 以降で利用するということです. この let 式の値は 2*5 で 10 です.
let は入れ子にもできます. この場合, let x の in 部分が let y = 2 in if x then y + 5 else y - 6 になっているということです.

1
2

let x = true in
  let y = 2 in if x then y + 5 else y - 6

let による定義は続く in の中でのみ有効です. 変数の有効範囲を表すために「変数」と「環境」を定義します.

1
2

x, y ∈ Var
E    ∈ Env := [] | E, x = v

この定義の意味するところは, 環境は空であるか, 環境に (変数)=(値) を付け加えたものであるかということです. 例えば上記で例に上げた入れ子の let だと, 最後の if を評価するときの環境は [x = true, y = 2] です.
変数の有効範囲は, 環境に含まれているときのみ変数を参照できるというルールとして記述できます.

関数も let と同様に環境を使います. OCaml の関数は以下のような fun (変数) -> (式) という形式です.

1

fun x -> x + 8

引数を 2 つ持つ関数は「関数を返す関数」を使って定義できます.

1

fun x -> fun y -> x + y

fun y -> x + y は引数 y を取って x と y の和を返す関数です. fun x -> fun y -> x + y は引数 x を取って, 「引数 y を取って x と y の和を返す関数」を返す関数です.
このように, 複数の引数を持つ関数を「関数を返す関数」を使って定義することを「カリー化」と言います.

さて, OCaml の変数の有効範囲の決め方はスタティックスコープです. 有効範囲の決め方は, 以下のような状況で重要になります.

1
2
3
4

let a = 3 in
let f = fun x -> x * a in
let a = 5 in
(f 1) + a

問題は, 最後の関数適用 f 1 で 1 に描けられる数は 3 なのか 5 なのかということです. スタティックスコープではプログラムの実行順序によらず, 関数を定義したときの有効範囲に基づいて環境が決まります. つまり, f が評価されたときにその時点での環境が保存されるということです. 上記の式 (f 1) + a の値は 3 + 5 = 8 です.

導出システムでは関数の評価と適用を以下のように表現することができます. E |- というのは, 環境 E の下で, という意味です.

1
2
3
4
5
6

値の追加
v ∈ Value := ... | (E) [fun x -> e]

推論規則の追加
E-Fun: E |- fun x -> e evalto (E)[fun x -> e]
E-App: (E |- e1 evalto (E2)[fun x -> e]) ∧ (E |- e2 evalto v2) ∧ (E2, x=v2 |- e0 evalto v) ⇒ E |- e1 e2 evalto v

let, 関数と来て, 次は再起関数, リスト, パターンマッチという風に拡張が進んでいきますが, 長くなるので省略します.

型システム

型を導出システムで扱う

本書のメイン, 型システムです. 型システムとは, プログラムを実行する前に未然に防げるエラーを検知する仕組みのことです.
と言っても, すべてのエラーを検知することはできず, 検知にも限りがあります. 型システムによって検知できるエラーとは, x + 1 で x が int でない, true < 5 のように真偽値を大小比較していると言った種類の, 型が不適切であることによって起きるエラーです.
検知できないエラーは, プログラムが無限ループに陥って終了しない, match 式で 1 つもマッチするパターンがない, などのエラーです.

規則に従って式や値に型をつけて, エラーなくすべての型が付けられた場合は型の不整合によるエラーは起きないことが保証されます (型安全性).
型付けの推論規則は以下のようなものです.

1
2
3

T-Int: T |- i : int
T-Bool: T |- b : bool
T-If: (T |- e1 : bool) ∧ (T |- e2 : t) ∧ (T |- e3 : t) ⇒ T |- if e1 then e2 else e3 : t

i : int は「i の型が int である」という意味です. 省略していますが, 他にも加算, 乗算, let, 関数適用などの型付け規則があります.

型推論

OCaml の主要な機能に型推論があります. これはコードに型を書くことなく自動的に型付けする機能です.
型推論の方法としてまず思いつくのは e1 + e2 : int という式があったら e1 と e2 は int であるとするというようなものでしょう. そうして e1 : int として再帰的に型を伝搬させていくやり方です. しかし関数 fun x -> e : t だと, x の型はすぐにはわかりません.

そこで工夫が必要なのですが, 型推論の主要なアイデアは, 型についての方程式を立てるということです. 不明な型はひとまず変数において, 連立方程式として解くということです.
例えば fun x -> (x 5) + 1 という式を考えてみます. x の型がわからないので, a と置きます. すると,

1. x 5 で x は 5 を引数として取る関数なので, 返り値の型を b として a = int -> b となる
2. (x 5) + 1 で加算をしているので, x 5 は int でなければならない. よって b = int が分かる
3. fun x -> (x 5) + 1 の型は a -> int でなければならない

以上の過程により, 型についての連立方程式は以下のようになります.

1
2

a = int -> b
b = int

これを解くと (解く, というほどでもないくらい簡単ですが) a = int -> int, b = int が得られます. よって, 最終的な fun x -> (x 5) + 1 の型 a -> int は (int -> int) -> int であることが分かりました.

型推論のアルゴリズムは, 方程式を抽出する過程と方程式を解く過程 (今回のような適切な値の割り当てを求める問題を単一化問題 = unification problem と呼ぶ) に分けられます.
抽出の規則は以下のようになります. 抽出は型環境 T と式を受けとって, 型の割り当て E と式の型を返す関数として定義します.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

Extract(T, i) = ([], int)

Extract(T, b) = ([], bool)

Extract(T, x) = ([], T(x))  <- 型環境 T から x の型を探すという意味

Extract(T, e1 op e2) = let (E1, t1) = Extract (T, e1) in
                       let (E2, t2) = Extract (T, e2) in
                       let E3 = E1 ∪ E2 ∪ (t1 = int, t2 = int) in
                       if op = '<' then (E3, bool) else (E3, int)

Extract(T, fun x -> e) = let a = (新しい型変数) in
                         let (E, t0) = Extract (T, x = a, e) in
                         (E, a -> t0)

これも全部書くと長くなるので省略しています.

最初の 3 つの規則は単純で, int なら int, bool なら bool, 変数なら型環境にある x の型, というルールを表しています. e1 op e2 は e1, e2 をそれぞれ抽出した後, それぞれの割り当てを合成します. 式全体の型は, op が「<」なら bool でそれ以外なら int です. 関数では未知の型を a として追加するという操作が含まれています.

例を見たほうが理解が早いと思います. fun x -> x + 2 で考えます.

まず式全体は fun です. スタート時点で型環境は空です.

1
2
3
4

Extract([], fun x -> x + 2)
= let a = "a_x" in
  let (E, t0) = Extract ([x = a], x + 2) in
  (E, a -> t0)

x + 2 に対して再帰呼出しです.

1
2
3
4
5

Extarct([x = "a_x"], x + 2)
= let (E1, t1) = Extract ([x = "a_x"], x) in
  let (E2, t2) = Extract ([x = "a_x"], 2) in
  let E3 = E1 ∪ E2 ∪ [t1 = int, t2 = int] in
  if op = '<' then (E3, bool) else (E3, int)

x, 2 に対して再帰呼出しです.

1
2

Extract([x = "a_x"], x) = ([], "a_x")
Extract([x = "a_x"], 2) = ([], int)

x + 2 は終了です.

1
2
3
4
5
6
7

Extarct([x = "a_x"], x + 2)
= let (E1, t1) = ([], "a_x") in  <- 結果を代入
  let (E2, t2) = ([], int) in    <- 結果を代入
  let E3 = E1 ∪ E2 ∪ [t1 = int, t2 = int] in
  if op = '<' then (E3, bool) else (E3, int)

Extarct([x = "a_x"], x + 2) = (["a_x" = int, int = int], int) <- 最終的な結果

ようやく最初に戻ってきました.

1
2
3
4
5
6

Extract([], fun x -> x + 2)
= let a = "a_x" in
  let (E, t0) = ([x = "a_x"], int) in <- Extract ([["a_x" = int, int = int], x + 2) の結果を代入
  (E, a -> t0)

Extract([], fun x -> x + 2) = (["a_x" = int, int = int], "a_x" -> int) <- 最終的な結果

連立方程式は "a_x" = int, int = int, 式全体の型は "a_x" -> int です.

次にこれを単一化していきます. 規則は以下の通りです (一部省略しています).

1
2
3
4
5
6

Unify([]) = []

Unify(E, t = t) = Unify(E)

Unify(E, a = t) = Unify(a を t に置換した E) ∪ (a = t)
Unify(E, t = a) = Unify(a を t に置換した E) ∪ (a = t)

割り当て E は "a_x" = int, int = int で, まず int= int に着目します. 未知の変数を含んでいないので, 削除して OK です.

1

Unify("a_x" = int, int = int) = Unify("a_x" = int)

次の呼び出し Unify("a_x" = int) は上の規則の Unify(E, a = t) に当たります. 今回は他の割り当てがないのでこれで終了です.
やっていることが単純な割に道のりは長かったですが, これでようやく式の型 "a_x" -> int が int -> int であることが分かりました.

以上で説明は終わりです.

このコードで fun x -> fun y -> if x then 2 + 3 else y 1 を以下のように型推論できます (utop で動作させています. Str が必要なので, 実際に動かすときは #use "topfind" #require "str" してください).

1

- : string = "bool -> (int -> int) -> int"

途中過程は以下のようになります.

1
2
3

- : (string * string) list * string = ([("a_y", "int -> a_z"); ("a_x", "bool"); ("int", "a_z")], "a_x -> a_y -> int")

- : (string * string) list = [("a_z", "int"); ("a_y", "int -> int"); ("a_x", "bool")]

結び

以前『論理学をつくる』を読んだとき, プログラムを厳密に分析する分野があるのではないかと思うので次のステップにしたいと書きましたが, まさに本書がそれでした (我ながら, 自分の選書眼に驚きです. 内容も似ていたので読む順番もバッチリです).

本書を読んで良かったことは, 単に導出システムでのプログラミング言語の分析について学べただけでなく, プログラムについて新たな気づきがあったことです.
例えば BNF でプログラムの構文を定義すると, プログラム全体を抽象構文木として捉えられます. すると, プログラムを実行するということは, つまり抽象構文木を順番に評価していくということなんだと, ふと思いました. これまで主に手続き型の言語を触ってきたので, プログラムの実行と言うと文を上から順番に実行していくというイメージでした. プログラム=巨大な抽象構文木, プログラムの実行=抽象構文木の評価というイメージが描けて新鮮でした. 関数型言語に親しんでいる人は, もしかするとこういうイメージを持っているのでしょうか. それとも全く別の捉え方があるのかもしれません.

他にも, 変数の定義は環境に変数を追加することなんだと理解でき, スタティックスコープの意味するところが分かりました. また, これまでカリー化の意義がわからなかったのですが, 関数の引数を 1 つに固定することで導出システムをシンプルにできるメリットがあると気づきました (他にも利点はあるかもしれませんが).
実用的な知識を得るためなら本書のような内容の勉強に時間を費やすのは遠回りだと思いますが, プログラミング言語に対する見方を新しくできたことは確かな収穫であったと感じます.

本書の演習システムを進めるに当たって OCaml を書いていましたが, ずっとやりたいことをうまくできない, もっと良い方法がありそうなのにわからないというフラストレーションを抱えていました. 今後は OCaml について知識を深めて, 納得行くようなコードを掛けるようにしたいと思います.