Parametryzowane typy indukcyjne w Agdzie

Question

Po prostu czytam Dependent Types at Work. We wstępie do sparametryzowane typy, autor wspomina, że ​​w tej deklaracji

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

rodzaj List jest Set → Set i że A staje niejawny argument obu konstruktorów, czyli tzw.

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

Cóż, starałem się go przerobić nieco inaczej

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

który niestety nie działa (Próbuję nauczyć Agda na dwa dni lub więcej, ale z tego co zebrałem to ponieważ konstruktory są parametryzowane przez Set₀, a więc List A musi być w Set₁).

Rzeczywiście, co następuje akceptowane

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

jednak nie jestem już w stanie wykorzystać {A : Set} → ... → List (List A) (co jest całkowicie zrozumiałe).

Moje pytanie: jaka jest rzeczywista różnica między List (A : Set) : Set a List : Set → Set?

Dziękujemy za poświęcony czas!

Answer 1

Używam uprawnień do zmiany nazw typów danych. Pierwszy z nich, który jest indeksowane na Set zostanie wywołana ListI, a drugi ListP, ma Set jako parametr:

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 

typów danych parametrów przejść przed dwukropkiem, a argument po okrężnicy są nazywane oznaczenia. Konstruktorzy mogą być używane w tym samym sposób można zastosować niejawny zestaw:

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

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

Nie

Różnica pojawia się, gdy pasujące do wzorca. Dla wersji indeksowanej mamy:

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

To nie może być zrobione dla ListP:

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

Komunikat o błędzie jest

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

ListP może być również zdefiniowane w moduł manekina, jak ListD:

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

open Dummy public 

Być może nieco zaskakujące, ListD jest równa ListP. Nie możemy wzór meczu na argument Dummy:

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

Daje to ten sam komunikat o błędzie, jak dla ListP.

ListP jest przykładem parametryczne typu danych, który jest prostszy niż ListI , który jest rodzina indukcyjny: to „zależy” na indeksów, chociaż w tym przykładzie w trywialny sposób.

parametryzowane typów danych są zdefiniowane the wiki, i here jest mała wprowadzenia.

rodziny indukcyjne nie są naprawdę określone, ale rozwinęły się the wiki z kanonicznym przykładem czegoś, co wydaje się potrzeba indukcyjnych rodzin:

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

Pomijając indeks typu, uproszczona wersja tego nie dało być napisany w trybie Dummy -moduł z powodu konstruktora lam.

Innym dobrym przykładem jest Inductive Families Petera Dybjer od 1997

Szczęśliwy Agda kodowania!