# 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 (p_{1}: P_{1}) … (p_{n}: P_{n}) : Set where c_{1}: A_{1}… c_{n}: A_{n}

The name D of the data type and the names c_{1}, …, c_{n} of the constructors must be new wrt the current signature and context.

Agda checks that the parameter types P_{1}, …, P_{n} are correct types wrt the current context. (Later parameter types can depend on earlier parameters.) Moroever it checks that A_{1}, …, A_{n} : Set wrt the current signature and context extended with the p_{1} : P_{1},… ,p_{n} : P_{n}.

Moreover, each A_{i} has the form

(y_{1}: B_{1}) → … → (y_{m}: B_{m}) → D p_{1}… p_{n}

where an argument types B_{i} of the constructors is either

*non-inductive*(a*side condition*) and does not mention D at all,- or
*inductive*and has the form

(z_{1}: C_{1}) → … → (z_{k}: C_{k}) → D p_{1}… p_{n}

where D must not occur in any C_{j}.

Note that all occurences of D are of the form of D p_{1} … p_{n} - 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.