Hindley-Milner型推論アルゴリズムをF#で書いてみた
この記事は F# Advent Calendar 2014の21日目の記事です。昨日はc0hamaさんの「Linux で F# を始める」でした。
いきなり弁解から入りますが、この記事は「Hindley-Milner型推論アルゴリズムをGroovyで書いてみた」というid:uehajさんの記事を単にF#で写経しました。という話をします。
動機
そもそもなんでそんなことをしようと思ったのか、
- 今年のICFPC2014でSECDマシン用のコンパイラを作る課題が出てmini-ML文法の独自DSLを作る。
- その言語がMLっぽい文法のくせに型検査がなくて開発効率が悪かった。
- よし、型検査を入れよう。ついでに型推論も入れよう。
- ネットで調べると日本語のコメント付きですげーわかりやすいブログ発見。
- →とりあえず、すぐに試せるF#で書き写してみよう。
という感じで作業していたら、テストが通るようになったので勢いでアドベントカレンダーにも登録するという暴挙にでてしまいました。
「HM型推論といえばML」ぐらいの重要機能だし（と勝手に思ってる）、F＃もMLファミリーなのでなんか絡んでるだろうと思ったんです。しかし、実際に書いてみたらぜんぜんF#関係ありませんでした。ごめんなさい。
でも、そんな中２マインドの俺にHM型推論がわかった気にさせてしまうF＃ってすごいなーと思うんです。
HM型推論に関しては確実に元のGroovyとScalaのソースを見たほうがよいでしょう。
特にGroovy版についているコメントは大変わかりやすいのでお勧めです。
その他、ネットで調べられるものはmin-camlのtyping.mlがいいと思います。これも日本語の解説があるので分かりやすいです。
Groovy版についているコメントも残してF#で自分が書いたソースはGistに置きました。
最後に下のテストが通ったときは、超少ないコードで型推論できるなんてHindleyさんとMilnerさんマジ、スゲーと思った。
そして、とても分かりやすいコメントを書いてくれたid:uehajさんありがとうございました。
let testShowType() =
// 最終的な型判定のテスト群。
assert (typeInfer.showType(Var("true")) = "Boolean[]")
assert (typeInfer.showType(Var("xtrue")) = "\n cannot type: xtrue\n reason: undefined: xtrue")
assert (typeInfer.showType(Var("zero")) = "Int[]")
let intList = App(App(Var("cons"),
Var("zero")),
Var("nil"))
let zero = Var("zero")
let one = App(Var("succ"), Var("zero"))
assert (typeInfer.showType(intList) = "List[Int[]]")
assert (typeInfer.showType(App(Var("isEmpty"), intList)) = "Boolean[]")
assert (typeInfer.showType(App(Var("head"), intList)) = "Int[]")
assert (typeInfer.showType(App(Var("tail"), App(Var("head"), intList))).StartsWith("\n cannot type: zero\n reason: cannot unify Int[] with List["))
assert (typeInfer.showType(App(Var("tail"), App(Var("tail"), intList))) = "List[Int[]]") // runtime erro but type check is OK
assert (typeInfer.showType(App(App(App(Var("if"), Var("true")), zero), one)) = "Int[]")
assert (typeInfer.showType(App(App(App(Var("if"), Var("true")), intList), one)) = "\n cannot type: succ\n reason: cannot unify List[Int[]] with Int[]")
let listLenTest = LetRec("len",
Lam("xs",
App(App(App(Var("if"),
App(Var("isEmpty"), Var("xs"))),
Var("zero")),
App(Var("succ"),
App(Var("len"),
App(Var("tail"),
Var("xs"))))
)),
App(Var("len"),
App(
App(Var("cons"),
Var("zero")),
Var("nil"))
)
)
assert (listLenTest.ToString() = "letrec len = λ xs . (((if (isEmpty xs)) zero) (succ (len (tail xs)))) in (len ((cons zero) nil))")
assert (typeInfer.showType(listLenTest) = "Int[]")
F#化したときに感じたこと
- 判別共用体のコンストラクタをその型の派生クラスみたいに扱いたいけどやり方がわからない。
type Type =
| Tyvar of tyvar
| Arrow of Type * Type
| Tycon of string * Type list
with
override this.ToString() =
match this with
| Tyvar x -> x
| Arrow(t1, t2) -> sprintf "(%s -> %s)" <| t1.ToString() <| t2.ToString()
| Tycon(k, ts) -> k + "[" + (ts |> List.map string |> String.concat ",") + "]"
//F#: 本当はTypeを継承したTyvar型を定義したかったけど、
// うまいやり方が分からないのでstringの別名としてtyvarを作ってお茶を濁す
and tyvar = string このときTyvar of tyvarというのをTyvarという型として扱いたかった。
うまいやりかたがあれば誰か教えてください。
- F#関係ないけど、テスト重要。自明なものから始めてやりたいことの全容を書いておくというのは超大事。
それと、F#のテスト関連は何が標準なんだろうか？C#/C++みたいなMSTestがすぐ使えるのはないのだろうか？
- F#は.NETのクラスを利用できたりfloatの演算を+.みたいににしてないから、型推論が弱いのはわかる。だけど、ラムダのパラメーターとかよく型推論してくれないので、型注釈書かないといけない。F#もHM型推論の仲間ならもっとガンバレと思う。
- でも、F#がVisualStudioに標準で入っているという手軽さがやっぱりいい。もっと仕事で使えるようになりたい！
