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

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

まあつまり、人によって「依存型」という言葉に期待する度合いが違うので
今後最小の機能しか持たない「依存型」が出てきて定理証明系クラスタを怒らせるのはあるかもとちょっと恐々としてるんだ……
(単に右辺の型を使うだけのものを「型推論」と呼んだ例みたいな)