課題４

線形型に関する論文を読んでそれに基づく型推論プログラムを書く

線形型システムとは？

線形型システムとは、プログラム実行中に作られた値が何度使われうるかによって 型を区別するような型システムです。例えば、整数の型はMLの型システムでは単に"int" ですが、 線形型システムでは、高々一回しか使われない整数の型は"int<１>", 何回でも使われうる 整数の型は"int<ω>" のように区別されます。このように型の概念を拡張しても MLと全く同じように自動的に型推論が行なえる （ここでは型の概念が拡張されていますから、 各データが何回使われるかも自動的に推論されることになります）ことが最近になって知られており、 例えば、fn x=>x+1 の型は、∀ｉ>=1, ｊ.(int<ｉ> -> int<ｊ>) のように推論できます。

線形型って何の役に立つの？

プログラム実行中に高々一度しか使われないと分かっているデータについては， コンパイル時にさまざまな最適化を施すことができます。 例えば，近代的なプログラミング言語ではメモリの解放はガベージコレクタという ランタイムシステムを定期的に起動する（ガベージコレクタがすることは， まだ必要だとわかっているレジスタやスタック中のデータからポインタでたどることが できるデータをすべて残し，それ以外のメモリ領域を解放することです）ことによって システムが自動的に行ないますが，一度しか使われないとわかっているデータについては， それを使用後に即座に解放することができます。 さらに，次のようなappend関数の場合、 
   fun append([], l) = l
     | append(x::l1, l2) = x::append(l1, l2)
第一引数のcons cell は他でまだ使われる可能性があるので通常は再利用することができず、 結果として第一引数として渡されるリストはコピーされることになります。しかし、線形型システム を用いると、第一引数が線形型、すなわち一度しかアクセスされないリストであると わかった場合、コピーをせずに破壊的書き換えによってappend を行なうことができます。

課題

この課題では，まず線形型システムに関する最近の論文，例えば次のような論文を最低一つ 読んでもらい，その上で余力があればそれに基づく簡単な型推論プログラムを書いてもらいます。

課題のホームページへ戻る

koba@is.s.u-tokyo.ac.jp