型システムを学ぼう！

書いた日： 2017 年 12 月 15 日^*1、 書いた人：@unnohideyuki、

これは Haskell Advent Calendar 2017 (その１) 15日目の記事です。 この記事では、以下のような構成で Hindley/Milner の型推論について述べたいと思います。

1. 型システム： 構文、意味論、および、型付け規則
2. Hindly/Milner の型推論
3. Haskell による実装

最初の節では、とても小さな言語を題材にして型システムを形式的に定義してみます。 ここでは、型とはなにか、また、その役割や能力について確認します。 この節のもうひとつの目的は、型システムを形式的に記述するやりかたに慣れることです。 そして次に、Hindley/Milner の型推論について述べ、最後に Haskell による実装を示します。

ここではちょっと手間をかけて、自然数と真理値、および、 条件式のみからなるような小さな言語の型システムを形式的に定義し、その性質について調べてみます。

ここで扱う言語の構文を以下に示します。

これは、次のような意味になります。

• 0, true, false は、いずれも項 (term) である。
• t1 が項であるなら、succ t1, pred t1, iszero t1 はいずれも項である。
• t1, t2, t3 がいずれも項であるなら、if t1 then t2 else t3 も項である。
• この言語は、以上の３つの条件のうち、いずれかを満たす項のみからなる。

以下に、この言語におけるいくつかのプログラム例をみてみましょう。

なお、この構文では、succ true や if 0 then 0 else 0 のような項も許容されることに注意してください。

言語の構文を定義したので、次は、項がどう評価されるかを定義します。

最初に着目したいのは、項の中でも、そのものが値を示しているような特別な項です。 値には、真理値 (bv; boolean value) をあらわす、true と false があります。

さらに、数値 (nv; numeric vaule) を表す項として以下のものがあります。 0、もしくは、数値に後者関数 succ を適用したものが数値です。

両者をまとめるて、この言語における値 (v; vaule) は以下のように定義できます。

次に、値以外の項の評価規則を定義していきます。 評価関係は \(\texttt{t} \rightarrow \texttt{t'}\) のように書かれ、「項 \(\texttt t\) が項 \(\texttt {t'}\) に評価される」とよみます。 また、前提条件のない評価は \(\texttt{t} \rightarrow \texttt{t'}\) そのものの形をとり、 前提条件がある場合には、以下のように前提となる評価関係と、適用される評価関係を重ねた推論規則の形をとります。

\[ \frac{\texttt{t1} \rightarrow \texttt{t1'}}{\texttt{t2} \rightarrow \texttt{t2'}} \]

では、if 文に関わる規則から。

\[ \begin{aligned} \texttt{if true then t2 else t3} \rightarrow \texttt{t2} &\quad \textrm{(E-IfTrue)}\\ \quad &\quad\\ \texttt{if false then t2 else t3} \rightarrow \texttt{t3} &\quad \textrm{(E-IfFalse)}\\ \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t1'}}{\texttt{if t1 then t2 else t3} \rightarrow \texttt{if t1' then t2 else t3}} &\quad \textrm{(E-If)} \quad &\quad\\ \end{aligned} \]

ひとつめの規則は、条件式において、検査対象の項が true そのものであった場合には t3 を評価せずに捨てて、条件式全体を t2 に起きかえることを意味しています。 ふたつめは、検査対象が false だった場合で、この場合は条件式の評価結果が t3 となります。

３つめは、検査対象の項が値でなかったケースに対応するもので、 他の規則によって t1 が t1' に評価されるときには、 条件式全体が if t1' then t2 else t3 へ評価されることを示しています。

残りの規則は以下の通り、算術式に関する評価規則です：

\[ \begin{aligned} \frac{\texttt{t1} \rightarrow \texttt{t'}}{\texttt{succ t1} \rightarrow \texttt{succ t1'}} &\quad \textrm{(E-Succ)}\\ \quad &\quad\\ \texttt{pred 0} \rightarrow \texttt{0} &\quad \textrm{(E-PredZero)}\\ \quad &\quad\\ \texttt{pred (succ nv1)} \rightarrow \texttt{nv1} &\quad \textrm{(E-PredSucc)}\\ \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t'}}{\texttt{pred t1} \rightarrow \texttt{pred t1'}} &\quad \textrm{(E-Pred)}\\ \quad &\quad\\ \texttt{iszero 0} \rightarrow \texttt{true} &\quad \textrm{(E-IszeroZero)}\\ \quad &\quad\\ \texttt{iszero (succ nv1)} \rightarrow \texttt{false} &\quad \textrm{(E-IszeroSucc)}\\ \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t'}}{\texttt{iszero t1} \rightarrow \texttt{iszero t1'}} &\quad \textrm{(E-IsZero)}\\ \quad &\quad\\ \end{aligned} \]

前節で示したプログラム例について、評価の様子を確認してみましょう。まずは、if false then 0 else (succ 0) から：

E-IfFalse 規則で if false then 0 else (succ 0) は succ 0 に評価されました。 succ 0 は値なので、そこで評価はおしまいです。

もう一つの例、iszero (pred (succ 0)) については以下のようになります。最初に E-PredSucc および E-IsZero 規則によって iszero (pred (succ 0)) → iszero 0 のように評価され、さらに、E-IszeroZero 規則によって true へ評価されます。

では、succ true や if 0 then 0 else 0 についてはどうでしょうか。 これまでの定義にてらしてみると、この２つはいずれも値ではなく、かといって、これらに当てはまる評価規則も存在しません。 このように、値でなく、かつ、当てはまる評価規則がないような状態を 行き詰まり状態 といいます。

項を評価すると、その結果が値として得られるか、または、ある段階でどの評価規則も適用できないような 行き詰まり状態 になるかのどちらかとなります。行き詰まり状態は、実行時エラーに対応するものであり、 できれば項を実際に評価せずに、その項の評価が行き詰まり状態にならないことを保証したいところです。

行き詰まり状態になるケースを観察すると、pred , succ , iszero などの引数に 数値以外を与えようとした場合や、if 文の検査対象に真理値以外を置いてしまったケースがあることがわかります。 そこで、数値に評価される項と真理値に評価される項とを、ふたつの型 Nat , Bool に分類することにします。

そういうわけで、ここでの型は Bool (真理値型）または、Nat (自然数型）です：

「項 t が型 T をもつ」という型付け関係を t:T と書くこととし、この言語における型付け規則を、 項に型を割り当てる推論規則の集合として定義しましょう。

\[ \begin{aligned} \texttt{true} : \texttt{Bool} &\quad \textrm{(T-True)}\\ \quad &\quad\\ \texttt{false} : \texttt{Bool} &\quad \textrm{(T-False)}\\ \quad &\quad\\ \frac{\texttt{t1}:\texttt{Bool} \quad \texttt{t2}:\texttt{T} \quad \texttt{t3}:\texttt{T}} {\texttt{if t1 then t2 else t3} : \texttt{T}} &\quad \textrm{(T-If)}\\ \quad &\quad\\ \texttt{0} : \texttt{Nat} &\quad \textrm{(T-Zero)}\\ \quad &\quad\\ \frac{\texttt{t1}:\texttt{Nat}} {\texttt{succ t1} : \texttt{Nat}} &\quad \textrm{(T-Succ)}\\ \quad &\quad\\ \frac{\texttt{t1}:\texttt{Nat}} {\texttt{pred t1} : \texttt{Nat}} &\quad \textrm{(T-Pred)}\\ \quad &\quad\\ \frac{\texttt{t1}:\texttt{Nat}} {\texttt{iszero t1} : \texttt{Bool}} &\quad \textrm{(T-IsZero)}\\ \quad &\quad\\ \end{aligned} \]

規則 T-True, T-False は、真理値定数 true と false に Bool 型を割り当てています。 規則 T-If は、部分項 t1 の型が Bool であり、かつ、t2, t3 に同じ型 T が割り当てられる場合に限って、 if 文全体に型 T が割り当てられることを主張しています。

これらの型付け規則によって、たとえば項 if true then false else false は Bool 型を持ち、 pred(succ(pred(succ 0))) は Nat 型を持つことが、項の値を評価することなくわかりました。 このようなに「項の値を実際に計算することなく」行う分析のことを、静的な分析といいます。

なお、実際に値を計算せずに行う型分析は、保守的になります。 つまり、if (iszero 0) then 0 else false 　や if true then 0 else false といった項は、実際には行き詰まり状態にはならないにも関わらず、 どんな型も持てません。

型システムの目的は、正しく型付けされた項はおかしくならない、つまり、 行き詰まり状態にならないことを保証することです。この性質のことを安全性といいます。 この性質は、進行と保存という２つのステップに分けて証明できることができます^*2。

• 進行とは、正しく型付けされた項は行き詰まり状態ではない（値であるか、評価規則によって評価を進められる）ということ
• 保存とは、正しく片づけされた項が評価できるならば、評価後の項も正しく型付けされるということ

これらの性質をあわせると、正しく型付けされた項は評価において行き詰まり状態になりえないことがいえます。

前の章では、算術と条件式からなる小さな言語に対する型検査を通じて、 型システムの概要をみてきました。 つぎに、本章では、もう少し大きな言語に対する型推論について述べます。

本章で扱うプログラミング言語の構文を以下に示します。

この言語の項 t を次のように定めます。 ただし x は変数を表します。

前章で扱ったのと同様の算術と条件式に加えて、 リスト、let 束縛、ラムダ抽象、および、関数適用があります。

この言語における値には、以下に示すものがあります：

次に、評価規則です。条件式と算術に関するものは、前章と共通です。

\[ \begin{aligned} \texttt{if true then t2 else t3} \rightarrow \texttt{t2} &\quad \textrm{(E-IfTrue)}\\ \quad &\quad\\ \texttt{if false then t2 else t3} \rightarrow \texttt{t3} &\quad \textrm{(E-IfFalse)}\\ \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t1'}}{\texttt{if t1 then t2 else t3} \rightarrow \texttt{if t1' then t2 else t3}} &\quad \textrm{(E-If)} \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t'}}{\texttt{succ t1} \rightarrow \texttt{succ t1'}} &\quad \textrm{(E-Succ)}\\ \quad &\quad\\ \end{aligned} \]

次に、新しい評価規則です。まずは、リストに関するものです。

\[ \begin{aligned} \frac{\texttt{t1} \rightarrow \texttt{t1'}} {\texttt{t1 : t2} \rightarrow \texttt{t1' : t2}} &\quad \textrm{(E-Cons1)}\\ \quad &\quad\\ \frac{\texttt{t2} \rightarrow \texttt{t2'}} {\texttt{v : t2} \rightarrow \texttt{v : t2'}} &\quad \textrm{(E-Cons2)}\\ \quad &\quad\\ \texttt{null []} \rightarrow \texttt{true} &\quad \textrm{(E-IsnilNil)} \quad &\quad\\ \texttt{null (v : v)} \rightarrow \texttt{false} &\quad \textrm{(E-IsnilCons)} \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t1'}} {\texttt{null t1} \rightarrow \texttt{null t1'}} &\quad \textrm{(E-Isnil)}\\ \quad &\quad\\ \texttt{head (v1 : v2)} \rightarrow \texttt{v1} &\quad \textrm{(E-HeadCons)} \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t1'}} {\texttt{head t1} \rightarrow \texttt{head t1'}} &\quad \textrm{(E-Head)}\\ \quad &\quad\\ \texttt{tail (v1 : v2)} \rightarrow \texttt{v2} &\quad \textrm{(E-TailCons)} \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t1'}} {\texttt{tail t1} \rightarrow \texttt{tail t1'}} &\quad \textrm{(E-Tail)}\\ \quad &\quad\\ \end{aligned} \]

残りの評価規則を示す前に、代入を表す記法を導入します。 変数 x へ s を代入することを \([\texttt{x} \mapsto \texttt{s}]\) と書くこととします。 これを用いると、\([\texttt{x} \mapsto \texttt{s}]\texttt{t}\) は、 項 t における変数 x の出現を s に置き換えたものを示します。

たとえば、\([\texttt{x} \mapsto \texttt{0}]\texttt{(succ x)}\) は、 \(\texttt{succ 0}\) となります。

なお、代入については、束縛変数の扱いについて考慮が必要なのですが、 煩雑なのでここでは省略します。

では、残りの、let束縛と関数に関わる評価規則を示しましょう。

\[ \begin{aligned} \texttt{let x=v1 in t2} \rightarrow [\texttt{x} \mapsto \texttt{v1}]\texttt{t2} &\quad \textrm{(E-LetV)} \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t1'}} {\texttt{let x=t1 in t2} \rightarrow \texttt{let x=t1' in t2}} &\quad \textrm{(E-Tail)}\\ \quad &\quad\\ \frac{\texttt{t1} \rightarrow \texttt{t1'}} {\texttt{t1 t2} \rightarrow \texttt{t1' t2}} &\quad \textrm{(E-App1)}\\ \quad &\quad\\ \frac{\texttt{t2} \rightarrow \texttt{t2'}} {\texttt{v1 t2} \rightarrow \texttt{v1 t2'}} &\quad \textrm{(E-App2)}\\ \quad &\quad\\ \texttt{(}\lambda \texttt{x -> t1) v2} \rightarrow [\texttt{x} \mapsto \texttt{v2}]\texttt{t1} &\quad \textrm{(E-AppAbs)}\\ \end{aligned} \]

この言語においても、項を評価すると、結果的に値が得られるか、 または、行き詰まり状態になるかのどちらかとなります。

たとえば、tail false は値ではなく、かつ、 当てはまる評価規則がないので行き詰まり状態です。

まず、この言語では、変数が登場するため、 型付け関係を t:T の二項関係から、 \(\Gamma \vdash \texttt{t:T}\) の三項関係に変更されます。 ここで、\(\Gamma\) は t に現れる自由変数の型に関する仮定です。

前章での型付け規則は、型を検査して、項の型を決めるような規則の集まりでした。 例えば (T-If）は、t1 の型が Bool で、t2, t3 が同じ型 T であることを要請しつつ、 条件式全体の型を T と出力する規則だったといえます。

一方で、型推論システムにおいては、型に関する規則は、次のような形をとります。

\[ \begin{aligned} \frac{\Gamma \vdash \texttt{t1}:\texttt{T1}\ |\ C_1 \quad \Gamma \vdash \texttt{t2}:\texttt{T2}\ |\ C_2 \quad \Gamma \vdash \texttt{t3}:\texttt{T3}\ |\ C_3} {\Gamma \vdash \texttt{if t1 then t2 else t3} : \texttt{T2}\ |\ C_1 \cup C_2 \cup C_3 \cup \{T1 = Bool, T2 = T3\}} &\quad \textrm{(CT-If)}\\ \quad &\quad\\ \end{aligned} \]

新しく登場した、縦棒の後ろの \(C\) は、制約の集合です。 この制約型付け規則 CT-IF は、前提条件としては、t1, t2, t3 の型を T1, T2, T3 としており、つまり、これらが特定の型であることを要請していません。 その代わり、規則を適用した結果として、 T1 = Bool, T2 = T3 という２つの新たな制約を、制約集合に追加します。

（未稿。この言語の制約型付け規則をここに示す。）

制約集合の解を計算するには、Hindley と Milner のアイディアを用います。 これは、単一化を用いて解の集合が空でないことを検査し、 空でないなら、「最良の」解を見つける方法です。

（二章は以下未稿。。。^*3）

簡単のために、型推論のコードは単一のモジュールとして提示します。

また、プログラムにおいては Haskell の豊富な語彙のうちでも基本的なものだけを使いました。 標準ライブラリ Prelude に含まれるもの以外では、Data.List より nub , (\\) , union の３関数、 そして、型推論モナドのために State ライブラリより State , runState , get , put の 4 関数のみを用いています。

識別子を表現するためには String を用いました。 また、整数値から識別子を生成するための方法を用意しておきます。 以下に示す enumId がこれで、後述する newTVar 関数から用いられます。

2.1 節で示した抽象構文を表現するための Term は以下のようになります。 ここでは、簡単のために、定数を定義済みの変数として扱うことにしています。

次に、型の表現を定義します。 型には、型変数 (TVar)、型コンストラクタ (TCon)、および、 一つの型に他のもう一つの型を適用したもの (TAp) があります。

型定義には、量化された型変数をあらわす TGen n が含まれていますが、 この TGen は、後に示す Scheme の中においてのみ用いられます。

以下に、いくつか型コンストラクタの実例を示します。

より複雑な型は、TAp を用いて定数や変数から構築されます。 たとえば、Int -> [a] 型の表現は次のようになります^*4。

このような関数型の構築は度々行うため、次に示すようなヘルパー関数を用意しておきます。 これを使うと、上の例は tInt `fn` TAp tList (TVar (Tyvar "a")) のように書けます。

型代入は、型変数から型への写像をあらわす有限関数（有限な定義域をもつ部分関数）であり、 第一要素に重複がないようなペアのリストとして表現できます。

最も単純なのは、null 代入で、つぎに単純な代入は、ひとつの型変数 u を型 t に移す u +-> t です。

型は型変数に適用します。ですが、それだけでなく、型を要素に含む（つまり型変数を含み得る） 他の値にも適用できるようにしておくのが便利です。 これは、つまり、型代入の適用関数 apply を異なる対象に使えるようにしておくと便利だということですね。

いずれの対象に用いる場合でも型代入を適用する目的は同じで、 型代入の定義域にある型変数の出現を対応する型に置き換えることです。 さらに、引数中に現れる型変数の集合を返す関数 tv も用意します。 これは、出現する順（左から右）に重複のないリストとして返されます。

まず、型を対象にした定義。

リストに適用できるようにしておくのは簡単で、かつ便利です。

apply 関数は、より複雑な型代入をつくるときにも使われます。 例えば、apply (a1 @@ s2) が apply s1 . apply s2 と等しくなるような複合関数はつぎのように書けます。

多相型をあらわすために、型スキームを定義します。Forall m t において、t に出現する TGen n は量化された（全称型の）型変数です。 m は t に含まれる TGen の個数を示します。この情報は型 t を分析すれば得られるため冗長なのですが、 後に、型スキームを実体化する際に便利なため、型スキームの定義に含めました。

たとえば、型スキーム \(\forall a \forall b . a \rightarrow b\) は、次のように書けます。

TGen がゆるされるのは、型スキームの中だけです。 また、量化された型変数は型スキームにおいて束縛されているので、型代入の影響を受けません。 これらをどうにか強制できないかということで、このような定義になっています。

変数の型に関する仮定は Assump データ型で表現されます。 仮定の各要素は、変数名と型スキームのペアです。

これも、Types クラスのインスタンスにして、型代入を適用できるようにしておきます。

仮定に関しても、いくつかヘルパー関数を用意します。 引数の型に含まれる型変数をすべて量化して型スキームをつくる gen 関数と、 仮定の集合から、特定の変数の型を探すための find 関数です。

単一化の目的は、２つの型が一致するような型代入を見つけることです。 単一化においては、なるべく小さい型代入を見つけることが重要で、 そうすることで、より一般的な型を得ることができます。

２つの型 t1, t2 に対し、apply s t1 と apply s t2 が等しくなるような型代入 s を t1 と t2 の単一化子 (unifier) といいます。

さらに、最汎単一化子 (most general unifier, mgu) とは、２つの型の単一化子 u で あって、かつ、次の性質をもつものです^*5：

• その２つの型の任意の単一化子 s に対して、s が s'@@u と等しくなるような s' が存在する。

今回対象とする言語の mgu は以下のように計算されます：

モナドは、ある種の「配管」を隠すことで、 プログラム設計のより重要な面に注意を向ける用途で広く用いられています。 今回の型推論でも、その目的で状態モナドを用います。

型推論モナドは、現在の型代入と「フレッシュな」変数を生成するための整数値の２つを状態として持ちます。

状態モナドから、現在の代入を返すのが getSubst 関数です。

引数として与えた２つの型の最汎単一化子で、現在の型代入を拡張するのが unify 関数です。

もうひとつの状態変数を用いて、あたらしい型変数を生成する関数が newTVar です。

newTVar が用いられる場面のひとつが、型スキームを新しい型変数とともに実体化するときです。

型推論の主な仕事を tiTerm 関数に実装していきます。 この関数は、仮定 as , 項 e , 型のプロトタイプ t を引数にとり、 現在の型代入^*6を拡張することで \(\sigma \Gamma \vdash e : \sigma t \) を満たすような型代入 \(\sigma\) を計算します。そのような型代入が存在しない場合には、モナド標準の fail 関数で計算が失敗します。

次に示す typeOf 関数は、tiTerm を用いて、与えられた仮定 as のもとで項 e の 型を計算します。

なお、型推論を行うにあたっては、組み込み定数に関する仮定をひとまとめに定義しておくと 便利です。

最後に、これまで定義した関数の使い方の例として、 与えられた項の型を返す関数を示します。

試しに、ghci を起動して実行してみましょう：

ちょっとわかりにくいですが、\x -> (x:[]) の型として、a4->[a4] が計算されたことがわかります。

Hindley/Milner の型推論について、その理論と Haskell による実装を解説してみよう･･･と思ったのですが、 ちょっと荷が重かったかも。

そういうわけで、型システムを学ぶには、以下の教科書を読むのがいいです。

• 型システム入門　プログラミング言語と型の理論（通称 TaPL）、Benjamin C. Pierce 著、オーム社
• 情報科学における論理、小野 寛晰著、日本評論社

後者は、型理論の教科書ではないのですが、形式体系による推論になじみのないひとで、 どんな教科書で勉強するのかわからん！という人にはオススメです。

型推論の実装については、Scala By Example の 16 章を元にしました。 ただ、それを Haskell に「移植」するのではなくて、Typing Haskell in Haskell の設計やプログラミングスタイルにあわせたつもりです。 コードの全体はGitHubに置いてあります。

なんか、長いわりに不完全な記事になってしまいましたが、ひとまずおしまいです^*7。

次は･･･、Typing Haskell in Haskell に再挑戦する前に、 How to make ad-hoc polymorphism less ad hoc の appendix を読みたい！今なら読めるかも知れない。

では。