ParameterizedInductiveTypes

See the official user manual for the most up-to-date version of the information on this page.

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 c₁, ..., c_n of the constructors must be new wrt the current signature and context.

Agda checks that the parameter types P₁, ..., P_n are correct types wrt the current context. (Later parameter types can depend on earlier parameters.) Moroever it checks that A₁, ..., A_n : Set wrt the current signature and context extended with the p₁ : P₁,... ,p_n : P_n.

Moreover, each A_i has the form

 (y1 : B1) -> ... -> (ym : Bm) -> D p1 ... pn 

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

 (z1 : C1) -> ... -> (zk : Ck) -> D p1 ... pn 

where D must not occur in any C_j.

Note that all occurences of D are of the form of D p₁ ... 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.