[過去ログ] 次世代言語13 Go Rust Swift Kotlin TypeScript (1002レス)
前次1-
抽出解除 必死チェッカー(本家) (べ) 自ID レス栞 あぼーん

このスレッドは過去ログ倉庫に格納されています。
次スレ検索 歴削→次スレ 栞削→次スレ 過去ログメニュー
501: デフォルトの名無しさん [sage] 2018/09/06(木) 05:51:15.46 ID:YGmGLZO1(1/2) AAS
>>492
492(1): デフォルトの名無しさん [sage] 2018/09/06(木) 02:01:31.14 ID:3Abdeyqw(1/3) AAS
依存型難し過ぎて流行らないよなぁって気持ちが強いがどうなんだろうな
Ada20に採用されたら笑う
それは、どこまでを依存型と呼ぶかが難しいんだ

型の属性として(実行時の)値を使えるというだけなら結構多くの言語ができる
Adaも最初の83からできるし、最近のFortranもできる。C言語もVLAに限ればできる。勿論動的な言語はほぼ全部できる

しかし依存型と言われて期待するのは証明、それも静的なヤツなわけで
これは型と型の関係を記述できる関数(熟語)をかなり強力なレベルで書けないとできない

あと、厳密にラムダキューブに則った定義しか認めないとなると、関数型言語以外はどんなに強力でも全滅ってことになるし
503
(1): デフォルトの名無しさん [sage] 2018/09/06(木) 06:21:10.79 ID:YGmGLZO1(2/2) AAS
あー実行時なのか静的なのかどっちだよってなってるな、スマン
証明とは全く別の話として、型に実行時の値を持たせられると便利だよねってグループがあって
で、単に値から型を作れるというだけでいいならそういうのも依存型と呼べてしまう、と言いたかったがぐじゃぐじゃになった

静的に証明をするなら勿論値もコンパイル時の値でないとだめなわけだけど
そこでもコンパイル時の型レベル関数と実行時の関数が完全に切り離されてるのか(C++のtemplateみたいな)
証明に使える関数を実行時にも普通の関数として使えるのか(Agda等)とまたグループがあるし

まあつまり、人によって「依存型」という言葉に期待する度合いが違うので
今後最小の機能しか持たない「依存型」が出てきて定理証明系クラスタを怒らせるのはあるかもとちょっと恐々としてるんだ……
(単に右辺の型を使うだけのものを「型推論」と呼んだ例みたいな)
前次1-
スレ情報 赤レス抽出 画像レス抽出 歴の未読スレ AAサムネイル

ぬこの手 ぬこTOP 1.390s*