なので、自動車メーカーが言ってる文脈での「若者のクルマ離れ」って、そういう所からメーカーが認識して危機感を持ってる話なので、雑誌とか新聞とかがてきとうに書くような(?)「若者の○○離れ」とはちょっと違う感じがあるっぽさ><
クルマ売れる売れないじゃなく、実際に整備士になってる人々までもが(整備士になる前に)趣味的に興味を持ってもらえてなくてヤバい><
雑に言うと、Haskellerがいう型システムだと「『リンゴが3つ』と『バナナが3つ』はこの場合は同じ」みたいな発想だけど、Ada的発想でいう型システムだと「まず果物にそろえよ! そもそもバナナが3つってなんだ!? 房か!?本数か!?質量か!? 数え方と単位も明示せよ!」って感じかも?><
前者だと現在の小学校の算数の教え方とあんまり変わらない・・・><
Ada方式の方が小学校1年生くらい?での「1ってなに? なんで1の次は2なの?」とか「おにぎり+おにぎりはでっかいおにぎりじゃん!? さんすうわけわからない さんすうきらい・・・」みたいなことを小学校で教えたり救ったりできるかも?><
それを踏まえると単に「型システム」と言うと、Haskellerが思い浮かべる物を指す方がより正確(?)なんだろうけど、じゃあ『その応用でAdaみたくガチガチで頭堅くて「明示的!!明示的記述!!命名せよ!!!暗黙は人を殺すミスを犯す!!!」みたいな、型を書かせる事によって齟齬を検出する意味での型システム』ってなんて言うんだろ?><
この齟齬、Adaの発想の延長で「小学校の算数にも(Ada的発想の)型システムを!>< そうすれば教えるの楽だろうし混乱しないかも><」って言ってる意図は、Haskellerとかその辺の方々にはそのままだと通じない可能性?><; ていうか、だからこそ数学界隈の方々は否定する?><;
だから、オレンジには、Haskellが「型ありき!」「型ありき!」とかいいながら、
「なんで型推論多用するの?>< プリミティブ型(? 標準ライブラリの型)そのまま使うの?>< それじゃ(ヒューマンエラーの観点から言うと)、型がゆるふわな言語と対して変わらないじゃん?><」
と見えたのかも><
でも、Haskellerの方々にしてみれば、弱い型つけの言語は自明ではない記述(?)が出来てしまう、Haskellのように十分に(?)強い型つけの言語であれば、記述は自明(?)になる(あるひとつの意味としか読むことが出来ない)ので、実用的に(型)安全であるということになるのかも?><
Haskellとかがいう型ありきは、プログラム意味論とかで、推論や自明性(?)を活用して記述を楽する(?)為に型を使うみたいな感じ?><
(めちゃくちゃ雑にいうとジェネリクスとかそういうのの超すごいやつ(?))
一方、Adaの型ありきは、それを元にむしろ制限させる事の為に、同じように抽象化できる物を、ヒューマンエラーを検出する為に明示的にのみ行わせると言う発想?><
ていうか、
https://mstdn.nere9.help/@orange_in_space/101389196152287067
これ読んだ瞬間に
「Haskellは型ありきの発想で...」
「Adaみたいに型システムを活用してヒューマンエラーを検出する方が型ありきじゃん!?>< 型作ってよ!>< 型書いてよ!><」
の間の齟齬がどういうことかやっとわかったかも><
これ、どういう人が書いたのか全くわからず(情報系の先生なのは本文からわかるけど)、単にググって「おもしろいなるほど><」 と思って読んでtootしてそして最後まで読んで、それからやっと「何の研究してる先生なんだろ?><」とリンクをクリックして、ぞわっと来た><
"インタラクティブメディア・ユーザーインタフェース・情報可視化・..."(以下略)
https://fukuchi.org/index.html.ja
読みかけだけどおもしろい><(読みかけなのにtootするほどに><)
-- プログラムを数学の言葉で理解すること https://fukuchi.org/essay/2015/math-or-machinecode.html
Span<T>構造体 - C# によるプログラミング入門 | ++C++; // 未確認飛行 C
https://ufcpp.net/study/csharp/resource/span/