><https://twitter.com/orange_in_spacehttps://pawoo.net/@orange_in_space
TAPL を参照するなら §8.3『安全性 = 進行 + 保存』がドンピシャの節か?
算術式がメモリを破壊するとかしないとか、そういう考え方はしない。
チューリング機械は計算機のいち実装でしかない
?><;
そもそも一般的な「計算」をメモリと CPU とかいう限定的なアーキテクチャで考えない
情報系の大学とかでのテストで「型安全とは何か?」って問題で、メモリ上のデータの安全性に注目した答えを書かないとバツになるんじゃないの・・・?>< オレンジはそういう風に解釈してた><
そもそもメモリ破壊とかを持ち出すのがレイヤー違いという感じがする (たとえば単純な項書換え系の言語を考えたときメモリ破壊もクソもない)
これ、あってるよね?><;https://mstdn.nere9.help/@orange_in_space/110698517477850292
スパコンの雪だるまアイコンの人がFediverseに来てくれたら便利なのに><;
オレンジも明示的な型変換な環境の方が好きだけど、世の中の人々が「冗長!」って馬鹿にしてくる21世紀・・・><
型安全はどうでもいいから、振る舞いの滅茶苦茶さと記述の気持ち悪さをどうにかしてくれ、みたいな方。とはいえ、振る舞いの滅茶苦茶さの中に、勝手に型変換するよ~、便利でしょ??みたいなのも入ってるのかもしれん。
あえて雑に言うと、型の誤りを原因にしてメモリを破壊する事が無い環境が狭義の型安全だったはずたぶん><;(TaPLを読んでる真面目な人が代わりに説明してほしい><;)
人々は型安全なプログラムを書きたいわけではなく振る舞いの良いプログラムを書きたいのだから
うんちみたいな動作するけど型安全だよ! というのがアリで、それを了解できるなら、それ以上型安全であることそのものを論じたってに実際的は嬉しくないでしょ (理論的なあれこれはさておき)
つまり意味論から逃げるなということなんだけど
それはそうで、同時に「狭義型安全かどうか」そのものの有難味の本質に目を向けろという話なんだよな
前に、「静的型つけと動的型つけってどう違っててなんで静的型つけの方がいいの?」とか「なんで型をガチガチにするの?」みたいな疑問がFediverse上で話題になった時にも、オレンジしか「静的か動的かと、ガチガチゆるふわは別の話だよ!>< 文字列型と数値型で足し算が出来るかどうかも動的静的と無関係だよ!><」って説明しなくて、他の人がみんな混同した説明してたのでオレンジが憤慨してた><(?)
ていうか、説明がおかしい気がするけど、狭義の型安全ってそういうものでは感><静的で強い型つけが好きな人々(><含む)からしたら、弱すぎて足りなすぎる「よくそんなの使う気になるね><;」だけど、例えば、文字列型と数値型で足し算が出来るか例外出すか、あるいは結果が数値になるか文字列型になるかみたいなのは、型安全かどうかや、静的動的であるかにも、直接は関係ない><
「/bin/sh ではあらゆる変数は文字列型で定義済の動作をするから静的型付きで型安全」
「クソみたいなコードを書いても定義済の動作をするから †型安全† です!」って、そりゃそうだが、その嬉しさの程度がいかほどのものかちゃんと考えたんか……? という感想にはなるな
思考の /dev/null