Re: ML & HOL
久野です。
kono@ie.u-ryukyu.ac.jpさん:
> 型宣言をプログラムコードから推論する型推論と言うのが売りで
> す。ということは、型がないのと同じ。
何書いてるんですか。違うでしょ。
> 自分で矛盾しない限りエラーにならない。
矛盾があればコンパイル時に解る。大切じゃないですか。
> 型推論は実は、Prolog のunification と同じだから、型のない
> Prologと、型推論のMLとは、実は、ほとんど同じ。
型のない言語では矛盾があってもそれにぶちあたる経路を実行しない
と間違いが発現しない。テストで全部の経路を通ることは不可能。発現
したときに「何がわるかったか」も探求しないといけない。コンパイラ
の出す型エラーの方が洩れもないし解りやすいしずっといいでしょ。
型推論は型がないのと同じなんて教えないでくださいよ〜(泣) 久野
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