引き続き、型システムの勉強をしつつ、ラムダ計算の体系を実装している。
型再構築
型検査に関しては以前までの記事の時点である程度できている。
次は「型再構築」を実装したい。型再構築は、ざっくり言うと、関数の引数の型を省略した場合でも処理系が適切に型を判断してくれる機能のことである。
注意して欲しいのは、「関数の中で（初期値付きで）定義される変数の型や、関数の結果の型を明示しなくていい」のは型再構築ではない、ということである。変数はその初期値を見れば型がわかるし、関数の結果の型は関数の本体を見ればわかる。
「型推論」という語は「関数の引数の型を省略できること」と「変数の型や関数の結果の型を省略できること」の両方に使われるようだが、実装者の観点からするとこの2つは違う種類のものなので、あまり良い用語とは言えない。
型再構築については TaPL の第22章で扱われている。単純型付きラムダ計算に関しては、 TaPL を読めば普通に実装できる。
let 多相
ML とか Haskell では、 let 式を使うと多相的な関数を書ける。つまり、
(\f. (f 1, f True)) (\x. x)
とは書けないが、
let f = \x. x in (f 1, f True)
は型チェックが通る。前者の f は単相的（？）だが、後者の let で定義された f は多相的なのである。
これを実装する際は、 let 式に遭遇した時は定義された変数の型を一般化して、その変数を使う際に具体化する。言葉にすると簡単だが、文脈に登場しない型変数だけを一般化する必要があって面倒である。また、単純型の場合は制約集合を計算した後に単一化を一回行うだけで良かったが、 let 多相では let 式が出現するたびに単一化を行う。面倒くさい。
そんなわけで一ヶ月ぐらい（他のこともやりつつ）あーだこーだ言っていたが、この度、ようやくそれっぽいものが実装できた。現在の実装は綺麗とはとても言えないが、 GitHub に上げてある。
https://github.com/minoki/LambdaQuest/blob/master/src/LambdaQuest/LetPoly/TypeCheck.hs
多相と言えば前に System F を実装したが、その時は（型再構築がないので）関数の引数の型を省略できないし、型抽象や型適用を明示的に書く必要があった。ちなみに、System F では型再構築が決定不能らしい。
拡張の方向性
もっと複雑な型システムを持つ体系では、当然、型再構築の話題もこれだけでは終わらない。
レコード型に関しては型変数に加えて列変数というのを使って制約を記述するらしい。Haskellには型の制約として型クラスがあるのは御存知の通りだ。
私としては部分型のある体系での型再構築に興味があるのだが、これに関しては、 TaPL には「有望な初期成果が報告されているが、実用的な検査器はまだ広く普及していない」とある。そこに挙げられている論文は読んでみるつもりだが、実用的な検査器が広く普及していないというのは何か理論的、技術的な困難があるのだろうか。それとも、単に普及している関数型言語に部分型を持つものが少ないという意味だろうか。
とにかく、部分型、特に交差型を持つ体系での型再構築の研究と実装が、今後の課題である。