gadt - Agda 中的参数化归纳类型

Answer 1

I take the liberty to rename the data types. The first, which is indexed on Set will be called ListI, and the second ListP, has Set as a parameter:

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

In data types parameters go before the colon, and arguments after the colon are called indicies. The constructors can be used in the same way, you can apply the implicit set:

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

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

There difference comes when pattern matching. For the indexed version we have:

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

This cannot be done for ListP:

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

The error message is

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

ListP can also be defined with a dummy module, as ListD:

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

open Dummy public

Perhaps a bit surprising, ListD is equal to ListP. We cannot pattern match on the argument to Dummy:

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

This gives the same error message as for ListP.

ListP is an example of a parameterised data type, which is simpler than ListI, which is an inductive family: it "depends" on the indicies, although in this example in a trivial way.

Parameterised data types are defined on the wiki, and here is a small introduction.

Inductive families are not really defined, but elaborated on in the wiki with the canonical example of something that seems to need inductive families:

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

Disregarding the Type index, a simplified version of this could not be written with in the Dummy-module way because of lam constructor.

Another good reference is Inductive Families by Peter Dybjer from 1997.

Happy Agda coding!