Data Types¶
Simple datatypes¶
Example datatypes¶
In the introduction we already showed the definition of the data type of natural numbers (in unary notation):
data Nat : Set where
zero : Nat
suc : Nat → Nat
We give a few more examples. First the data type of truth values:
data Bool : Set where
true : Bool
false : Bool
The True
set represents the trivially true proposition:
data True : Set where
tt : True
The False
set has no constructor and hence no elements. It
represents the trivially false proposition:
data False : Set where
Another example is the data type of non-empty binary trees with natural numbers in the leaves:
data BinTree : Set where
leaf : Nat → BinTree
branch : BinTree → BinTree → BinTree
Finally, the data type of Brouwer ordinals:
data Ord : Set where
zeroOrd : Ord
sucOrd : Ord → Ord
limOrd : (Nat → Ord) → Ord
General form¶
The general form of the definition of a simple datatype D
is the
following
data D : Setᵢ where
c₁ : A₁
...
cₙ : Aₙ
The name D
of the data type and the names c₁
, …, cₙ
of
the constructors must be new w.r.t. the current signature and context,
and the types A₁
, …, Aₙ
must be function types ending in
D
, i.e. they must be of the form
(y₁ : B₁) → ... → (yₘ : Bₘ) → D
Parametrized datatypes¶
Datatypes can have parameters. They are declared after the name of the datatype but before the colon, for example:
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
Indexed datatypes¶
In addition to parameters, datatypes can also have indices. In
contrast to parameters which are required to be the same for all
constructors, indices can vary from constructor to constructor. They
are declared after the colon as function arguments to Set
. For
example, fixed-length vectors can be defined by indexing them over
their length of type Nat
:
data Vector (A : Set) : Nat → Set where
[] : Vector A zero
_∷_ : {n : Nat} → A → Vector A n → Vector A (suc n)
Notice that the parameter A
is bound once for all constructors,
while the index {n : Nat}
must be bound locally in the constructor
_∷_
.
Indexed datatypes can also be used to describe predicates, for example
the predicate Even : Nat → Set
can be defined as follows:
data Even : Nat → Set where
even-zero : Even zero
even-plus2 : {n : Nat} → Even n → Even (suc (suc n))
General form¶
The general form of the definition of a (parametrized, indexed)
datatype D
is the following
data D (x₁ : P₁) ... (xₖ : Pₖ) : (y₁ : Q₁) → ... → (yₗ : Qₗ) → Set ℓ where
c₁ : A₁
...
cₙ : Aₙ
where the types A₁
, …, Aₙ
are function types of the form
(z₁ : B₁) → ... → (zₘ : Bₘ) → D x₁ ... xₖ t₁ ... tₗ
Strict positivity¶
When defining a datatype D
, Agda poses an additional requirement
on the types of the constructors of D
, namely that D
may only
occur strictly positively in the types of their arguments.
Concretely, for a datatype with constructors c₁ : A₁
, …, cₙ :
Aₙ
, Agda checks that each Aᵢ has the form
(y₁ : B₁) → ... → (yₘ : Bₘ) → D
where an argument types Bᵢ of the constructors is either
non-inductive (a side condition) and does not mention
D
at all,or inductive and has the form
(z₁ : C₁) → ... → (zₖ : Cₖ) → D
where
D
must not occur in any Cⱼ.
The strict positivity condition rules out declarations such as
data Bad : Set where
bad : (Bad → Bad) → Bad
-- A B C
-- A is in a negative position, B and C are OK
since there is a negative occurrence of Bad
in the type of the
argument of the constructor. (Note that the corresponding data type
declaration of Bad
is allowed in standard functional languages
such as Haskell and ML.).
Non strictly-positive declarations are rejected because they admit non-terminating functions.
If the positivity check is disabled, so that a similar declaration of
Bad
is allowed, it is possible to construct a term of the empty
type, even without recursion.
{-# OPTIONS --no-positivity-check #-}
data ⊥ : Set where
data Bad : Set where
bad : (Bad → ⊥) → Bad
self-app : Bad → ⊥
self-app (bad f) = f (bad f)
absurd : ⊥
absurd = self-app (bad self-app)
For more general information on termination see Termination Checking.