の住人でも、の住人でType 1もない人の例は? Idris REPL を調べている間、何も思いつきませんでした。TypeType
より正確には、次の結果が得られるものx以外を探しています。Type
Idris> :t x
x : Type 1
2 に答える
7
私は型理論の専門家ではありませんが、私の理解は次のとおりです。Idris チュートリアルには、セクション12.8 Cumulativityがあります。タイプユニバースの内部階層があると言われています：
Type : Type 1 : Type 2 : Type 3 : ...
そして for any は for any をx : Type n意味x : Type mしますm > n。型推論で起こりうるサイクルをどのように防止するかを示す例もあります。
Type (n+1)しかし、このヒエラルキーは内部使用のみであり、 にない値を作成する可能性はないと思いますType n。
型理論におけるユニバースおよび型の型に関する nLab の記事も参照してください。
idris-dev リポジトリーのこの問題も役に立つかもしれません。Edwin Brady はそこで、設計と実装に関する論文(セクション 3.2.2 を参照) を参照しています。
于 2014-11-12T22:08:44.033 に答える