(redirected from ReferenceManual.Datatypes)
This document has been extracted from a literate Agda file, which was tested with Agda 2.3.0
Table of contents
- Example datatypes
- General form
- Formation and introduction rules
- Definition by pattern matching
- Elimination and equality rules
- Large elimination
- Beyond elimination rules
- Large inductive types
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
Then the unit set:
data True : Set where tt : True
The True set represents the trivially true proposition.
data False : Set where
The False set has no constructor and hence no elements. It represent the trivially false proposition.
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
The general form of the definition of a simple data type D is the following
data D : 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 A1, ..., An : Set wrt the current signature and context. Moreover, each Ai has the form
(y1 : B1) -> ... -> (ym : Bm) -> D
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
where D must not occur in any Cj.
The condition that D must not occur in any Cj can be also phrased as D must only occur strictly positively in Bi.
Agda can check this positivity condition.
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 one can write a non-terminating function using them.
The declaration above of the data type I generates a typing
D : Set
which is called the formation rule of D in Martin-Löf type theory. Similarly the typings of the constructors
c1 : A1 ... cn : An
are called the introduction rules of I in Martin-Löf type theory.
When a data type has been declared functions can be defined by pattern matching on its elements. Here are some examples.
_+_ : Nat -> Nat -> Nat m + zero = m m + suc n = suc (m + n) not : Bool -> Bool not true = false not false = true _+'_ : Ord -> Ord -> Ord m +' zeroOrd = m m +' sucOrd n = sucOrd (m +' n) m +' limOrd f = limOrd (\n -> m +' f n)
Agda has a special facility for pattern matching over an empty type. For example, we can define a function from the empty set to an arbitrary other set:
emptyfunction : (C : Set) -> False -> C emptyfunction C ()
This is definition by pattern matching on the elements of False. Since this type has no elements, there are no cases. Agda indicates this by the second line, which tells the system that this is definition by no cases on the second argument.
All these cases are examples of ''structural recursion" (in one argument) on the way an element of a given data type is defined. To each correct data type declaration we can associate a constant (the recursor or elimination constant) which expresses the general principle of structural recursion for the data type. Each such constant is defined by pattern matching:
natrec : (C : Nat -> Set) -> C zero -> ((x : Nat) -> C x -> C (suc x)) -> (z : Nat) -> C z natrec C d e zero = d natrec C d e (suc n) = e n (natrec C d e n) if : (C : Bool -> Set) -> C true -> C false -> (z : Bool) -> C z if C d e true = d if C d e false = e onecase : (C : True -> Set) -> C tt -> (z : True) -> C z onecase C d tt = d nocase : (C : False -> Set) -> (z : False) -> C z nocase C () ordrec : (C : Ord -> Set) -> C zeroOrd -> ((x : Ord) -> C x -> C (sucOrd x)) -> ((f : Nat -> Ord) -> ((x : Nat) -> C (f x)) -> C (limOrd f)) -> (z : Ord) -> C z ordrec C d e g zeroOrd = d ordrec C d e g (sucOrd a) = e a (ordrec C d e g a) ordrec C d e g (limOrd f) = g f (\x -> ordrec C d e g (f x))
The typings of these constants are called elimination rules in Martin-Löf type theory and the defining equations are called equality rules.
We can also define sets by structural recursion. Here is a definition of the function which translates an element in Bool to the corresponding Set:
isTrue : Bool -> Set isTrue true = True isTrue false = False
We can even define large versions of the elimination constants above. For example,
if1 : (C : Bool -> Set1) -> C true -> C false -> (z : Bool) -> C z if1 C d e true = d if1 C d e false = e
Agda's pattern matching goes beyond the usual notion of structural recursion in one argument.
We can for example define a function by pattern matching on two arguments _==_ : Nat -> Nat -> Bool zero == zero = true zero == suc n = false suc m == zero = false suc m == suc n = m == n
Recursive calls can more generally be on structurally smaller arguments:
half : Nat -> Nat half zero = zero half (suc zero) = zero half (suc (suc n)) = suc (half n)
Agda allows quite a general class of definition of recursive functions by pattern matching. Both a termination checker (which checks size-change termination in the sense Jones et al) and a coverage checker are provided, but we postpone the description of these until later - see Totality.
Agda also allows the definition of large inductive types, such as
data Large : Set1 where El : Set -> Large Arrow : Large -> Large -> Large
Since one of the constructors of Large ranges over the type Set, Large cannot be a member of Set but has to belong to the next universe Set1.
In general, to define a data type in Set(i+1) all constructor types must be in Seti.