SimpleInductiveTypes

See the official user manual pages on data types and pattern matching for the most up-to-date version of the information on this page.

This document has been extracted from a literate Agda file, which was tested with Agda 2.3.0

Table of contents

1. Example datatypes
2. General form
   1. Strict positivity
3. Formation and introduction rules
4. Definition by pattern matching
5. Elimination and equality rules
6. Large elimination
7. Beyond elimination rules
8. Large inductive types

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

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

General form

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

Agda checks that A₁, ..., A_n : Set wrt the current signature and context. Moreover, each A_i has the form

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

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

where D must not occur in any C_j.

Strict positivity

The condition that D must not occur in any C_j can be also phrased as D must only occur strictly positively in B_i.

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.

To see how one can write a looping definition using the Bad datatype from above, see BadInHaskell. For more general information on termination see Totality.

Formation and introduction rules

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.

Definition by pattern matching

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.

Elimination and equality rules

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.

Large elimination

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

Beyond elimination rules

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.

Large inductive types

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.