# 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.