2

リーン チュートリアルの最初の 3 つの章を完了し、命題論理でいくつかの証明を既に完了しました。

今、私は少し戻って、愚かな質問を自問しようとしています.

私の理解は次のとおりです。

  1. 項には次のタイプがあります: constant A : Type. Aは用語でTypeあり、 のタイプですA。
  2. 用語はタイプになることができます: constant a : A.
  3. 用語のタイプは、別の用語のタイプに依存するconstant B : A -> Type場合があります。constant B' : Π (a : A), Type

しかし、このコードは型チェックを行っていないため、この理解は明らかに間違っています。

constant A : Type

constant a : A

constant B : A -> Type

constant B' : Π (a : A), Type

constant C : Π (b : B), Type

constant C' : Π (B : A), (Π (b : B), Type)

constant C'' : B -> Type

で始まるすべての行constant C、つまり行 9、11、および 13 でエラーがスローされます。error: type expected at B

なんで？すべての項が型になるわけではないと思います。タイプが他のタイプに依存する用語はタイプになれないのではないかと思います。なんで？

4

1 に答える 1

1

最初のタイプのエラー

の最初のタイプのエラーの問題

constant C : Π (b : B), Type

は typeの関数(定義なし) であるb : Bため、 とは言えません。つまり、は型ではなく値です。or orのような主張をしても意味がありません。BA -> TypeBb : 1b : "xyz"b : (λ a : A, Type)

たとえば、次のように動作しますB a : Type。

constant C : Π (b : B a), Type

2 番目のタイプのエラー

の 2 番目のタイプのエラー

constant C' : Π (B : A), (Π (b : B), Type)

が型であることがわかっていないという事実に由来します。B私たちが知っているのBは、それが type の何らかの値 (住民) であるということだけですA。そのように使用できるようにするにはB、次のようなものが必要です。

constant C' : Π (B : Type), (Π (b : B), Type)

つまりB、型であると明示的に言います。

第三種の誤り

constant C'' : B -> Type

これが型チェックに失敗する理由は、最初のケースと同じです。Bここでは型が必要ですが、これが機能する理由constant B : A -> Typeです。

于 2016-12-08T10:09:01.793 に答える