Maths - Types

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

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)

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:

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 destructuing (elimination) (projections).

 

product type

Sum Type

Has multiple constructors but only one way to use it.

sum type

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.

We can recover the contained types as follows:

  • π1(M)
  • π2(M)
Product A /\ B (M N) This contains both of the types (like tuples) . An instance will contain an instance of all of the types.
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

Dependent Types

There are two dependent types:

  • dependent product types (Π)
  • dependent sum types (Σ)
construct dependent types

(above diagram adapted from diagram in Thorsten Altenkirch paper)

Each of these can be related to non-dependent types in two ways (blue and red lines in diagram above).

As indexed types:
Here we extend the binary product type to a product of multiple terms. In order to select a particular projection it is helpful to consider these types as indexed so the projections can be represented as a function from a term to a type: i -> Bi. indexed dependent product type
Similarly the binary sum type can be extended to a sum of multiple terms. In order to use the type it is helpful to have an index to know what it is so the type can be represented as a product of a term and a type: i×Bi. indexed dependent sum type

Families of types:

(Π x : A) B(x)   f where f(x)=b
(Σ x : A) B(x)   (a,b)
A + B   i(a),j(b)

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

  Type Term  
Dependent Product x:A->B Πx:M.N[x]

 

Dependent Sum <x:A,B[x]> Σx:M.N[x] Strong sum type: expresses the concept of subset.

Dependent Product Types (Π)

I find it helps to visulise as a fibre bundle:

We have a type A with terms a1, a2,a3 ... an

For each of these terms we have a type Bn

This gives a family of types, we can either think of this as being indexed by 'A' .

dependant type
dependant square  

Dependent Sum Types (Σ)

In the same way that dependent product types are functions with a type and a term dependent sum types are products with a type and a term.

dependant sum type

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

Type Notation Element Dependant Functions over Type

product type

(cartesian product)

A×B (a,b):(A×B)
f: Π ((pr1(x),pr2(x)) =A×B x
x:A×B

coproduct type

(sum)

A+B

a:(A+B)

b:(A+B)

f: Σ B(x) given a:A and b:B(a)
x:A

type of second component of pair depends on value of first component

exponent type

BA

(or AB)

λ b. a: BA  

Dependent Types in Programming

In the language 'Scala' we can define a type that is parameterised by another type (polymorphism) for instance:
List[T]

This represents a list of any type, represented by 'T', for example a list of Integers or a list of boolean values.

However, Scala does not allow dependent products like say: Modulo[n:Integer] which would represent any modulo number system such as modulo 3 or modulo 27.

Dependent Types as Fibre Bundles.

The situation where a type depends on the value of another type is modeled by fibre bundles.

We discuss fibre bundles on the page here.

So a model of a vector category depends on its dimension:

dependent type

Semantics

We can start with some of the simpler ways of creating compound types.

Formation, Introduction, Elimination and Computation rules

Formation rules

 

Introduction rules

 

Elimination rules

 

Computation rules

 

 

 

 

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.

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

 

 


metadata block
see also:
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-2018 Martin John Baker - All rights reserved - privacy policy.