18/09/06 05:51:15.46 YGmGLZO1.net
>>492
それは、どこまでを依存型と呼ぶかが難しいんだ
型の属性として(実行時の)値を使えるというだけなら結構多くの言語ができる
Adaも最初の83からできるし、最近のFortranもできる。C言語もVLAに限ればできる。勿論動的な言語はほぼ全部できる
しかし依存型と言われて期待するのは証明、それも静的なヤツなわけで
これは型と型の関係を記述できる関数(熟語)をかなり強力なレベルで書けないとできない
あと、厳密にラムダキューブに則った定義しか認めないとなると、関数型言語以外はどんなに強力でも全滅ってことになるし