3 ms·
Interestingly, even thought type-in-type is inconsistent, there are no normal terms of the “empty” type. So, if you restrict to normal terms you do not get full
by gylterud 3y ago
Interestingly, even thought type-in-type is inconsistent, there are no normal terms of the “empty” type. So, if you restrict to normal terms you do not get full explosion. There are however types A such that both A and not A have normal terms. It is just that if you combine them with modus ponens the term diverges.
Another cool thing is that type-in-type is inconsistent, but has models. In particular, Palmgren constructed a model, based on domain theory, of Martin-Löf type theory with type-in-type.
- skulk 3y agoIn this context, what do you mean by "normal terms"?
- gylterud 3y agoType theories usually come with a reduction relation on terms. It computes things like β-reduction for function, inserting arguments into function bodies, computes projections out of tuples, etc A normal term is one where no further reductions can be made. Without type-in-type you can prove that all terms can be reduced to a normal form. With type-in-type some terms normalise while other diverges. In fact, using type-in-type you can define the fixed point operator and do general recursion!
- xavxav 3y agowow that's really cool, I wonder what the essential difference is between type-in-type and other classic "nice" inconsistencies in type theories. It seems like it's "almost" consistent.