Type Theory
Models of predicative type theory are well-studied and have been mechanized,
ranging from proofs of consistency for a minimal type theory with a predicative hierarchy
in 1000 lines of Rocq
to proofs all the way up to decidability of conversion
in 10 000 lines of Agda.
In contrast, the story for impredicative type theory is not so clear.
Incorporating different features alongside an impredicative Prop
may require substantially different proof methods.
This post catalogues these various models, what type theories they model,
and what proof technique is used.
Most proofs fall into one of three techniques:
proof-irrelevant set-theoretic models,
reducibility methods,
and realizabililty semantics.
Overview
| Work |
Theory |
Proof method |
Universes |
Inductives |
Equality |
| Coquand (1985) |
CC |
? |
Prop, Type |
none |
untyped |
| Pottinger (1987) |
CC |
? |
Prop, Type |
none |
untyped |
| Ehrhard (1988) |
CC |
ω-Set |
Prop, Type |
none |
none |
| Coquand and Gallier (1990) |
CC |
reducibility |
Prop, Type |
none |
untyped |
| Luo (1990) |
ECC |
reducibility; ω-Set |
Prop ⊆ Type{i} |
dependent pairs |
untyped |
| Terlouw (1993) |
CC |
reducibility |
Prop, Type |
none |
untyped |
| Altenkirch (1993) |
CC |
Λ-Set |
Prop, (Type) |
impredicative |
typed |
| Goguen (1994) |
UTT |
set-theoretic |
Prop, Type |
predicative |
typed |
| Geuvers (1995) |
CC |
reducibility |
Prop, Type |
none |
untyped |
| Melliès and Werner (1998) |
PTS |
Λ-Set |
Prop ⊈ Type{i} |
none |
untyped |
| Miquel (2001) |
CCω |
set-theoretic; ω-Set |
Prop ⊆ Type{i} |
none |
untyped |
| Miquel (2001) |
ICC |
? |
Prop ⊆ Type{i} |
none |
untyped |
| Miquel and Werner (2003) |
CC |
set-theoretic |
Prop, Type |
none |
untyped |
| Lee and Werner (2011) |
pCIC |
set-theoretic |
Prop ⊆ Type{i} |
predicative |
typed |
| Sacchini (2011) |
CIC^- |
Λ-Set |
Prop, Type{i} |
predicative, sized |
untyped |
| Barras (2012) |
CCω |
set-theoretic |
Prop ⊆ Type{i} |
naturals |
untyped |
| Barras (2012) |
CC |
Λ-Set |
Prop, Type |
naturals |
untyped |
| Timany and Sozeau (2018) |
pCuIC |
set-theoretic |
Prop ⊆ Type{i} |
predicative |
typed |
More …
…probably. To be clear, ECIC refers to Monnier and Bos’
Erasable CIC, with erasable in the sense of erasable pure type systems (EPTS).
I’ll argue that even with erased impredicative fields,
Coquand’s paradox of trees is still typeable.
More …
I’ve wanted to write an informal (but technical!) post about my current research in progress on Stratified Type Theory (StraTT), but we’ve been occupied with writing up a paper draft for submission to CPP 2024, then writing a talk for NJPLS Nov 2023, then being rejected from CPP, then I’ve just been randomly distracted for two weeks but I’m so back now.
That paper draft along with the supplementary material will have all the details, but I’ve decided that what I want to focus on in this post is all the other variations on the system we’ve tried that are either inconsistent or less expressive. This means I won’t cover a lot of motivation or examples (still a work in progress), or mention any metatheory unless where relevant; those can be found in the paper. Admittedly, these are mostly notes for myself, and I go at a pace that sort of assumes enough familiarity with the system to be able to verify well-typedness mentally, but this might be interesting to someone else too.
More …
Overview
| Work |
Summary |
| Nakano |
STLC + recursive types + guarded types |
| Birkdeal, Møgelberg, Schwinghammer, Stovring |
dependent types + recursive types + guarded types |
| Atkey and McBride |
STLC + recursive types + guarded types + clocks |
| Birkedal and Møgelberg |
dependent types + guarded types |
| Møgelberg |
dependent types + guarded types + clocks |
| GDTT |
dependent types + guarded types + clocks + delayed substitution |
| CloTT |
dependent types + guarded types + ticks + clocks |
| GCTT |
cubical type theory + guarded types + delayed substitution |
| TCTT |
cubical type theory + guarded types + ticks |
| CCTT |
cubical type theory + guarded types + ticks + clocks |
More …
More …
More …
While it’s rather difficult to accidentally prove an inconsistency in a well-meaning type theory that isn’t obviously inconsistent
(have you ever unintentionally proven that a type corresponding to an ordinal is strictly larger than itself? I didn’t think so),
it feels like it’s comparatively easy to add rather innocent features to your type theory that will suddenly make it inconsistent.
And there are so many of them!
And sometimes it’s the interaction among the features rather than the features themselves that produce inconsistencies.
More …
This post is inspired by this thread
from the Agda mailing list.
Because Agda treats Size like a first-class type,
there’s quite a bit of freedom in how you get to use it.
This makes it a bit unclear where you should start:
should Size be a parameter or an index in your type?
What sizes should the constructors’ recursive arguments’ and return types have?
Here are two options that are usually used (and one that doesn’t work.)
The recommended one is using inflationary sized types and Size<.
More …
Sized types hold great potential as a very practically useful way to do type-based termination checking,
but sufficiently expressive sized types in dependent type theory come with a host of problems,
mostly related to its incompatibility with the infinite size found in most simpler or nondependent type systems.
This post attempts to describe some potential but ultimately unsatisfying solutions.
More …
More …
Back during the summer of 2019, I worked a bit on the Coq kernel. At the same time, I posted a lot of toots on Mastodon about whatever random problems I was encountering. I’ve decided to collect them here, as it might just be that some of these will be useful to me again at some point.
More …
