[過去ﾛｸﾞ]
次世代言語13 Go Rust Swift Kotlin TypeScript (1002ﾚｽ)
次世代言語13 Go Rust Swift Kotlin TypeScript http://mevius.5ch.net/test/read.cgi/tech/1534769753/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
503: デフォルトの名無しさん [sage] 2018/09/06(木) 06:21:10.79 ID:YGmGLZO1 あー実行時なのか静的なのかどっちだよってなってるな、スマン 証明とは全く別の話として、型に実行時の値を持たせられると便利だよねってグループがあって で、単に値から型を作れるというだけでいいならそういうのも依存型と呼べてしまう、と言いたかったがぐじゃぐじゃになった 静的に証明をするなら勿論値もコンパイル時の値でないとだめなわけだけど そこでもコンパイル時の型レベル関数と実行時の関数が完全に切り離されてるのか(C++のtemplateみたいな) 証明に使える関数を実行時にも普通の関数として使えるのか(Agda等)とまたグループがあるし まあつまり、人によって「依存型」という言葉に期待する度合いが違うので 今後最小の機能しか持たない「依存型」が出てきて定理証明系クラスタを怒らせるのはあるかもとちょっと恐々としてるんだ…… (単に右辺の型を使うだけのものを「型推論」と呼んだ例みたいな) http://mevius.5ch.net/test/read.cgi/tech/1534769753/503
511: デフォルトの名無しさん [sage] 2018/09/06(木) 09:56:35.47 ID:3Abdeyqw >>503 多分言わんとする所は理解できた こちらとしては証明を含めた静的な世界での依存型が難しいという話で、単に型に値を含めるようなのはそちらの言うとおり既に実務向け言語でいくつか有るので、それらは依存型から除いて流行らないと言ってしまったな http://mevius.5ch.net/test/read.cgi/tech/1534769753/511
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.041s