# Maths - Inductively Defined Types

An inductive definition of a type is given by a list of constructors. Each of these constructors has a signature like the following examples:

 name : T no parameters defines a single term (element) of the type name: Nat -> T defines a term for every term of Nat name: Nat -> Nat -> T defines a term for every pair of Nats name: T -> T defines a potentially infinite sequence of terms name: T -> T -> T defines a potentially infinitely deep tree of terms name: (Nat -> T) -> Nat -> T covariant terms like (Nat -> T) can appear as parameters but not contravariant terms like (T -> Nat).

So:

• The type being defined can appear as an input to a constructor but only strictly positively (covariant not contravariant).
• If we want an infinite number of constructors we use a term like Nat -> (T -> T).
• If we want an infinite number of parameters we use a term like (Nat -> T) -> T.

As an example we might have these 3 constructors:

• (A -> T) -> T
• (B -> C -> T) -> T
• D -> T -> T

These can be combined into a single constructor:

c : (A -> T) -> (B -> C -> T) -> D -> T -> T

### Recursion Principle

This is the eliminator for non-dependant types.

In order to construct a property P (which is a type, such as an equation) from our type T. That is a function f of type:

f : T -> P:Type

it suffices to consider the case where the input t:T arises from one of the constructors, allowing ourselves to recursivly call f on the inputs to that constructor.

So for the example given above:

• (A -> T) -> T
• (B -> C -> T) -> T
• D -> T -> T
• A -> P
• B -> C -> P
• D -> T -> P

Bringing this together we would require P to be equipped with a function of type:

d : (A -> T) -> (A -> P) -> (B -> C -> T) -> (B -> C -> P) -> D -> T -> P -> P.

### Constructors for Higher Types

For dependent types we can now have multiple levels of constructors.

• The ordinary constructors we have discussed so far, known as point constructors.
• Higher level constructors, known as path constructors. ### Idris Code Examples

 An example of a 'point' constructor is Nat. So we are just constructing a simple type so the constructors have this form: Z -> Nat S Nat -> Nat which are of type: F(T) -> T where 'T' is a type being constructed ```||| Natural numbers: unbounded, unsigned ||| integers which can be pattern matched. data Nat = ||| Zero Z | ||| Successor S Nat``` Idris code
 Whereas to construct a 'path' type we have constructors of the form: F(a->T) -> (a->T) where 'T' is a type and 'a' is a term of some type. Here we are constructing the path: a->T ```|| Vectors: Generic lists with explicit length in the type ||| @ len the length of the list ||| @ elem the type of elements data Vect : (len : Nat) -> (elem : Type) -> Type where ||| Empty vector Nil : Vect Z elem ||| A non-empty vector of length `S len`, consisting of ||| a head element and the rest of the list, of length `len`. (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem``` Idris code

For example to construct a vector, such as [1,2,3], we first have to construct a type of vectors of size 3 then we can construct an element of this type. Some programs will do the higher construct automatically without the need for an explicit command.

### Induction Principle

This is the eliminator for dependant types.

Other sites

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.      Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.