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).


As an example we might have these 3 constructors:

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:

we need to add:

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.



  dependent type constructor

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.





metadata block
see also:
  • More information about fixpoints on this page.
  • More information about algebra and monad on this page.

Other sites

Correspondence about this page

Book Shop - Further reading.

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.

flag flag flag flag flag flag 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.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2021 Martin John Baker - All rights reserved - privacy policy.