Hmm, I may have spent too much time with Agda lately, as I read "type theory" as "Type Theory". This recommendation is specifically for Type Theory in the Martin-Löf sense
Conversation
Except that apparently Coq counts as type theory, so it's not Type Theory. But I'm happy to label "Coq is not Type Theory" as European nonsense that Americans have no time for :-)
1
The difference between "type theory" and "Type Theory" is part of the thing about type theory that I'd like to be able to teach. There are many such distinctions people care so much about that I just don't understand at all.
1
3
Martin-Löf Type Theory:
- less documented than ideal
- predicative
- typed conversion
- no Prop/Type distinction (irrelevance modalities allowed)
Calculus of (Inductive) Constructions:
- well-documented by French papers
- impredicative
- untyped conversion
- erasable Prop.
2
4
Exactly. Why are *those* the interesting aspects? I know they are, I know people care about them... but frankly, I don't understand them enough to care, and don't know of intro material that compares/contrasts
1
Not sure either, but:
1. Do you care about eta? Even for records? Eta's more insidious than you'd think, unless you use type-directed conversion and eta-expansion (possibly w/ NbE). cs.le.ac.uk/people/ng13/et by seems relevant (updated links in personal.cis.strath.ac.uk/neil.ghani/pub).
2
2
2. How do you justify TT? Predicative TT can be arguably justified with meaning explanations — a "pre-mathematical" version of realizability semantics/logical relations. Impredicative TT requires impredicativity in the metatheory, which is fine in ZFC but more suspect.
1
1
3. In Coq, since Prop is a different universe, for many constructs you have a copy in Prop and one in Type (e.g. conjunction vs product). To avoid that, make irrelevance into a modality! But I never got Agda's multitude of irrelevance modalities and their soundness bugs.
2
2
There's this weird thing how you can use universes (like Coq's `A : Prop`), modalities (like in `[0] A` Granule), or binder annotations (like in Quantitative Type Theory, eg. `(0 x : A) -> B a`) for the same sorts of thing. Kind of frustrating how they are all incompatible?
2
1
3
The already linked twitter.com/Blaisorblade/s is about part of that frustration — for a universe with hardcoded irrelevance you can get some special rules easily, can you get those special cases clearly with an irrelevance modality?
Quote Tweet
Can you connect System F existentials and their universe levels to some form of irrelevance? Formally?
Intuitively, System F existentials are proof-irrelevant/erased Sigma-types, and that explains why they live in Set0, but can you make that formal?
#typetheory
Show this thread
1
2
Ahhh, I missed that, thanks for linking! Yeah the special cases are something I'm not really experienced with, having not used Coq heavily and experienced their utility first-hand.
OTOH, you probably know of existentials in System F, and those are already subtle ;-)
1