Maths - Types

ref nlab

We can look at types from a mathematical or a computing point of view.

Types in Computing

In computing we think of type as representing some type of data structure, this determines:

See these pages for types as related to programming:

Types in Mathematics

Types were originally added to set theory to try to resolve some paradoxes that arose. types and sets

Another way to look at it:

A type is the range of significance of a variable, that is, the concept of a vaiable is tied up with the concept of a type.

Type Theorys

Here are some atomic mathematical types with some examples of terms that may inhabit those types:

Type Term  
Boolean True
False
 
Natural Numbers 0,1,2...  
Real Numbers 0.582  
Set a  

Type is a collection of terms having some common property.

Terms are values (or variables, or functions like the sum of other terms).

We can think of types as classifying values. If we know the type of something we have less information than knowing its value (and also its type). If we know a value without knowing its type, for example 0 (zero) we don't know if it is a natural number, or an integer, or a real number. Hence we don't know what operations might be valid to apply to it.

Types and terms are a similar (but different) concept to sets and elements. In both cases we think about it as a container relationship.

The ':' colon symbol is used to declare the type of a given term:

Type Term  
M x:M typing declaration

If the type is not declared, it can be inferred in some circumstances.

We can have a multiple level hierarchy of types. For instance, the type 'M' in the above table may itself have a type of 'Type' ( M:Type ). However giving all higher order types the type of 'Type' could theoretically lead to circular references and hence paradoxes. Some theories allow these 'Type's to be numbered to enforce a hierarchy of universes and prevent any circular references. (see kinds)

Set Theory and Type Theory

Both types and sets can also be thought of as a collection of elements.

In type theory the elements (terms) are defined only for a given type and don't exist outside it. So, for example, the same element can't be a element of two different types.

Elements of a type can optionally be types themselves but, as with sets, a type must not contain itself. That is, it must be a strict hierarchy (no loops). See type universes.

Category Theory and Type Theory

We can relate type theory to category theory by linking:

So if a category has various objects each of these could be related to a type. type to category

More about linking category theory and type theory on this page.

Martin-Löf Type Theorys

These are 'constructive' type theories also known as Intuitionistic type theories, that is, we can start with some atomic types as above and define compound types by building them up inductively.

There are a number of type theorys developed by Church, Martin-Löf, etc. Such as:

Constructs

Constructors and Eliminators

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

Type Name Type Constructor Constructor Eliminator  

for more details click on link below

formation constructors deconstructors notes
0
 
0:type
 
e:0   A:type
absurd(e) : A

empty
cannot be constructed
initial object

1
 
1:type
 
*:1
 

unit
cannot be deconstructed
terninal object

Bool   True
False
conditional expression
if then else
 
inductive datatypes     induction principle  
Nat   Z
S n

elim_Nat: (P : Nat -> Set) -> P Z ->
((k : Nat) -> P k -> P (S k)) ->
(n : Nat) -> P n

where:

  • P n = property of number n
  • Z = zero
  • S n = successor to n

elim_Nat P pz ps Z = pz
elim_Nat P pz ps (S k) = ps k (elim_Nat P pz ps k)

 
List   cons car
cdr
 
Pair Pair (a,b) fst
snd
 
Function   λ function application  
Expression Atom      
Equality (≡) : t->t->Type refl : { A : Typei } → ( x : A ) → x ≡ x

J : { A :Typei } →
(P: (x y :A) → x ≡ y → Typej ) →
(for allx . P x x ( refl x )) →
for all{ x y } . ( eq : x ≡ y ) →P x y eq

 
+       sum
Record   tuple projection  
×       product - special case
of dependant product
Π       dependant product
space of sections
Σ       dependant sum
         

For eliminator, for inductive types we can use a recursor.

Syntax

History: start with type theories with special types for natural numbers and truth values.

(see Lambek&Scott p129)

If A and B are valid types then we can define:

  One Element Type Natural Numbers Container for elements of type A Product Truth Value  
type notation 1 N PA A×B Ω  
term (for type with intuitionistic predicate calculus) * 0,Sn {a∈A | φ(a)} <a,b> T,_|_, ...  
term (for type based on equality) * 0,Sn {a∈A | φ(a)} <a,b>

a∈α

a = a'

 

where:

Product and Sum Types

Product and sum types construct a type from 2 (or more) types (A and B).

Product Type

Has one constructor (formation) and multiple ways of deconstructing (elimination) (projections).

 

product type

Sum Type

Has multiple constructors but only one way to use it.

sum type

In type theory types are defined in terms of:

  • Type formation
  • Term introduction
  • Term Elimination

This picture shows how programming language constructs (In this case: Idris) relate to this theory:

product type as pair

Sum, Product and Exponent

A type theory with Sum, Product and Exponent type is related to a Cartesian Closed Category (CCC).

A term may be represented by some variable such as x,y... or a compound term using the following:

If 'M' and 'N' are valid terms, then the following are also valid terms:

  Type Term  
    M[x] We will use this notation to denote a term 'M' with multiple values depending on the value 'x'.
Sum A \/ B <M,N>

This is a union of the two types. An instance will contain an instance of only one of the types.

Product A /\ B (M N)

This contains both of the types (like tuples) . An instance will contain an instance of all of the types.

We can recover the contained types as follows:

  • M = π1(M N)
  • N = π2(M N)
Exponent A->B λ x:M.N

This is a function from M to N.

where x is an instance of 'M' and the function returns an instance of 'N'

See lambda calculus.

Where:

Here are some more atomic types, this time denoted in a more category theory way:

Type Term  
0 &bottom; empty type (initial)
1 &top; unit type (terminal)
2 True
False
boolean

Semantics

To put this in a slightly more formal setting see semantics page.

Dependent Types

see this page

Recursive and Co-recursive Types

see this page

Type Theory and Logic

There are various approaches to this:

Curry-Howard

There is a correspondence between constructive (intuitionistic) logic and propositional logic.

Constructive Logic Type Theory  
proposition type of its proofs A proposition is true iff we have a proof of that proposition
proof an object of that type  
     
     

This does not work for more complicated type theorys and logics such as higher order logic.

Logic over a Type Theory

We treat logic as a meta-mathematics, that is a layer above the mathematics that allows us to apply axioms and rules to prove things about the mathematics.

Type Theory and Information

Informally we sometimes think about 'information' when discussing types. for instance, does some particular operation loose or gain information. The concept of information was precisely defined by Claude Shannon in 1948. It is linked to the concept of 'entropy' which quantifies the amount of uncertainty involved. However something involving probabilities doesn't seem to be what's required here.

So if we are trying to get an intuitive understanding of why the types/sets on the right are not isomorphic we need to see that the function shown can't be reversed. Intuitively we can see that this function 'looses information'. How can we make this more precise? non isomorpic

More specifically, in type theory we have the 'computation rule' (beta reduction rule) and the 'Local completeness rule' (eta reduction rule) - see page here. We say that the 'beta reduction rule' ensures that information is not gained and the 'eta reduction rule' ensures that information is not lost.

One way to think about this is as a constructor as a producer of information (particle of information) and as an evaluator as a consumer (anti-information) which collide and annihilate in computation and local completeness rules.

Comprehension

Any collection of elements of the same type may form an object of the next higher type.

there existsz'for allx[x∈z <-> Φ(x)]

Concepts related to Type

 

type theory

 

β Reduction

In type theory, β-reduction is a process of 'computation', which generally replaces more complicated terms with simpler ones.

Example of Cut elimination / substitution

In its most general form, β-reduction consists of rules which specify, for any given type T, if we apply an “eliminator” for T to the result of a “constructor” for T, how to “evaluate” the result. (n-Lab)

(λx.M) N
M[N/x]
Function evaluation is called β-reduction. This is done by substitution.

Frank Pfenning - Proof Theory Foundations, Lecture 2

Here we show deconstruct followed by construct for Product, Sum and Exponent types: beta reduction

η Reduction

In type theory, η-conversion is a process of 'computation' which is 'dual' to β-conversion.

Whereas β-reduction tells us how to simplify a term that involves an eliminator applied to a constructor, η-reduction tells us how to simplify a term that involves a constructor applied to an eliminator.

In contrast to β-reduction, whose “directionality” is universally agreed upon, the directionality of η-conversion is not always the same. Sometimes one may talk about η-reduction, which (usually) simplifies a constructor–eliminator pair by removing it, but we may also talk about η-expansion, which (usually) makes a term more complicated by introducing a constructor–eliminator pair.

η-reduction is ill-defined for the unit type (n-Lab) .

eta reduction

 

Examples from Idris

More examples on this page

Product Type

Here we start with a product type 'M'. We can deconstruct it by using 'fst' and 'snd' then construct it to get back to 'M'
Idris> :let M = MkPair 2 "2"
Idris> MkPair (fst M) (snd M)
(2, "2") : (Integer, String)
Here we start with two terms 'x' and 'y' if we first construct using MkPair then deconstruct we get back to 'x' and 'y'.
Idris> :let x = 3
Idris> :let y = "3"
Idris> fst (MkPair x y)
3 : Integer
Idris> snd (MkPair x y)
"3" : String

Sum Type

We can't constuct terms as easily because its more difficult to infer the type.
Idris> :let M = Either Integer String
Idris> M
Either Integer String : Type
Idris> the M (Left 4)
Left 4 : Either Integer String
Idris> :let m = the M (Left 4)
Idris> m
Left 4 : Either Integer String
'case' as deconstructor
lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
                              Nothing => def
                              Just x => x

Exponent Type

An element of A->B can be represented as λ a.Φ
λ a.Φ : A->B

β-reduction

The second form allows us to change the name of the variable by substitution.

Replaces a bound variable in a function body with a function argument - inlining.

(λ a.Φ) a = Φ
(λ a.Φ) x = [a/x]Φ
η-reduction
f = (λ x . f(x))

We cam implement in Idris like this:

We create anominous lambda like this and apply it like this.

Idris> \x => prim__toStrInt x
\x => prim__toStrInt x : Int -> String
Idris> (\x => prim__toStrInt x) 3
"3" : String

Computations in Idris

A function tends to deconstruct types, rearange and do computations on the terms and then construct the output types.

The deconstruction tends to be done by a 'case' construct in the form of pattern matching on the left hand side. computations in Idris

 


metadata block
see also:
  • For more information about propositional logic see page here
  • Specifically about how constructors and deconstructors relate to introduction and elimination see page here
  • For more information about proofs using Idris see page here
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-2020 Martin John Baker - All rights reserved - privacy policy.