# Theory

Informally, an inductive datatype is a datatype whose elements can be described as being built one step at a time, starting from one or more base cases.

Mathematically speaking, an inductive set is the smallest closed set built from a set of constructors. We shall explain this idea further in this section.

Why study inductive types? Inductive datatypes are every where in computing and programming. Many data structure like numbers, lists, trees and, programs and even mathematical proofs are examples inductive datatypes. Therefore it is necessary to understand how to construct them and program with them.

## Natural Numbers as inductive types

We are used to thinking about natural numbers using numerals such as 0, 1, 2, ..., etc. But there is another way of thinking of natural numbers in which natural numbers are built one at a time, step by step.

Mathematically, the set N of natural numbers is the smallest set of values satisfying the conditions

Z() belongs to N

if ( n belongsto N) then s(n) belongs to N

An equivalent short hand for the above is the set of the following rules:

--------- ZERO

z() : N

n : N

-------- SUCC

s(z) : N

Here, we have two rules, called ZERO and SUCC (for successor). Each rule consists of two parts divided by a horizontal line, which may be read as an "if-then". The part(s) above the line is called hypothesis or antecedent; the part below the line is called the consequent or conclusion. The colon denotes membership in the set N. Z and s are constructors. You may think of constructors as functions. In the above case, Z takes nothing and returns an element of N. s takes an element of N and returns another element of N.

Depending on our choice of Z and s, different different representations of N are possible. The constraints on the constructors are the following:

Each constructor is injective.

Each constructor is distinct from the other.

The above two constraints guarantee that every element of the inductive type is uniquely constructed using the constructors. From this we may then conclude that if n is an element of N, then exactly one of the following is true:

n = z()

n = s(m) for a unique m.

In the particular case of N, the m above is called the predecessor of n.

## Summary

Inductive types are built using constructors. Every element of an inductive set is uniquely constructible using the constructors, which are injective and mutually distinct. An inductive type may have several different representations