ていうか、
https://mstdn.nere9.help/@orange_in_space/101389196152287067
これ読んだ瞬間に
「Haskellは型ありきの発想で...」
「Adaみたいに型システムを活用してヒューマンエラーを検出する方が型ありきじゃん！？＞＜ 型作ってよ！＞＜ 型書いてよ！＞＜」
の間の齟齬がどういうことかやっとわかったかも＞＜
Haskellとかがいう型ありきは、プログラム意味論とかで、推論や自明性（？）を活用して記述を楽する（？）為に型を使うみたいな感じ？＞＜
（めちゃくちゃ雑にいうとジェネリクスとかそういうのの超すごいやつ（？））
一方、Adaの型ありきは、それを元にむしろ制限させる事の為に、同じように抽象化できる物を、ヒューマンエラーを検出する為に明示的にのみ行わせると言う発想？＞＜
だから、オレンジには、Haskellが「型ありき！」「型ありき！」とかいいながら、
「なんで型推論多用するの？＞＜ プリミティブ型（？ 標準ライブラリの型）そのまま使うの？＞＜ それじゃ（ヒューマンエラーの観点から言うと）、型がゆるふわな言語と対して変わらないじゃん？＞＜」
と見えたのかも＞＜
でも、Haskellerの方々にしてみれば、弱い型つけの言語は自明ではない記述（？）が出来てしまう、Haskellのように十分に（？）強い型つけの言語であれば、記述は自明（？）になる（あるひとつの意味としか読むことが出来ない）ので、実用的に（型）安全であるということになるのかも？＞＜
この齟齬、Adaの発想の延長で「小学校の算数にも（Ada的発想の）型システムを！＞＜ そうすれば教えるの楽だろうし混乱しないかも＞＜」って言ってる意図は、Haskellerとかその辺の方々にはそのままだと通じない可能性？＞＜； ていうか、だからこそ数学界隈の方々は否定する？＞＜；
