2015/12/15

型推論のしくみ

このエントリーは、KLab Advent Calendar 2015 の15日めの記事です。

こんにちは、めっきり Jenkins の介護士となった @kakkun61 です。

趣味では Haskell を書いているのですが、そこでお世話になっている「型推論」のしくみを少し知ることができたのでみなさんに紹介したいと思います。

初めにお断わりしておくと、これから紹介する内容は『型システム入門』に全て書かれてあることです。KLab では『型システム入門』輪講をしているのですが、一緒に勉強している同僚と社外から先生として来ていただいている方にこの場を借りて感謝の意を表します。ひとりだとここまで読めなかったと思います。

『型システム入門』

型推論の解説に入る前に少し『型システム入門』について書こうと思います。

『型システム入門』は原著名 “Types and Programming Languages” 通称 “TaPL” で、プログラミング言語について形式的につまり数学の言葉を使って解説した入門書になります。集合論や論理学の知識は要りますが「入門」という書名の通り事前知識なしに読めるようになっています。その分、分量が多いのですが。

また、TaPL からいくつか内容を削ったような日本語で読める本に『プログラミング言語の基礎概念』があります。まだ、最後まで読めていませんが、型推論のしくみについて知るならこちらの方がお手軽かもしれません。

そもそも型とは

プログラマーなら多かれ少なかれ型の恩恵にあずかっていると思いますが、そもそも型とはどういうものなのでしょうか？

まず型なしの言語を考えてみましょう。ほとんどの言語には if-then-else 式もしくは文があります。そして、ほとんどの人がそれがどう評価されるかを理解していると思いますが、一度その評価のルールがどうなっているかを考えてみましょう。if 文が if (t₁) t₂; else t₃; という形になるとしましょう。すると評価のルールを明文化すると次のようになりますよね？

t₁ が true なら t₂ を評価
t₁ が false なら t₃ を評価
t₁ が値でないなら t₁ を評価して、t₁ をその結果で置き換えた if 文全体を評価

ここで暗黙のキャストはないとして if (0) then foo(); else bar(); という文があった場合、これを評価すると何が起こるでしょうか？まず、ルールで t₁ に当たるところは 0 ですが、これは true でも false でもないが値なのでルールのどのパターンにも当てはまらず評価ができません。こういう状態を「行き詰まり（stuck）」と言います。

このような行き詰まりにならないように評価前にチェックしたいわけです。この場合 if 文の条件式のところの型は bool にしかならないと定めておくと 0 の型 int と合わないことは構文木を走査すれば分かります。

型推論とは

最近では C# や C++ や Java にも簡単な型推論が導入されていて、全く触れ合ったことがないという人は少ないと思います。

例えば C# で下記のようなプログラムの1行めを型推論を使えば2行めのように書くことができます。

List<Tuple<Foo, Bar>> list = new List<Tuple<Foo, Bar>>();
var list = new List<Tuple<Foo, Bar>>();

もしこの list 変数が下記のように使われていれば、list は Tuple<Foo, Bar> 型を要素に持つリストだと分かるはずです。

list.Add(new Tuple<Foo, Bar>(foo, bar));

なので、次のように書いても型推論してほしくなるかもしれませんが実際はこのような型推論はしてくれません。

var list = new List();

C# や Java などではこのように非常に限られた条件でしか使えませんが、Haskell や OCaml などの言語ではもっとゆるい条件で型推論を利用することができます。下記プログラムは標準入力から受けとった文字列の各単語の先頭文字を大文字にするプログラムで、型を註釈していませんがちゃんと静的に型付けされてコンパイルできます。（Wandbox で実行）

import Data.Char

main = interact (unlines . map unwords . cap . map words . lines)

cap = map (map go)
      where go (h:r) = toUpper h : r
            go [] = []

ちなみに cap 関数は [[String]] → [[String]]（文字列のリストのリストを取って文字列のリストのリストを返す関数）の型で go 関数は String → String の型です。

このように、型なし言語に追加で注釈を書いてないにもかかわらず、型の恩恵にあずかることができます。

Haskell は全ての型註釈なしのプログラムの型を型推論することはできませんが（OCaml の方は詳しくないので分かりません。）、ここではもっと単純な言語で型註釈がないどんなプログラムでも型推論できるものを見ていきます。

これから議論する言語

まずどういう言語についてこれから議論していくのかを明確にしないといけません。

項を下記のように定めます。プログラム全体は1つの項になるものとします。:= の右辺に出現する t はそこに項が当てはまることを表します。JavaScript のサブセットで function が fun に、関数の中身が式だけになったような言語です。

t := …, -2, -1, 0, 1, 2, …      整数
     true, false                真偽値
     t + t                      加算
     if t then t else t         if 式
     fun(x) { t }               関数（ラムダ抽象）（本体の t の値が返り値となります）
     t(t)                       関数呼び出し（適用）

そうすると型は下記の3つになります。:= の右辺に出現する T はそこに型が当てはまることを表します。

T := Int                        整数
     Bool                       真偽値
     T → T                      関数（ラムダ抽象）（→ の左辺が引数で右辺が返り値を表す）

型推論の手掛かり

わざわざ型推論のアルゴリズムを考えなくても人間の直感で型が分かるものがあるのでまずはそれから考えていきましょう。

0 の型は当然 Int ですし、true は当然 Bool になりますよね。（というよりも、そうなるようにこれから定めます。）

では、fun(x) { true }(0) の部分項の fun(x) { true } の型はどうでしょうか？? → ? という関数型になることは分かります。次に返り値の型は関数本体が評価されて得られる値の型と同じになるはずです。つまりここでは true の型ということになりますので ? → Bool となります。引数の方はどうでしょうか。仮引数の型は実引数の型と同じになるはずです。実引数を見ると 0 になっているので引数の型は Int となります。最終的に部分項 fun(x) { true } の型は Int → Bool となることが分かりました。

ここの考察で分かったことは下記2つあります。

項を見れば自然と型が決まるものがある（0 とか true です。）
型は決まらないが制約が決まるものがある（fun(x) { true } では、返り値と関数本体・仮引数と実引数の間に制約がありました。）

この2つの視点で項の定義を見ていくと、項を見れば自然と型が決まるものは次のものがあります。

…, -1, 0, 1, … : Int
true, false : Bool

次に、型は決まらないが制約が決まるものを考えます。

1つめに加算式を見ます。加算式は次の項で表せます。

t₁ + t₂

ここで、項全体に型 T を、項 t₁ に型 T₁ を、項 t₂ に型 T₂ を与えます。すると下記制約が決まります。

T₁ = Int
T₂ = Int
T = Int

これをまとめて次のように書くこととします。

t₁ + t₂ : T
- t₁ : T₁
- t₂ : T₂
- 制約
  - T₁ = Int
  - T₂ = Int
  - T = Int

残り3種類の項についても同様に考えて、ここまで分かったこととまとめると下記のようになります。

…, -1, 0, 1, … : Int (CT-Int)
true, false : Bool (CT-Bool)
t₁ + t₂ : T (CT-Plus)
- t₁ : T₁
- t₂ : T₂
- 制約
  - T₁ = Int
  - T₂ = Int
  - T = Int
if t₁ then t₂ else t₃ : T (CT-If)
- t₁ : T₁
- t₂ : T₂
- t₃ : T₃
- 制約
  - T₁ = Bool
  - T₂ = T₃
  - T₂ = T
fun(x) { t₁ } : T (CT-Abs)
- x : X
- t₁ : T₁
- 制約
  - T = X → T₁
t₁(t₂) : T (CT-App)
- t₁ : T₁
- t₂ : T₂
- 制約
  - T₁ = T₂ → T

このルールを制約型付け規則といいます。CT-Xxx というのが各規則の名前とします。

この規則を項に適用していくと最後には制約の集合ができあがるので、その制約の集合（連立方程式）を解けば（単一化すれば）その項と部分項の型が求まることになります。

実際に制約型付け規則を適用してみる

次のプログラムを例に考えていくことにしましょう。

fun(a) {
  fun(f) {
    if a
    then 0
    else f(1)
  }
}

この項全体は関数になっているので CT-Abs を適用できます。CT-Abs の x が項 a に、t₁ が fun(f) { … } に当たります。ここでそれぞれの項の型を A, T₁ とし、全体の型を T とします。上で決めた書き方で書くと次のようになります。

fun(a) { fun(f) { if a then 0 else f(1) } } : T (CT-Abs)
- a : A
- fun(f) { if a then 0 else f(1) } : T₁
- 制約
  - T = A → T₁

ここで、部分項 fun(f) { … } が出てきたので同様に次々と規則を適用していきます。

fun(a) { fun(f) { if a then 0 else f(1) } } : T (CT-Abs)
- a : A
- fun(f) { if a then 0 else f(1) } : T₁ (CT-Abs)
  - f : F
  - if a then 0 else f(1) : T₂ (CT-If)
    - 0 : Int (CT-Int)
    - f(1) : T₃ (CT-Abs)
      - 1 : Int (CT-Int)
      - 制約
        
        F = Int → T₃
    - 制約
      - A = Bool
      - Int = T₃
      - Int = T₂
  - 制約
    - T₁ = F → T₂
- 制約
  - T = A → T₁

型を A, F, T, T₁, T₂, T₃ とおくことで、仮ではありますが一応全ての部分項に型が付きました。生成された制約を下記にまとめます。

F = Int → T₃ (1)
A = Bool (2)
Int = T₃ (3)
Int = T₂ (4)
T₁ = F → T₂ (5)
T = A → T₁ (6)

制約の連立方程式を解く

この制約を解いて、仮でおいた型を Int, Bool, → で表すことがここでの目的となります。それでは解いていきましょう。

まず、制約 (3) を使って T₃ に Int を代入します。そうすると、制約 (1) は F = Int → Int (1') となります。ここでもう1度制約を書き出すと下記となります。

F = Int → Int (1')
A = Bool (2)
Int = T₃ (3)
Int = T₂ (4)
T₁ = F → T₂ (5)
T = A → T₁ (6)

この調子で解いていきます。(4) を (5) に代入すると。

F = Int → Int (1')
A = Bool (2)
Int = T₃ (3)
Int = T₂ (4)
T₁ = F → Int (5')
T = A → T₁ (6)

(2) を (6) に代入すると。

F = Int → Int (1')
A = Bool (2)
T₃ = Int (3)
T₂ = Int (4)
T₁ = F → Int (5')
T = Bool → T₁ (6')

(1') を (5') に代入すると。

F = Int → Int (1')
A = Bool (2)
Int = T₃ (3)
Int = T₂ (4)
T₁ = (Int → Int) → Int (5'')
T = Bool → T₁ (6')

(5'') を (6') に代入すると。

F = Int → Int (1')
A = Bool (2)
Int = T₃ (3)
Int = T₂ (4)
T₁ = (Int → Int) → Int (5'')
T = Bool → (Int → Int) → Int (6'')

求まりました。求まった型を項と並べると下記となります。

fun(a) { fun(f) { if a then 0 else f(1) } } : Bool → (Int → Int) → Int
- a : Bool
- fun(f) { if a then 0 else f(1) } : (Int → Int) → Int
  - f : Int → Int
  - if a then 0 else f(1) : Int
    - 0 : Int
    - f(1) : Int
      - 1 : Int

直感にも反しませんね！

まとめ

しくみ自体は結構簡単だなと感じられたのではないかと思います。問題は制約型付け規則をきちんと作るところです。TaPL ではきちんと作れたかどうかを数学的に証明していくのですがそれが大変ですね。

型推論に頼れば型註釈を書かずにプログラムを書けるのですが、プログラムをまちがえたときにデバッグがしにくくなったり、他人が読みにくくなったりするので、トップレベルの関数については型を明記すべきだと思います。実際 Haskell のコンパイラーである GHC ではトップレベルの関数に型註釈がなければ警告が出ます。

Java や C# などの言語にこれくらい強力な型推論を付けたくなるかもしれませんが、おそらく多相性（部分型多相）や暗黙の型変換のあたりが障害となって実現できないと思います。型推論は TaPL では第22章で解説されますが、第23章で出てくる System F という計算体系では、「全く型註釈のない全てのプログラムで型推論することはできない」ということが言及されています。どこまで型推論を実現するのか、どこまで多相性を認めるのか、というところは、言語設計者が考える必要のある重要なバランスだと思います。

おまけ

ここで説明した内容を実装しています。 https://github.com/kakkun61/TaPL/tree/master/Chapter22Reconstruction

Haste コンパイラーを使って Haskell から JavaScript に変換してこのページで動くようにしようと思ったんですが、生成した JS を V8 に読ませると Type Error と言うので諦めました……

明日

明日は k-saka が「Unity なんでもインスペクタに表示していくやつ」を書きます。

お楽しみに。

このブログについて

KLabのゲーム開発・運用で培われた技術や挑戦とそのノウハウを発信します。

記事検索

このブログについて

KLabのゲーム開発・運用で培われた技術や挑戦とそのノウハウを発信します。

型推論のしくみ

『型システム入門』

そもそも型とは

型推論とは

これから議論する言語

型推論の手掛かり

実際に制約型付け規則を適用してみる

制約の連立方程式を解く

まとめ

おまけ

明日

このブログについて

記事検索

おすすめ

このブログについて

記事検索