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