gadt - Agda のパラメーター化された誘導型

Answer 1

データ型の名前を自由に変更できます。インデックスが付けられた最初の はSetと呼ばれListI、2 番目ListPの はSetパラメータとして次のようになります。

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

データ型では、パラメーターはコロンの前に置かれ、コロンの後の引数は指標と呼ばれます。コンストラクターは同じ方法で使用でき、暗黙的なセットを適用できます。

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。この例では些細な方法ですが、指標に「依存」します。

パラメータ化されたデータ型はwikiで 定義されています。ここに簡単 な紹介があります。

帰納的な家族は実際には定義されていませんが、帰納的な家族が必要と思われる何かの標準的な例でウィキで詳しく説明されています。

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

Type インデックスを無視すると、これの単純化されたバージョンは、コンストラクターDummyが原因で -moduleの方法で記述できませんでした。lam

別の良い参考文献は 、1997 年の Peter Dybjer によるInductive Familiesです。

ハッピーアグダコーディング！