型理論

それほど勉強したわけではないですが、Curry-Howard 対応ぐらいは知ってます。
　http://tinyurl.com/yol7mf

「当然のことながら，プログラムというのは，Curry-Howardの対応を理解して、初めて「書ける」と言うものです．」
　http://tinyurl.com/cpret6

という人もいるけど、そうは思わないな。(かっこ良いから勉強する価値はあります)

もともと型理論って、カントールの集合論の矛盾「あらゆる集合を含む集合」を避けるために導入されたもの。

プログラム言語の場合は、実質的に有限集合しか扱わないから、濃度的な矛盾はないです。自己言及命題は、ループを持つデータ構造として現れてくるだけ。何も考えないアルゴリズムだと無限ループしたりするけど、避けるのは簡単。

で、僕が型理論がプログラム言語に不要だと思う根拠の一つは「型抜きでプログラムは動くから」だと思う。Perl とか Smalltalk とか、JavaScript とか。

正しく動くことを証明すること自体には型理論は不要。証明されたプログラムに、エルブラン的な型を付けるのは自明。

でも、プログラムに型が役に立つなら、勉強する価値はあると思う。でも、どうかなぁ。

プログラミング言語 Standard ML 入門
　http://tinyurl.com/dlwo5z

MLって実は、型宣言がない。プログラムコードそのものが型宣言だから。と言うことは、例えば、Java から型宣言を取り除いて、MLの型推論を行なって、型エラーを表示するってことは可能なんだよね。

もちろん、それをClass/Interface で補助するとか、IDEが型情報を利用して補完候補を出すとかに使えることは理解できます。

でも、そのために、Generic とかTemplate で、振り回されるのはいただけないなぁ〜

逆に、MLを使えば、そのあたりから解放されるってのはあるんだけど、SMLは module の実行時loadとかが、たこで、実用的でないと思う。Prolog とか Smalltalk/Squeak 的。

オブジェクトは関数言語ではClosureで実現できるので、そのあたりがまずいとは思いませんが、必要以上に「型」を連発されるのは苦痛。