Things only really clicked for me when I read Type Theory and Functional Programming cs.kent.ac.uk/people/staff/s It has modest background requirements and clear writing
Conversation
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
2
3
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
Sorry - bit of a digression on the main point - just something I've been slightly annoyed by having to decide between as somebody trying to implement some of this stuff. 🤔
Got similar vibes from this post: edsko.net/2017/01/08/lin - maybe it got me thinking about it, I can't remember though.
1