Re: ML & HOL
河野真治 @ 琉球大学情報工学です。
In article <070516084728.M0143621@utogw.gssm.otsuka.tsukuba.ac.jp>, kuno@gssm.otsuka.tsukuba.ac.jp writes
> 型推論は型がないのと同じなんて教えないでくださいよ〜(泣) 久野
同じってのは言いすぎか...
> 型のない言語では矛盾があってもそれにぶちあたる経路を実行しない
> と間違いが発現しない。テストで全部の経路を通ることは不可能。発現
> したときに「何がわるかったか」も探求しないといけない。コンパイラ
> の出す型エラーの方が洩れもないし解りやすいしずっといいでしょ。
一方で、世の中を複雑にしているものの一つでもありますね。
「プログラム書くときに最適化を考えるな」と言いつつ、double
にするか float にするか悩むのを強制されるのも、実はうっとうしい。
Open/GLみたいに、引数の型毎に違う関数が用意されているのを
見たりすると「なんだかなぁ」と思います。
Cだとポインタで渡せば、型なんてないも同然だしな。
ML の「別に、型宣言なんて要らないんだよ」ってのは、それなりに
説得力はありますね。
---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科
Fnews-brouse 1.9(20180406) -- by Mizuno, MWE <mwe@ccsf.jp>
GnuPG Key ID = ECC8A735
GnuPG Key fingerprint = 9BE6 B9E9 55A5 A499 CD51 946E 9BDC 7870 ECC8 A735