orange @[email protected]

それを踏まえると単に「型システム」と言うと、Haskellerが思い浮かべる物を指す方がより正確（？）なんだろうけど、じゃあ『その応用でAdaみたくガチガチで頭堅くて「明示的！！明示的記述！！命名せよ！！！暗黙は人を殺すミスを犯す！！！」みたいな、型を書かせる事によって齟齬を検出する意味での型システム』ってなんて言うんだろ？＞＜

ていうか、Haskellとかその辺の型システム（以下『前者』）って、人間と計算機の間の齟齬を最小限にしつつも記述を簡潔にする為にあって、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>使ったこと無かったけど、オーディオバッファとかでコピーすると遅くてマズい場面で、バッファそのままと始点と有効な長さを渡すよりもSpan<T>の方がエレガント？＞＜

よくみたら鍵括弧もおかしくなってるしもう駄目＞＜；

x気がしてる？＞＜
o気がしてる＞＜

C# だと「ブロックに入る時初期化出る時開放（IDisposeとusing）」GCが動いてオブジェクトが破棄される時（ファイナライザ（名前変わった？））」はあるけど、「スコープが外れた時（＝参照カウントがゼロになった時に）にGCを待たずすぐに」が無い点が不便な気がしてる？＞＜
（それがあるとそればっかり気軽に使われてせっかくのGCの最適化（？）が・・・ってなるのを避ける為なんだろうけど＞＜）

IDisposeの実装ややこしいけど、今のVSだとこういう風に解説のコメントありで補間してくれるのでわかりやすいかも？＞＜

あと記事の途中の例示が、それ両向じゃなくINTPじゃん感＞＜

MBTIのようなものでテストする度に最初のEとIがコロコロ変わるようならば、この記事の通り両向なんだろうけど＞＜