アガダの誘導型誘導

Question

私はただ読んでいるだけです。種類をparametrisedの導入部で、著者はこの宣言

data List (A : Set) : Set where 
    [] : List A 
    _::_ : A → List A → List A 

にListの種類がSet → Setであることを言及し、Aこと、すなわち両方のコンストラクタへの暗黙の引数になります。

[] : {A : Set} → List A 
_::_ : {A : Set} → A → List A → List A 

まあ、私はそれを悲しげに動作しません少し異なる

data List : Set → Set where 
    [] : {A : Set} → List A 
    _::_ : {A : Set} → A → List A → List A 

を（私はそれが何私が集まってから、二日かそこらのためにAgdaを学ぶためにしようとしている書き直してみましたなぜなら、コンストラクタはSet₀よりもパラメータ化されているから、List AはSet₁でなければならないからです。

実際に、以下を

data List : Set₀ → Set₁ where 
    [] : {A : Set₀} → List A 
    _::_ : {A : Set₀} → A → List A → List A 

を受け入れているが、私はもはや（完全に理解している）{A : Set} → ... → List (List A)を使用することができますよん。

私の質問：List (A : Set) : SetとList : Set → Setの実際の違いは何ですか？

ありがとうございました！

Answer 1

私は自由を取ってデータ型の名前を変更します。データ型で

data ListI : Set → Set₁ where 
    [] : {A : Set} → ListI A 
    _∷_ : {A : Set} → A → ListI A → ListI A 

data ListP (A : Set) : Set where 
    [] : ListP A 
    _∷_ : A → ListP A → ListP A 

パラメータはコロンの前に行くと、 コロンの後に引数が呼び出されます。 はSetにインデックス化され、最初のListIと呼ばれる、第二ListP、 は、パラメータとしてSetを持っていますインディーズ。コンストラクタは同じ 方法で使用することができ、あなたは暗黙のセットに適用することができます

nilI : {A : Set} → ListI A 
nilI {A} = [] {A} 

nilP : {A : Set} → ListP A 
nilP {A} = [] {A} 

あり違いをするときパターンマッチングいます。我々が持っているインデックス付きのバージョンの場合：

null : {A : Set} → ListI A → Bool 
null ([] {A})  = true 
null (_∷_ {A} _ _) = false 

これはListPのために実行することはできません。

-- does not work 
null′ : {A : Set} → ListP A → Bool 
null′ ([] {A})  = true 
null′ (_∷_ {A} _ _) = false 

エラーメッセージが

The constructor [] expects 0 arguments, but has been given 1 
when checking that the pattern [] {A} has type ListP A 

ListPも同様に、ダミーモジュールで定義することができていますListD：

module Dummy (A : Set) where 
    data ListD : Set where 
    [] : ListD 
    _∷_ : A → ListD → ListD 

open Dummy public 

おそらく少し驚くべきことに、ListDはListPに等しいです。私たちは、Dummyへの引数のパターン と一致することはできません：

-- does not work 
null″ : {A : Set} → ListD A → Bool 
null″ ([] {A})  = true 
null″ (_∷_ {A} _ _) = false 

これはListPと同じエラーメッセージを表示します。

ListPは、誘導の家族である、単純 よりListIをパラメータ化されたデータ型の例である：それは些細な方法で、この例ではあるが、 なインデックスに「依存します」。

データ型は the wiki上に定義されているパラメータ化

、 と hereが小さく導入です。

誘導家族は本当に定義されていますが、誘導 家族必要があるように見える何かの標準的な例でthe wiki での詳述されていない：型のインデックスを無視

data Term (Γ : Ctx) : Type → Set where 
    var : Var Γ τ → Term Γ τ 
    app : Term Γ (σ → τ) → Term Γ σ → Term Γ τ 
    lam : Term (Γ , σ) τ → Term Γ (σ → τ) 

を、これの簡易版ではできませんでしたlamコンストラクタのために と書かれているのはDummyです。

もう一つの良い参照は1997年

ハッピーAgdaコーディングからピーターDybjerでInductive Families です！