Hindley-Milner型推論をCで実装した話

SecHack365 2019 Advent Calendar 14日目の記事です(大遅刻)．

what is this
きっかけ
実装したもの
型と型推論について
実装
感想
参照したリンクとか

what is this

　型理論とか全く知らない人がHindley-Milner型推論器(+ REPL)をCで実装したお話．

記事に誤謬などを発見したらコメントとかDM，リプライください(@cmpl_error)．

きっかけ

　今年の4月からHindley-Milner型推論という型推論アルゴリズムがあるのはなんとなく知っていて，実装してみたいなーという気持ちがなんとなくありました．

そして，今年の10,11月くらいにすごいH本を買って，Hindley-Milner型推論が自分の想像していた以上に強力であることを知りました．無知な自分には，一切型注釈の無い以下のコード

let f x y = x + y

が文脈からfがint -> int -> intと正しく型付けされると知ったときは結構衝撃でした．

で，型推論について調べていたところBasic Polymorphic Typecheckingという多相型についての論文が読みやすくて良さげということを知りました．さらに，その論文を元にした型推論アルゴリズムのC実装を見つけたので，もうこれは実装するしかないかということになりました．

実装したもの

　今回の型推論の対象となる言語(以下mini-ML)のlexer,parserと，出来た構文木を解析して式の型を推論する推論器を作成しました． f:id:admarimoin:20191227180411g:plain 　リポジトリ： github.com

申し訳程度のコメントもついてます．

型と型推論について

型？

　型が何をしてくれているのか，mini-MLを例に出して説明します．

まずは，mini-MLの式の定義を以下に示します． $e$ は式， $x$ は変数， $n$ は整数を表しています．

\begin{align}
e ::=\ & x \tag{変数} \\
| \ \ \ & n \tag{整数} \\
| \ \ \ & {\rm fun} \ x → e \tag{ラムダ抽象} \\
| \ \ \ & (e\ e) \tag{関数適用} \\
| \ \ \ & {\rm let} \ x = e\ {\rm in}\ e \tag{let式} \\
| \ \ \ & {\rm let\ rec} \ x = e\ {\rm in}\ e \tag{letrec式} \\
\end{align}

慣れない言葉がいっぱい出てきた人のために：

ラムダ抽象
　無名関数．fun x -> eでは，xが仮引数，eが返り値．例えば，fun a -> aは受け取った値をそのまま返す関数(受け取った値をaに束縛し，aを返しているので)．
関数適用
　関数呼び出し．(e e)はe(e)と読み替えてもらって問題ないです．
let式
　変数束縛．let x = e in eは，変数xに式eを束縛し，その変数xのスコープはin以降の式にのみ持つ．in以降の式はlet式の返り値になる．
let rec式
　再帰する定義が書けるlet式．例えば，フィボナッチ数列のn番目を求めるプログラムを書くにはこれを使う．
(関数<, +, -, ifは事前に定義されているものとする)

let rec fibo = fun n -> (((if ((< n) 2)) n) ((+ (fibo ((- n) 2))) (fibo ((- n) 1)))) in (fibo 30)

慣れない言葉がいっぱい出てきた人のために　おわり

　さて，説明の為に以下の事柄は事前に定義されているものとします．

true, false
真偽値を表す変数．
+
2つの値(整数)を受け取り，それらを加算した値(整数)を返す関数．((+ 200) 300)は200 + 300と同じ意味．
pair
2つの値を受け取り，それらをタプルにして返す関数．((pair 20) false)はタプル(20, false)になる．

　式の定義を元に，式の例を書き下してみました．

100
true
fun x -> ((+ x) 1)
(fun x -> ((+ x) 1) 348)
((pair 20) false)
let f = fun a -> a in (f 2141)
(1500 false)

　ここで出てくるのが，「構文的には合ってるけど正しく実行出来ない」式です．ここでは(1500 false)がそれに当たります(1500は整数であり関数ではないので，関数適用はできません)．

この正しく実行できない式を，実行時ではなく，解析時に検出するために導入されたのが型です．

静的型付け言語を触ったことのある人，コンパイル時にエラーが出たことがありませんか？それはコンパイラがコンパイル時に型を解析してくれているお陰です．

正しく型付けされたプログラムは不正な動きをしないことが保証されます(型安全)．

　さて，mini-MLの型の定義を以下に示します． $t$ は型， $α$ は型変数(後述)を表しています．

\begin{align}
t ::=\ & \alpha \tag{型変数} \\
| \ \ \ & {\rm int} \tag{整数型} \\
| \ \ \ & {\rm bool} \tag{真偽値型} \\
| \ \ \ & t → t \tag{関数型} \\
| \ \ \ & t \times t \tag{タプル型} \\
\end{align}

関数型 $t → t$ は $t$ 型の値を受け取って $t$ 型の値を返す関数の型を表しています．例えば， ${\rm int} → {\rm bool}$ はint型の値を受け取ってbool型の値を返す関数の型となります．

　試しに，先程上げた式の例の各々に型をつけてみます．式 $e$ が型 $t$ を持つとき， $e : t$ と書きます．

型の付けようがない場合は $\rm error$ としました．

100 : int
true : bool
fun x -> ((+ x) 1) : int -> int
(fun x -> ((+ x) 1) 348) : int
((pair 20) false) : int * bool
let f = fun a -> a in (f 2141) : int
(1500 false) : error

式の型は，型付け規則によって導出することができます．

型付け規則はこわくない

\begin{align}
{\frac{\Gamma \vdash e _ 1:t _ 1→t _ 2\ \ \ \Gamma \vdash e _ 2 : t _ 1}{\Gamma \vdash (e _ 1\ e _ 2) : t _ 2}}
\end{align}
これは型付け規則の一例です．今からこれを読んでいきます．

型環境

　例えば，式

の型を導出しろと言われたとします．

勿論xだけじゃ型を導出することはできません．しかし，

let x = 10 in
x

のように変数xがどのように導入されたかが書かれていれば，xの型はintと導出することができます．変数がどのように導入されたかは，型環境に登録します．型環境は，変数とその型の組の集合です．

ここでは，型環境を $\Gamma$ で表します．

型環境 $\Gamma$ において，式 $e$ の型が $t$ であるとき，

\begin{align}
\Gamma\vdash e:t \end{align}
と書き，「型環境 $\Gamma$ の下で式 $e$ は型 $t$ を持つ」と読みます．

型環境 $\Gamma$ に変数 $x$ と型 $t$ の組を追加するとき， $\Gamma, x: t$ と書きます．

型環境 $\Gamma$ において変数 $x$ は型 $t$ を持つと仮定するとき， $x:t \in \Gamma$ と書きます．

型付け規則を読む

　上から下に読みます．

型付け規則の下に，その読み方の例を乗っけています．

整数

\begin{align}
n: {\rm int} \tag{T-Int}
\end{align}
　整数 $n$ は型 ${\rm int}$ を持つ．

変数

　型環境から，その変数に対応する型を導出します．

\begin{align}
{\frac{x:t \in \Gamma}{\Gamma \vdash x:t}} \tag{T-Var}
\end{align}
型環境 $\Gamma$ において変数 $x$ は型 $t$ を持つと仮定するとき，
型環境 $\Gamma$ において変数 $x$ は型 $t$ を持つ．

~~小泉進次郎構文みたいだな~~

ラムダ抽象

　 ${\rm fun}\ x → e$ は， $e$ で引数 $x$ を使うため，型環境に $x$ を新たに追加してやる必要があります．

\begin{align}
{\frac{\Gamma, x:t _ 1 \vdash e:t _ 2}{\Gamma \vdash {\rm fun}\ x → e:t _ 1 → t _ 2}} \tag{T-Abs}
\end{align}
$x: t _ 1$ を追加した型環境 $\Gamma$ において，式 $e$ が型 $t _ 2$ を持つとき，
その型環境 $\Gamma$ において ${\rm fun}\ x → e$ は型 $t _ 1 → t _ 2$ を持つ．

関数適用

　 $(e _ 1\ e _ 2)$ の $e _ 1$ は必ず関数型( $t _ 1→t _ 2$ )でなければならず， $e _ 2$ の型は $e _ 1$ の引数の型( $t _ 1$ )と一致してなければなりません．

\begin{align}
{\frac{\Gamma \vdash e _ 1:t _ 1→t _ 2\ \ \ \Gamma \vdash e _ 2 : t _ 1}{\Gamma \vdash (e _ 1\ e _ 2) : t _ 2}} \tag{T-App}
\end{align}
型環境 $\Gamma$ において，式 $e _ 1$ が型 $t _ 1→ t _ 2$ を持ち，式 $e _ 2$ が型 $t _ 1$ を持つとき，
型環境 $\Gamma$ において $(e _ 1 \ e _ 2)$ は型 $t _ 2$ を持つ．

let式

　 ${\rm let}\ x = e _ 1\ {\rm in}\ e _ 2$ は，変数 $x$ を $e _ 2$ の中で使いたいので，型環境に $x$ とその型(= $e _ 1$ の型)の組を追加してあげる必要があります．

\begin{align}
{\frac{\Gamma \vdash e _ 1:t _ 1\ \ \ \Gamma,x:t _ 1 \vdash e _ 2 : t _ 2}{\Gamma \vdash {\rm let}\ x = e _ 1\ {\rm in}\ e _ 2: t _ 2}} \tag{T-Let}
\end{align}
型環境 $\Gamma$ において，式 $e _ 1$ が型 $t _ 1$ を持ち， $x: t _ 1$ を追加した型環境 $\Gamma$ において式 $e _ 2$ が型 $t _ 2$ を持つとき，
その型環境 $\Gamma$ において ${\rm let}\ x = e _ 1\ {\rm in}\ e _ 2$ は型 $t _ 2$ を持つ．

let rec式

　 ${\rm let\ rec}\ x = e _ 1\ {\rm in}\ e _ 2: t _ 2$ は，let式とは違い変数 $x$ を $e _ 1$ ， $e _ 2$ の中で使える必要があります． \begin{align}
{\frac{\Gamma, x: t _ 1 \vdash e _ 1:t _ 1\ \ \ \Gamma \vdash e _ 2 : t _ 2}{\Gamma \vdash {\rm let\ rec}\ x = e _ 1\ {\rm in}\ e _ 2: t _ 2}} \tag{T-Letrec}
\end{align}
$x: t _ 1$ を追加した型環境 $\Gamma$ において，式 $e _ 1$ が型 $t _ 1$ を持ち，その型環境 $\Gamma$ において式 $e _ 2$ が型 $t _ 2$ を持つとき，
その型環境 $\Gamma$ において ${\rm let}\ x = e _ 1\ {\rm in}\ e _ 2$ は型 $t _ 2$ を持つ．

(本当に合ってるのか自信なくなってきた)

型推論？

　型推論を使えば，型注釈が無いプログラムから，プログラムや変数の型を知ることができます．OCamlを例に出します．

# let add x y = x + y;;
val add : int -> int -> int = <fun>

型注釈の無いプログラム(1行目)から，変数addの型を知ることが出来ています(2行目)．

Hindley-Milner Type System

　多相型付きラムダ計算のための型システムで，これを使えば型注釈が一切無くても式から適切な型が導出できることが知られています．多相についてはまた後で．HMはパラメトリック多相とかなんとか．

Hindley-Milner型推論

　型推論はどうやって行われているか説明していきます．

ズバリ，型の連立方程式を解いています！(ドン！！！)

その方程式が解けなかったら，それは型検査をパスしてはダメなプログラムなので弾けばいいわけです．

型の連立方程式

　型の連立方程式とは何なのか，簡単な例を出して説明していきます．

fun x -> ((+ x) 10)

受け取った値に10を足して返す関数です．(分かりやすい形にするとfun x -> x + 10)

まずは，連立方程式について考えていきます．連立方程式を解くとき，後で求める現在未知の値は変数にしておきます．
型の連立方程式でも同じです．後で求める未知の型は型変数( $\alpha, \beta, \ldots$ )にしておきます．
実際にやってみます．型付け規則や型環境から今わかっている事をすべて書きだし，未知の型には型変数をつけます．
+の型は ${\rm int} → {\rm int} → {\rm int}$ で，xの型は未知なので型変数 $\alpha$ で置きます．

+の型は ${\rm int} → {\rm int} → {\rm int}$
xの型は $α$

(+ x)の型は不明なので，型変数 $\beta$ と置きます．すると，型付け規則T-Appより+の型は $\alpha→\beta$ と分かります．

+の型は ${\rm int} → {\rm int} → {\rm int}$
xの型は $α$
(+ x)の型は $\beta$
+の型は $\alpha→\beta$

すると，+によって $\alpha→\beta = {\rm int} → {\rm int} → {\rm int}$ と分かりました．これを解いて型変数の正体を暴きます！(単一化)

+の型は ${\rm int} → {\rm int} → {\rm int}$
xの型は ${\rm int}$
(+ x)の型は ${\rm int}→{\rm int}$

解いたら次行きます．T-Intより10の型は ${\rm int}$ です．
((+ x) 10)の型は不明なので， $\gamma$ と置きます．すると，T-Appより(+ x)の型は ${\rm int}→\gamma$ と分かります．

+の型は ${\rm int} → {\rm int} → {\rm int}$
xの型は ${\rm int}$
(+ x)の型は ${\rm int}→{\rm int}$
10の型は ${\rm int}$
((+ x) 10)の型は $\gamma$
(+ x)の型は ${\rm int}→\gamma$

すると，(+ x)より ${\rm int}→{\rm int} = {\rm int}→\gamma$ となることが分かったので，解きます．

+の型は ${\rm int} → {\rm int} → {\rm int}$
xの型は ${\rm int}$
(+ x)の型は ${\rm int}→{\rm int}$
10の型は ${\rm int}$
((+ x) 10)の型は ${\rm int}$

そして，最後はfun x -> ((+ x) 10)です．以上の情報よりxの型は ${\rm int}$ ，((+ x) 10)の型は ${\rm int}$ と分かっているので，T-Absを適用すると

+の型は ${\rm int} → {\rm int} → {\rm int}$
xの型は ${\rm int}$
(+ x)の型は ${\rm int}→{\rm int}$
10の型は ${\rm int}$
((+ x) 10)の型は ${\rm int}$
fun x -> ((+ x) 10)の型は ${\rm int}→{\rm int}$

となります．このようにして型推論器は型注釈が無いプログラムから型を推論します．

多相性

　次は，以下の式について考えてみます．

fun x -> x

受け取った値をそのまま返す関数です．これの型を推論していきます．まず，xの型は未知なので，型変数 $α$ を置きます．

xの型は $\alpha$

次はfun x -> xです．xの型は $\alpha$ なので，T-Absを適用すると型は $\alpha→\alpha$ となります．

xの型は $\alpha$
fun x -> xの型は $\alpha→\alpha$

終わりです．

型変数が残ったまま推論が終了してしまいましたが，失敗ではありません．
最終的な推論結果に型変数が残った場合，その型変数にはどんな型を入れてもOKということになります(多相性)．

$\alpha → \alpha$ は， ${\rm int} → {\rm int}$ でも ${\rm bool}→{\rm bool}$ でも ${\rm int}→{\rm int}→{\rm int}→{\rm int}$ でもOKです．

「未知なのでとりあえず変数として置いておく」型変数と「どんな型を入れてもOK」な型変数との区別を付けるために，後者の型変数には $\forall \alpha .$ を付けて $\forall \alpha . \alpha$ と表現したりします(型スキーム)．

実装

　Basic Polymorphic Typecheckingという論文で実装されている型推論のソースコードを元に実装しました．
さらに，その実装を元にした実装も参考にしました．

github.com github.com http://dysphoria.net/code/hindley-milner/HindleyMilner.scala

　~~詳しくはソースコード読んでください．~~ リポジトリの各ファイルとその説明を申し訳程度に書いておきます．

src/env.c, include/env.h
型環境に関することが書かれています
src/nongeneric.c, include/nongeneric.h
ジェネリックでない型変数(つまり，「未知なのでとりあえず変数として置いておく」型変数)に関することが書かれています
src/expr.c, include/expr.c
mini-MLの式に関することが書かれています
src/type.c, include/type.h
mini-MLの型に関することが書かれています
src/infer.c, include/infer.h
型推論のコア部分．実際にここで型推論が行われています
src/lexer.c, src/token.c, src/parser.c, include/lexer.h, include/token.h, include/parser.h
入力を解析して構文木にしてます．型推論とは直接には関係していません
src/util.c, include/util.h
C言語には可変長配列とかMapがデフォルトで無いので自分で実装したもの

詳細は力尽きました．気が向いたら追記します．

感想

　C言語の話をしてねえ！ただ単純に型と型推論について自分なりの解釈を語った記事になってしまっtar...

free(malloc(sizeof(MRM)));

虚無・アクセラレーション