[過去ﾛｸﾞ]
次世代言語13 Go Rust Swift Kotlin TypeScript (1002ﾚｽ)
次世代言語13 Go Rust Swift Kotlin TypeScript http://mevius.5ch.net/test/read.cgi/tech/1534769753/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
必死ﾁｪｯｶｰ(本家)
(べ)
自ID
ﾚｽ栞
あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
501: デフォルトの名無しさん [sage] 2018/09/06(木) 05:51:15.46 ID:YGmGLZO1 >>492 それは、どこまでを依存型と呼ぶかが難しいんだ 型の属性として(実行時の)値を使えるというだけなら結構多くの言語ができる Adaも最初の83からできるし、最近のFortranもできる。C言語もVLAに限ればできる。勿論動的な言語はほぼ全部できる しかし依存型と言われて期待するのは証明、それも静的なヤツなわけで これは型と型の関係を記述できる関数(熟語)をかなり強力なレベルで書けないとできない あと、厳密にラムダキューブに則った定義しか認めないとなると、関数型言語以外はどんなに強力でも全滅ってことになるし http://mevius.5ch.net/test/read.cgi/tech/1534769753/501
503: デフォルトの名無しさん [sage] 2018/09/06(木) 06:21:10.79 ID:YGmGLZO1 あー実行時なのか静的なのかどっちだよってなってるな、スマン 証明とは全く別の話として、型に実行時の値を持たせられると便利だよねってグループがあって で、単に値から型を作れるというだけでいいならそういうのも依存型と呼べてしまう、と言いたかったがぐじゃぐじゃになった 静的に証明をするなら勿論値もコンパイル時の値でないとだめなわけだけど そこでもコンパイル時の型レベル関数と実行時の関数が完全に切り離されてるのか(C++のtemplateみたいな) 証明に使える関数を実行時にも普通の関数として使えるのか(Agda等)とまたグループがあるし まあつまり、人によって「依存型」という言葉に期待する度合いが違うので 今後最小の機能しか持たない「依存型」が出てきて定理証明系クラスタを怒らせるのはあるかもとちょっと恐々としてるんだ…… (単に右辺の型を使うだけのものを「型推論」と呼んだ例みたいな) http://mevius.5ch.net/test/read.cgi/tech/1534769753/503
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
1.386s*