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