昨日見たけど、選曲的にえじょさんが興味持つかな？＞＜； ってちょっと思った＞＜
昨日見たけど、選曲的にえじょさんが興味持つかな？＞＜； ってちょっと思った＞＜
"バスト占いのうた歌ってみた" を YouTube で見る https://youtu.be/85MTpYdwweQ
こんなカッコイイ声して初投稿がこれか……（困惑）
"【新人デビュー】3Dのクオリティだけは業界No.1！！！！！※当社比【2年ぶり】" を YouTube で見る https://youtu.be/v0eh9-ufEyM
え！？
新人かっこよ！
テンセグリティ構造、なにかに応用できないか色々妄想するけど、結局L字の固い部分が圧縮に対してかなり強くないといけないので、アーム式の継ぎ手とかの方がだいたいよくなる？＞＜ ってなってる＞＜
オレンジの発想の範囲では、設計が楽ってメリットくらいしか思いつけない・・・＞＜
これ＞＜
セリアで『夏休みの自由研究キット』としてテンセグリティ構造が売っていたけどレベル高すぎませんか？「とても欲しい！」「科学に興味を持ちそう」 - Togetter https://togetter.com/li/2184005
それ、ついに100円ショップの商品になったってtogetter昨日見た＞＜
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
「静的に型が決まっていたとしても、静的型検査せずに実行するのに静的型付けって言うのはおかしい」って点と、「タグつき共用体のサポートがあったら、もう部分的に動的型付けに近いと言えそうだし、BASICほど全面的に活用してたらもう静的型付けを名乗れないでしょ？」辺りが論点になりそう＞＜；
古典的BASICインタプリタは静的型付けであるか動的型付けであるかって、実用的ではない議論だけどちゃんといろんな人が意見したらすごくおもしろそう＞＜
(ちょっとググって見たけど、静的に分類してる人の方が多い？＞＜)
エラーが含まれていることを実行なしに確実に判定できるなら静的と言って良いと思う (その検査が本当に実行前に行われるかは別の話？)
「ただしエラーが含まれている可能性がある」の種類によると思うけど
一般に「静的」とは「実行せずとも確認できる」を意味していると思う (e.g. 静的解析)
となると例えば
「全ての変数等には明示的な型の宣言が必要で、一方でインタプリタであり、全体の実行前には型検査は行われず、実行時に型検査を行う」って珍妙な環境があったとしたら、それは「実行時までに型検査は行われないけど、静的型つけな言語」になる？＞＜；
検査が実行時ってだけであって、実行前に型は決まってる(ただしエラーが含まれている可能性がある)ので＞＜；
このアカウントは、notestockで公開設定になっていません。
わからないことや興味深い事を教えてくれる博識なリアル友人なんて滅多に見つけられるものじゃないと思うけど、ビル・ゲイツにとってのポール・アレンがそういう稀有な事例かもって思うかも＞＜
世の中にポール・アレンみたいな人はそんなに居そうも無いし、SNSならば大人数で知識を出しあってポール・アレンひとり分くらいの能力(？)を発揮出来る可能性が、ポール・アレンとお友だちになる可能性よりは高そうな気がしてる＞＜
オレンジはそれをSNSに求めてるし、だから逆にわかんなくて困ってる人を見かけたらオレンジが知ってる範囲だけでも教えてあげようとしてるし、ついでに調べるのも手伝ってあげたりする＞＜
オレンジもそうしてほしいから＞＜
2chに居た時もそう＞＜(お節介エスパーテックサポートとか＞＜)
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
となると例えば
「全ての変数等には明示的な型の宣言が必要で、一方でインタプリタであり、全体の実行前には型検査は行われず、実行時に型検査を行う」って珍妙な環境があったとしたら、それは「実行時までに型検査は行われないけど、静的型つけな言語」になる？＞＜；
検査が実行時ってだけであって、実行前に型は決まってる(ただしエラーが含まれている可能性がある)ので＞＜；
古典的BASICは、動的型つけでは無く、「タグつき共用体をフル活用する事で結果的にまるで動的型つけでゆるふわな言語かのように振る舞ってる(し、表面上はゆるふわ)」って、
最初にBASIC使ってから30年くらい？経つけど、そんな話聞いた事無かったけど、よく考えてみると初歩の初歩である「なんでドルがついてない変数には文字列が入らないの？＞＜」を突き詰めて考えれば、厳密にはたしかになるほど＞＜；
まあ厳密な話をするなら、システムプログラミング言語はハードウェア由来の不確定性とか諸々と向き合うことになるので完全無欠な保証は難しかったりするんだけど、 C/C++ の穴はそういう次元ではないので……
みんな外付けで不完全な仕組みをゴテゴテ付けながら騙し騙し頑張ってるんだけど、土台が腐ってるからどうしようもないのよ。だから、これだけ長く使われていて多数のプラットフォームで動くという圧倒的アドバンテージを持ちながら、他の言語に移行したい！ とかいう声が沢山ある
C/C++ が安全だと心から思ってる人、地球上に存在するん？
「文字列と数値を足せるこの言語ヤバすぎィ！」に対して「この言語は型安全です！ (文字列と数値を足すと必ず異常終了します)」はヤバさを全く否定できてないんよ。挙動とか以前の問題でそもそも実行できる時点でヤバいと言っているわけで。
ていうか、今の議論で今さらふと気づいたけど、古典的BASICって、厳密には動的型つけ環境じゃなくて静的型つけ環境であり、
バリアント型は持っていても動的型は持っていないのでつまり定義上、環境としては静的型検査は行われないのに(ただしプログラム実行時に行単位で静的型検査をしてるとも言える？)、しかしながら静的型つけな言語？＞＜；
C/C++ は、あれだけ使われていながら、すべての実行可能な記述について挙動がちゃんと定義されているわけではないという、類稀なるクソ言語です (歴史的経緯ェ……)
実用性はそれはそうだけど、TaPLとかで説明されてる型安全はそうではなく、C/C++は、そういう厳密な意味で型安全では無い環境ではないの？＞＜；
良い喩えかは知らないけど、「この車は状況と操作に対して必ず再現性のある振る舞いをします。たとえば時速128kmでブレーキを踏むとブレーキは壊れて確実に効かなくなります！」というのは型安全のいう “安全” の範疇なわけ。クソ。
我々が求める安全性ってのはそうじゃなくて「ブレーキが壊れて効かなくなるような速度をそもそも出せません」でしょう
じゃあ “実用的” な観点での型システムが保証してくれる安全性とは何なのかといえば、「『はい異常終了！！！』とか『手遅れになってから例外飛ばしてあげるね♡』とかいう挙動がそもそも起きない」という点で、巷で言われている安全とかそうでないとか静的型付きがどうとかの話はだいたいこれ
狭義の型安全性すら持たない実用言語、探してくる方が難しいぞ (言うまでもないが C/C++ はカウントしない)
例外として C/C++ はそのベースラインを大幅に下回る史上最強の殿堂入りクソ言語です、掛け値なしに
だから結局のところ型安全かどうかをというのは言語や型システムの設計者の心配事なのであって、ユーザはそれを当然のベースライン保証として考えるんだから、巷の実用言語について “型安全性” を論ずることに実用的な意味はほとんどなくない？ ということです
型安全の範疇ではあるかもしれないが、その有難味は如何程か、という話
https://mastodon.cardina1.red/@lo48576/110698823590524781
で、プログラム書いてるとき気付けなくて実際にある程度動かしてから突然「はい異常終了！」と言われるの、未定義動作より “少しマシ” な程度でしかなくない？ という
ワイ「hoge型が想定されてるストレージにfuga型書き込んだろwww」
プログラム「はい型が違いま〜すwww異常終了！！！」
↑ みたいな例を考えたとき、異常終了が必ず保証されているならこれは型安全性を破ったことにならない
なんらかの結果、ある場所にhoge型として値が書き込まれたとして、「よーし、fuga型の値として扱うぞ」ってなった時に
型安全・明示的「駄目です。それはhoge型での値で、fuga型として扱うなら明示的に指定してくれたら互換性がある型なので変換できます」
型安全・暗黙的「互換性があるのでだいじょうぶ！ 変換しとくね！」
型安全じゃ無い「ええんやない？ 知らんけど」
かも？＞＜
https://mstdn.nere9.help/@orange_in_space/110698764108611611
オレンジのこの説明だと「32bit整数型？ 知るか！ 32bit float型としてアクセスしてやる！」ってつまり情報無視での扱いも型安全って事になっちゃうからダメだね＞＜；
そもそもそういう考え方は「アドレス」という概念を持たない言語に対して全く効力がないので、モデル化に失敗していると思う
例えば hoge+fuga を piyopiyo番地に書けって命令を実行したとして、
で、そのあとにpiyopiyo番地～のメモリを見て、「ところでここにあるバイナリはなに？＞＜」ってなった時に「さぁ・・・？」ってなるのが型安全じゃなくて、「なんとか型でかんとかって値が置いてあります！」ってわかるのが型安全
って事じゃないの？＞＜；
その文脈での「マシさ」には度合いがあって、動的型付き言語はそのマシさにおいて最底辺に近い、ということをわかってほしいという話
あらゆる不都合な動作を「例外が飛びます」とか「終了コード127でプログラムが終了します」とかの “定義済の挙動/状態” へと飛ばしてしまえばそれは “型安全” な言語になるんだけど、それで？ という話でしかない。
極論を言えば「未定義動作で必ず abort() する拡張されたC言語」みたいなものがあったらそれは型安全といえるはず。
で、サイレントに狂わなくなるのは確かにだいぶマシではあるが、所詮マシなだけなのよね
それはそうだけどJavaは定義上型安全で、学校のテストで「Javaは型安全な環境であるか？」に「違う！＞＜」って書いたら不正解なんでしょ？＞＜；
で、定義済の挙動であることはわかったけど、そもそも実行時に型エラーが出るようなプログラムを実行できてしまうのは本当に嬉しさ十分なんですか？ というのが、開発者が向き合うべき本当の問題なのよ
たとえば「Javaは型安全です！」というのは「Javaの書き換え可能な配列型は共変なんだけど、型エラーの際には ArrayStoreException が飛ぶという定義済の挙動になるから、プログラム全体としての振る舞いはちゃんと想定されたものになっています！」というのを含意している、ということをまず了解する必要がある。
オレンジ的にも心情的にPerlも古典的BASICも「どこが型安全なんだよ！＞＜；」って思ってるけど、
そう思いながら「Adaがもっと普及するべき！＞＜＃ 」ってブーブー言いながら調べた時に「型安全って言葉はそういう意味じゃないですよ」になって「そうなの？＞＜； 変なの！＞＜；」になったので、混乱してる＞＜
結局、型安全の話って、いろんなのが入り混じってて整理しきってないよね、いや、整理はされてるんだけど、それをきっちり理解してる人って少ないよねという。
俺も理解しているうちには入らない。
Perlは型安全なのかというと、気持ち悪いの一言に尽きる。PHPはもっと気持ち悪い。結局Rubyで落ち着いている。
よくわからないけど、TaPLの第一章にはPerlも安全に分類されてるし、wikipedia英語版を見るとBASICの型安全はstrongに分類されてる・・・＞＜
手続き型言語だとその辺りのハンドリングがややこしいんだけど (操作的意味論)
でも、それだと、例えば型Aと型Bで演算した時に、型Bの方の値によって、型Aが返ってきたり、型Bが返ってきたり、型Cが返ってきたりする言語って型安全ではないになる・・・？＞＜(？)
オレンジ的には「そんなの型安全じゃないよ！＞＜」だけど、学問的にはそれも型安全であるってことになってるんじゃないの・・・？＞＜
で、これらを合わせると、「型のつく項が、型を保ったまま、値になるまで行き詰まることなく評価できる (または永久に値にできないまま評価し続ける破目になる)」というのが型システムの安全性 (健全性) という性質である、ということになる
[EDIT: 修正した (https://mastodon.cardina1.red/@lo48576/110698616033544189)]
保存: 項 t に型がついて t が項 t' へと評価できるなら、 t' には t と同じ型がつく。
ようは評価してたら急に型が変わったりしないという話
進行: 項 t に型がつくなら、 t は値であるか、または別の項へと評価できる。
項ってのは大雑把には「式」みたいな概念だと思っといていいかも
お金が無い(し、英語力がない)ので無料で読める第一章しか読んでない＞＜；
TAPL を参照するなら §8.3『安全性 = 進行 + 保存』がドンピシャの節か？
算術式がメモリを破壊するとかしないとか、そういう考え方はしない。
そもそも一般的な「計算」をメモリと CPU とかいう限定的なアーキテクチャで考えない
情報系の大学とかでのテストで「型安全とは何か？」って問題で、メモリ上のデータの安全性に注目した答えを書かないとバツになるんじゃないの・・・？＞＜ オレンジはそういう風に解釈してた＞＜
そもそもメモリ破壊とかを持ち出すのがレイヤー違いという感じがする (たとえば単純な項書換え系の言語を考えたときメモリ破壊もクソもない)
スパコンの雪だるまアイコンの人がFediverseに来てくれたら便利なのに＞＜；
オレンジも明示的な型変換な環境の方が好きだけど、世の中の人々が「冗長！」って馬鹿にしてくる21世紀・・・＞＜
型安全はどうでもいいから、振る舞いの滅茶苦茶さと記述の気持ち悪さをどうにかしてくれ、みたいな方。とはいえ、振る舞いの滅茶苦茶さの中に、勝手に型変換するよ～、便利でしょ？？みたいなのも入ってるのかもしれん。
あえて雑に言うと、型の誤りを原因にしてメモリを破壊する事が無い環境が狭義の型安全だったはずたぶん＞＜；
(TaPLを読んでる真面目な人が代わりに説明してほしい＞＜；)
人々は型安全なプログラムを書きたいわけではなく振る舞いの良いプログラムを書きたいのだから
うんちみたいな動作するけど型安全だよ！ というのがアリで、それを了解できるなら、それ以上型安全であることそのものを論じたってに実際的は嬉しくないでしょ (理論的なあれこれはさておき)
それはそうで、同時に「狭義型安全かどうか」そのものの有難味の本質に目を向けろという話なんだよな
前に、「静的型つけと動的型つけってどう違っててなんで静的型つけの方がいいの？」とか「なんで型をガチガチにするの？」みたいな疑問がFediverse上で話題になった時にも、オレンジしか「静的か動的かと、ガチガチゆるふわは別の話だよ！＞＜ 文字列型と数値型で足し算が出来るかどうかも動的静的と無関係だよ！＞＜」って説明しなくて、他の人がみんな混同した説明してたのでオレンジが憤慨してた＞＜(？)
ていうか、説明がおかしい気がするけど、狭義の型安全ってそういうものでは感＞＜
静的で強い型つけが好きな人々(＞＜含む)からしたら、弱すぎて足りなすぎる「よくそんなの使う気になるね＞＜；」だけど、
例えば、文字列型と数値型で足し算が出来るか例外出すか、あるいは結果が数値になるか文字列型になるかみたいなのは、型安全かどうかや、静的動的であるかにも、直接は関係ない＞＜
「/bin/sh ではあらゆる変数は文字列型で定義済の動作をするから静的型付きで型安全」
「クソみたいなコードを書いても定義済の動作をするから †型安全† です！」って、そりゃそうだが、その嬉しさの程度がいかほどのものかちゃんと考えたんか……？ という感想にはなるな
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
書いた＞＜
Re:観光特化 (#.4493334) | JR東日本、2022年度の輸送密度を公表。55区間が1000人未満 | スラド https://srad.jp/comment/4493334
なんか、本当にこの場所がドキュメンタリー番組とかで紹介されたあの場所で、1万人以上の日系人が収容されてた場所って＞＜
ドキュメンタリー番組とかで見てる範囲だとどうしても現実に今もその場所があるって実感がちょっと減っちゃってるかも＞＜
NHKとかのドキュメンタリーで見るのと、ほぼリアルタイムのyoutubeライブの散策で見るの、全然感覚違うし、木々が多いのも景色が想像以上にきれいだったのも驚きだし、そのアメリカの風景のなかに漢字で「慰霊塔」って書かれた石碑が現れるの、写真で見た時と比べ物になら無いほどの衝撃だった＞＜
配信してたスマホが電動キックボードからとれて落ちてストリーム途切れちゃったっぽい？＞＜；
マンザナー、歴史番組での当時の写真とか、ドキュメンタリー番組での紹介だと緑があんまり無いイメージだけど、時期によってはこんなに緑が多くなるんだね＞＜
ほとんどタンブルウィードっぽいけど＞＜
新しい枠出来た＞＜
"BigRigTravels LIVE from Lone Pine, California. ( Jul 11, 8:22 AM )" を YouTube で見る https://www.youtube.com/live/tPd4knvsyWs?feature=share
ストリーム切れちゃった＞＜；
マンザナー日系人収容所跡地を電動キックボードで散策するっぽい？＞＜
なんか、マンザナー日系人収容所跡地に寄ってる！＞＜
"BigRigTravels LIVE from Independence, California. ( Jul 11, 7:49 AM )" を YouTube で見る https://www.youtube.com/live/9EO20ePuK9k?feature=share
