-
TuvianNavy
- 1535
- 2
- 0
- 0
-
- いいね！0
(change of )*state
@TuvianNavy
型システムを壊れたままにしておく（完全性を追求しない）ことで組み合わせ爆発を根本から断つことができる（計算機科学にも敗北主義ってあったんだ）
2021-01-14 09:52:52
(change of )*state
@TuvianNavy
全称量化も存在量化も要するにユニバースの全件検索ができるかどうかということで、できない場合は個体記号を使った陳述しかできない、これmonadicとかいうやつだっけ
2021-01-14 09:26:23
(change of )*state
@TuvianNavy
実装上の問題として、複数のアトミックドメインに属する値は（キャストのことはとりあえず忘れてよう）字句的に区別がつかないといけない、、だから型の暗黙の実装は字句解析やシンボル解決などに散在してしまう
2021-01-14 09:37:06
(change of )*state
@TuvianNavy
訂正：実装上の問題として、値リテラルの属するアトミックドメインは（キャストのことはとりあえず忘れてよう）字句的に区別がつかないといけない
2021-01-14 13:42:37
(change of )*state
@TuvianNavy
プログラムの一部がコンパイルを通ったかどうか、を、別のところで条件コンパイルの入力として使いたい、現状ではこれはMakefileやそこから呼ばれるシェルスクリプトたちなどビルドシステムの支援が必要
2021-01-09 10:24:53
(change of )*state
@TuvianNavy
AgdaやCoqの証明の中で別の定理が証明済かどうかは判るはずなので、つまりこれがC++に入ればビルドシステムは必要なくなる
2021-01-09 10:28:10
(change of )*state
@TuvianNavy
プログラミング言語でもSQLでもぼーっとしているとnull値の類が入り込むし、それは論理を破壊する
2021-01-14 09:38:45
(change of )*state
@TuvianNavy
暗黙の実装の散在、とか、monadic、とか、null値、とか、ともかく壊れた型システムというのはいつのまにか存在していがち
2021-01-14 09:48:37
(change of )*state
@TuvianNavy
これを直して完全性を実現するのが結構非効率でねえ、というか、完全性という言葉が出てきたらどこかでブルートフォースが必要になるということ
2021-01-14 09:49:58
(change of )*state
@TuvianNavy
翻訳時と実行時の連携に必要な情報の引継ぎはABIというかリンカ仕様の問題になってくるので、この引継ぎができないせいで型システムが壊れたままになるというのもあるか（仕事で下請けがプロパーさんの見てるgitlab見れないとかよくあるっしょ）
2021-01-14 10:00:56