# Maths - Constructors and Eliminators

On this page we discuss constructors and eliminators for various types and relate this to introduction and elimination in propositional logic. We can then go on to relate programs to proofs.

The constructors and eliminators of a type, along with the other constructs here, uniquely specify the type. This corresponds to a 'universal property' in category theory. (the mappings into and out of an object uniquely determine it up to isomorphism - see Yoneda lemma).

#### Sum Type

On the page about propositional logic here we had the introduction and elimination rules for 'or' :

Introduction Elimination
 A A\/B
(\/I1)
 B A\/B
(\/I2)
 A\/B [A] ... C [B] ... C
C
(\/E)

So the introduction rules show,

• If we have a proof of A we have a proof of A \/ B
• If we have a proof of B we have a proof of A \/ B

However we can't go in the reverse direction, for instance, if we have a proof of A \/ B we can't get to a proof of A. A proof of A \/ B does give us some information that is if:

• We have a proof of A \/ B
• A implies C
• B implies C

Then we have a proof of C.

When we translate from propositional logic to type theory we get the corresponding example of a constructors and eliminator for a sum type (Taken from Idris prelude here):

Constructor Eliminator
```data Either : (a, b : Type) -> Type where
||| One possibility of the sum
||| conventionally used to
||| represent errors
Left : (l : a) -> Either a b
||| The other possibility,
||| conventionally used to
||| represent success
Right : (r : b) -> Either a b```
```||| Simply-typed eliminator for Either
||| @ f the action to take on Left
||| @ g the action to take on Right
||| @ e the sum to analyze
either : (f : Lazy (a -> c)) ->
(g : Lazy (b -> c)) ->
(e : Either a b) -> c
either l r (Left x)  = (Force l) x
either l r (Right x) = (Force r) x```

So, like with the introduction rules, the constructors are easy:

• Left to create from type a
• Right to create from type b

As with the elimination rule, the eliminator is more complicated.

If we have a function (a -> c) and a function (b -> c) then we can generate a function: Either a b -> c

 Rather than use the 'either' function above, it might be easier to use a 'case' construct: ```case x:(Either A B) of a => c b => c```

### W-Type (Inductively Defined Types)

Computer languages such as Haskell and Idris define types as inductively defined types. In mathematics these are W-Types and they have some nice properties.

Examples of W-Types are Nat and trees. They are free initial types.

#### W-Type Constructors

An inductively defined type (W-Type) has one or more constructors of the form:

F(T) -> T

where:

• T is the type being defined
• F(T) is some function of T which may contain T. Hence the induction/recursion.

F(T) may contain some combination of T and other types with sum, product and function types. However in function types T can only be in the codomain, not the domain (it must be covariant)

#### W-Type Deconsructors/Eliminators

Eliminators can be derived from the constructors.

 For each constructor of the form: F(T) -> T There is an deconsructor/eliminator of the form: Where:

• T is an element of the type we are defining
• F is a free function of that type
• P is a property of the type (a mapping out of the type)

#### Example Natural Numbers

An example is the natural numbers

 There are two constructors: Z -> N S N -> N Which gives rise to two deconstructors: Z -> P (S N -> P) -> (N -> P)

So the deconstructor is induction. When programming we tend to do this in reverse (recursion rather than induction).

#### Example Product Type

 The product type requires both types in the constructor so, by the rule given above, there is only one deconstructor containing both types. However, these two types are orthogonal so we can have separate deconstructors with each projection. (how could we prove this?) ```||| The non-dependent pair type, also known as conjunction. ||| @A the type of the left elements in the pair ||| @B the type of the right elements in the pair data Pair : (A : Type) -> (B : Type) -> Type where ||| A pair of elements ||| @a the left element of the pair ||| @b the right element of the pair MkPair : {A, B : Type} -> (1 a : A) -> (1 b : B) -> Pair A B```

### Function Types

 In type theory a function type can be constructed from(deconstructed to) an expression. More about lambda functions on page here.

### More Exanples

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.