河野真治 @ 琉球大学情報工学です。

In article <040908162853.M0183605@sma.gssm.otsuka.tsukuba.ac.jp>, kuno@gssm.otsuka.tsukuba.ac.jp writes
>   未だに型の理論は判りません。型と型に包含関係があって、Javaのイ
 ...
> 「プログラミングの役に立つように」定式化できてるんだろうか。そう
> いうのがスッキリ扱えるという論文知ってたら教えてください。

(久野さんがそういうこというの? なんか、ずるいなぁ)

僕も、前の記事で (で、割りと役に立たないわけだが...) とか書
いてあったりするわけですけど。

型の理論よりも、値の理論の方が面白いと僕は思う。

>      そういう部分では現実は理論より奇なりという気がする。  久野

「実装は理論より面白い」じゃないですか?

型理論も ML の自動的な型整合として実装されてみると「なるほど、
便利！」って感じがしますね。Lisp と同じで、その世界にはまると
気持ち良いらしい。

一方で、C++ のTemplate みたいな感じで ad-hoc にすると「そうか、
こういうぐちゃぐちゃなものになってしまい、整合性もなくなるのか」
という感じ。

そういう意味で、型理論だと、シグネチャとかユニフィケーション
とかはやさしいし、かっこいいし、役に立つ感じ。C++ より ML が
いいのは何故かっていうのに「きれいな型理論があるから」って
言えるじゃないですか。

別に万人が、そこまで理解する必要があるってわけでもないんでし
ょうけど。

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科