Confusion about dependent types

Stream: new members

[Nicolò Cavalleri]

I was recently rereading Theorem proving in Lean to clear some doubts I had and, as it often happens, I realized I have a confusion regarding dependent types.

In the section on dependent types, list is quoted as an example of dependent type and similarly I'd guess the product of two types to be a dependent type. However, lists and product are there also in Isabelle and indeed in Isabelle, through type constructors, you can have types depending on other types. After a discussion on the Isabelle's Zulip, my guess is that what distinguishes dependent type theory from simple type theory is that in dependent type theory types can depend on terms. Things such as Pi types and Sigma types, that are not present in Isabele, ask for an term of type α → Type* which is a term that is not a type. Is this correct? If yes I wonder why this remark is not there in the book, since it seems quite central! Also, in case yes, is still correct to say that list and product are dependent types? If yes one could argue that simple type theory also has dependent types...

[Josh Chen]

I assume you're referring to the discussion in Section 2.8 about polymorphic lists.
Polymorphism can be implemented with dependent types if you have a universe $U$, or Type, or whatever you like to call it, but it's also possible without full blown dependent types, which is what Isabelle, Haskell etc. do.
Pure type systems describe general theories of dependencies one may add on top of basic STLC, and MLTT-style dependent type theory is just one instance of such a system.

[Horatiu Cheval]

See also the lamba cube: https://en.m.wikipedia.org/wiki/Lambda_cube for a classification of type systems based on what is allowed to depend on what.

[Scott Morrison]

A big distinction is whether you are only allowed to depend on other types, or if you can also depend on terms of types. The first is enough for list, but you need the second e.g. for vector.