I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles on dependent typing.
Many type theory discussions seem to focus on adding incremental features to previous type systems, not "what's the next large generalization up from type system X?". Dependent types seem to be the next large generalization from System F, but I have yet to find the intuitive, canonical dependently typed language. The many references to Calculus of (inductive) Constructions makes me think CoC is that language, but the explanations of the language I have seen don't seem very clear or intuitive to me.
I am expecting/guessing such a language would have features like: (and please let me know if anything in particular jumps out as confused or unrealistic)
- Generalized abstraction (can have functions from any domain in the type hierarchy to other, kind -> term, term->type''' etc.)
- Has an infinite hierarchy of typing (terms : types : types' : types'' : ...)
- A minimum number of basic elements. I am imagining that the language only asserts a single element for each level. For example it might assert that (() : Unit : Type : Type' : ...). Other elements are built from these elements.
- Sum and product types are derivable.
I am also looking for an explanation of that language which ideally would discuss:
- The relationship between abstraction and quantification in that language. If they are not unified, then explain why they are not unified.
- The infinite type hierarchy explicitly
I am asking this question because I want to learn dependent type theory but also because I want to put together a guide that, assuming a little CS background, teaches the use of and how to understand proof assistants and dependently typed languages.