Parameterized Inductive Types

Examples

A data type declaration can depend on a sequence of parameters. For example, the type of lists is parameterized on the type A of elements:

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

This will introduce the constructors (*** note this refers to implicit arguments! ***)

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

A data type declaration can depend on more than one parameter. For example, Martin-Löf’s wellordering type is a type of trees with variable branching factor, is defined as follows:

 data W (A : Set) (B : A → Set) : Set where
    sup : (x : A) → (B x → W A B) → W A B

A node sup x f has branching type B x. The type W A B has two parameters: the family B x of branching types indexed by x : A and the index set A.

General form

Parameters can have arbitrary types, and later parameters can depend on elements of earlier parameters (cf the W-example).

The general form of a (simple) parameterized type declaration is

 data D (p1 : P1) … (pn : Pn) : Set where
   c1 : A1
   …
   cn : An

The name D of the data type and the names c1, …, cn of the constructors must be new wrt the current signature and context.

Agda checks that the parameter types P1, …, Pn are correct types wrt the current context. (Later parameter types can depend on earlier parameters.) Moroever it checks that A1, …, An : Set wrt the current signature and context extended with the p1 : P1,… ,pn : Pn.

Moreover, each Ai has the form

 (y1 : B1) → … → (ym : Bm) → D p1 … pn 

where an argument types Bi of the constructors is either

  • non-inductive (a side condition) and does not mention D at all,
  • or inductive and has the form
 (z1 : C1) → … → (zk : Ck) → D p1 … pn 

where D must not occur in any Cj.

Note that all occurences of D are of the form of D p1 … pn - the parameters are constant over the definition! In the following section we shall introduce “inductive families” (indexed families of sets) where this is not required.

Parameterized inductive families and inductive-recursive types

Below we will introduce more general classes of data types: the inductive families, the inductive-recursive types, and the inductive-recursive families. Declarations of such data types can be parametrized in a similar way as above.