Tipos inductivos parametrizados en Agda

Question

Estoy leyendo Dependent Types at Work. En la introducción de tipos parametrizado, el autor menciona que en esta declaración

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

del tipo de List es Set → Set y que se convierte en A argumento implícito a ambos constructores, es decir.

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

Bueno, he intentado volver a escribir un poco diferente

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

que lamentablemente no funciona (estoy tratando de aprender Agda durante dos días más o menos, pero por lo que deduje que es porque los constructores están parametrizados en Set₀ y entonces List A debe estar en Set₁).

De hecho, se acepta la siguiente

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

sin embargo, ya no soy capaz de utilizar {A : Set} → ... → List (List A) (lo cual es perfectamente comprensible).

Entonces mi pregunta: ¿Cuál es la diferencia real entre List (A : Set) : Set y List : Set → Set?

¡Gracias por su tiempo!

Answer 1

Me tomo la libertad de cambiar el nombre de los tipos de datos. El primero, que es indexados en Set será llamado ListI, y la segunda ListP, tiene Set como un parámetro:

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 

En tipos de datos parámetros ir antes de que el colon, y los argumentos después de la de colon son llamados indicies. Los constructores se pueden utilizar de la misma manera , se puede aplicar el conjunto implícito:

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

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

hay diferencia cuando se trata de patrones. Para la versión indexada tenemos:

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

Esto no se puede hacer para ListP:

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

El mensaje de error es

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

ListP también se puede definir con un módulo comodín, como ListD:

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

open Dummy public 

Quizás un poco sorprendente, ListD es igual a ListP. No podemos patrón partido en el argumento de Dummy:

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

Esto da el mismo mensaje de error como para ListP.

ListP es un ejemplo de un tipo de datos parametrizado, que es más simple de lo ListI, que es una familia inductivo: es "depende" de los índices del , aunque en este ejemplo de una manera trivial.

tipos de datos parametrizados se definen en the wiki, y here es una pequeña introducción.

familias inductivos no son muy definidos, pero detallados en los registros the wiki con el ejemplo canónico de algo que parece necesitar inductivas familias:

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

Sin tener en cuenta el índice de Tipo, una versión simplificada de esto no podía ser escrito en el Dummy -module forma de lam constructor.

Otra buena referencia es Inductive Families por Peter Dybjer de 1997.

feliz Agda de codificación!