Hatena::ブログ(Diary)

 | 

2010-12-26

型推論はどのようにして実装されているか - ラムダプラス+の紹介

この記事は Haskell Advent Calendar jp 2010 のために書かれた物です。(20日目)

型推論は簡単

MLHaskell のような言語の型推論は、型推論を知らないみなさんが考えているよりは遥かに簡単な物です。大雑把に言ってしまえば、構文木全体を探索して、同一である事が明らかな型同士の単一化をしていけば型推論できてしまうのです。

型推論の難しい所その1 - 多相型

しかし、型推論にも難しい事が無いわけではありません。まず最初の難関としては多相型が挙げられます。

ML や Haskell では let などの変数束縛に対して多相型が導入されています。式の中でこれらの変数が出現すると、その型の型変数(確定していない部分)を全て付け替える操作が発生します。

しかし、確定していない部分を付け替えるという事は、最終的に元の型が確定した後にその操作をしなければ、型を正しく推論する事ができません。ML に let と let rec がある理由の1つがこれです。再帰関数に対する型推論では、自分自身の型を多相型にしない事によって型推論の正しさを保証しています。

型推論の難しい所その2 - 依存関係解析

では、Haskell ではどうでしょうか。Haskell のトップレベル定義は、お互いに参照可能な束縛の並びが含まれています。

これらは ML でいえば全体が let rec で書かれているのと同じ状態にありますが、Haskell は適切に多相型を導入する事ができています。なぜでしょう?

Haskell の型推論では、定義同士の参照関係のグラフから推論順序と多相型の導入に関する問題を適切に解決するようになっています。

型推論の難しい所その3 - 純粋関数型言語で実装すると

静的型付け関数型言語の型推論に関する多くの資料は、その対象や実装言語として ML を使用している事が多いようです。実際の所、ML はある意味で型推論に都合の良い言語と言えます。

もし Haskell で型推論を実装しようとすると、色々な部分で苦労する事になります。その1つとしては、型変数の扱いが挙げられます。

型の単一化の結果は、型変数への書き込みによって返されます。つまり、型変数は書き込みが可能でなければなりません。

Haskell でこれを簡単に実現するには、型変数を数値として、IntMap などを状態として持つ事で型を管理するといった方法が考えられます。この場合には、型変数への書き込みは状態の書き換えとなります。

しかし、型変数を参照するのに IntMap の中を検索していては、参照を使うのに比べると実行時間が増えてしまいます。それならば、参照を使うのが正しいでしょう。Haskell で参照を使うには……?

型推論は簡単だが、落とし穴が多い

以上のような型推論の簡単な所からちょっと難しい所まで、理論と実装を1冊の本「ラムダプラス+」にしました。冬のコミックマーケットで出ます。

スペースは三日目(12/31) 東ヘ-41b「YUHA」(ヘはカタカナ)です。他にも幾つか本が出るようです。型推論に興味がある方は是非買いに来てください。

ラムダプラス+は、mayah さんとの共著で、1,2章を mayah さんが、3章を私が書きました。(実際の所、私の担当箇所に関しても mayah さんにとても助けて頂きました。ありがとうございます。)

補足

なにやらすごい数のはてなブックマークが付いてしまい驚きました。

コミケまで買いに来れない方が多いようですが、関係者に会う機会があるような方であれば手渡しが可能です。通販の予定は無い気がします。

oskimuraoskimura 2010/12/27 13:35 もし余れば一部ほしいです。

pi8027pi8027 2010/12/27 19:12 有界の会などにも持って行くと思います。余らなければ増刷できるようなので、多分渡せると思います。

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/pi8027/20101226/lambdaplusplus
 |