型理論の入門文書

最近プリントアウトして読み散らかしてる（初心者向け）文書の紹介．Lisperだというのに静的型に浮気してスマソ（ぉ
J. Hughes先生のリンク集がイイ！ 基本的にここに載ってるものから選んでいる．
http://www.cs.chalmers.se/~rjmh/tutorials.html
Hughes先生は なぜ関数プログラミングは重要か で有名だが，個人的には「遅延評価は譲れないね☆」にはついて行けない... あれは「操作」を捨て去って「概念」に移行することを強制するからなぁ...
リンク集にL. Cardelli氏の文書がいくつか載ってるけど，他にもサイトには読み易そうな文書が置いてある（小難しそーなのが大量にあるけど）．
http://www.luca.demon.co.uk/
実は2chで教えてもらってあれこれ調べるきっかけになった Basic Polymorphic Typechecking は，易しめだが初心者には「へぇへぇ」なポイントで一杯だ（「ジェネリック」/「ノンジェネリック」の違いなど）．付録にModula-2で書かれた型推論プログラムの実装が付いてる．
On Understanding Types, Data Abstraction, and Polymorphism は長くて字も詰まってるんでほぼ未読（行間が狭杉）．基本的なところ（ポリモルフィズムの分類，λ式とは）から始まって∀な型（いわゆる「ジェネリック」「ポリモルフィック」），∃な型（構造体型に使う？），部分型へと続く．ところで「型とはイデアルだ」って節があるけど，Basic ... で「型を値の集合として捉えると関数型の意味が不明確だ」って書いてなかったか？
P. Wadler先生は言うまでもなく著明な大物だ．しかし写真を初めて見て ... （以下略
「なぜモナドなのか」「どうしてそんなに嬉しいのか」についての Monads for Functional Programming は素人向けに非常に噛み砕いて書いていてうれしい（直接には型と関係ない？）．かなりの説得力で，つりこまれてしまいそう．でもな...
Haskellの特徴である型クラスの実装原理が Typeclasses in Haskell にある．Haskellはよく知らないしまだ読み途中だが，個人的にはDictionaryの型が気になる．関数とDictionaryの両方を格納できるコンテナ？（笑 まじめな話をすると，Haskellではポリモルフィックな関数には型を内部で陽に付けているらしい．
その他， Javaの拡張に関する文書群辺りはJava 1.5のGenericsの実装に相当影響したんじゃないだろうか． 言語デザインに関する文書群は比較的気軽に読めそうなタイトルが多い．HOT: Higher-OrderでTypedな言語について，とか．