Maths - Universes

A type can have terms which are themselves types. We call these higher order types (types of types) 'universes' or 'kinds'.

The 'type of all types' leads to paradoxes, a 'type of all types' would contain itself and therefore cause a infinite loop.

So we need to have a hierarchy of universes to avoid an infinite loop. So each layer in the hierarchy may only have part of the picture as it may be defined by the layer above it. This is open ended, potentially infinite number of universes.

There are different type theories depending on how we organise these universes of types.

Theory Logically Consistent Turing Complete
Predictive type theories Martin-Löf No
because every type is inhabited.
Impredicative type theories Girard, Reynolds, Coquand Yes No

If we want a program to work as both a 'computer algebra system' CAS and a 'proof assistant' then we have a problem because we want both logical consistency and Turing completeness. So we need some way to try to get both.

Example Idris programming language

Idris has a 'termination checker' which makes sure that only terminating functions are evaluated by the type checker, this puts the programmer in the loop by allowing hints to be put in the code about whether a given function is 'total'.

Another way round this problem might be to abandon the strong form of the (Curry-Howard) 'propositions as types' principle and only allow some types to represent propositions.

Modification to Propositions-as-types

'Mere' propositions allow us to use classical logic (to use the law of excluded middle) when appropriate (for set-like structures) while still allowing the advantages of propositions-as-types such as constructive mathematics.

'Mere' propositions correspond to the 'unit' type, in homotopy this collapses to a point.

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-2023 Martin John Baker - All rights reserved - privacy policy.