Parametrized Inductive Types in Agda

Question

Sto solo leggendo Dependent Types at Work. Nell'introduzione al parametrizzato tipologie, l'autore afferma che in questa dichiarazione

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

il tipo di List è Set → Set e che A diventa implicita argomento per entrambi i costruttori, vale a dire.

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

Beh, ho provato a riscrivere un po 'diverso

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

che purtroppo non funziona (sto cercando di imparare Agda per due giorni o giù di lì, ma da quello che ho raccolto è poiché i costruttori sono parametrizzati su Set₀ e pertanto List A devono essere in Set₁).

Infatti, il seguente è accettata

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

tuttavia, non sono più io sono in grado di utilizzare {A : Set} → ... → List (List A) (che è perfettamente comprensibile).

Quindi la mia domanda: qual è la differenza effettiva tra List (A : Set) : Set e List : Set → Set?

Grazie per il vostro tempo!

Answer 1

Mi permetto di rinominare i tipi di dati. Il primo, che è indicizzati Set sarà chiamato ListI, e la seconda ListP, ha Set come parametro:

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 

Nei tipi di dati parametri vanno prima dei due punti, e argomenti che seguono il colon sono chiamati indicies. I costruttori possono essere usati nello stesso modo , è possibile applicare il set implicita:

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

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

Ci

differenza arriva quando pattern matching. Per la versione indicizzata abbiamo:

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

Questo non può essere fatto per ListP:

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

Il messaggio di errore è

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

ListP può anche essere definita con un modulo fittizio, come ListD:

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

open Dummy public 

Forse un po 'sorprendente, ListD è uguale a ListP. Non possiamo modello corrispondenza sull'argomento per Dummy:

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

Questo dà lo stesso messaggio di errore come per ListP.

ListP è un esempio di un tipo di dati parametrizzato, che è più semplice rispetto ListI, che è una famiglia induttivo: essa "dipende" dal indicies, sebbene in questo esempio in modo banale.

tipi di dati parametrizzati sono definite sulla the wiki, e here è una piccola introduzione.

famiglie induttivi non sono realmente definiti, ma elaborati in in the wiki con l'esempio canonico di qualcosa che sembra avere bisogno induttivi famiglie:

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

Trascurando l'indice tipo, una versione semplificata di questo non poteva essere scritto con il metodo Dummy a causa del costruttore lam.

Un altro buon riferimento è Inductive Families da Peter Dybjer dal 1997.

codifica

Felice Agda!