Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
The book The Little Typer explains dependent types using a toy language called Pie (https://github.com/the-little-typer/pie).
I'd say that Pie is a much smaller version of the core languages of those systems. It's a bit closer to Lean's core than to Coq, Agda, or Idris, but the differences are not very large there. When I say "core language" what I mean is that these languages typically have a lot of powerful automation features that make it much more convenient to write things in them, but that make it harder to understand what's being automated. They're optimized for doing useful things, rather than for understanding the core of dependent types.
Basically: Pie is intentionally low-tech, because using a low-tech tool can help you learn to understand the domain in which the tool is applicable. Manual work is an opportunity to learn. These other languages are not teaching tools, they're work tools, so they help out a lot more.
I don't know your background, so in this answer I'll use some technical terminology from dependent type theory. If that makes it hard to understand, please feel free to follow up and I'll do what I can to explain.
Pie's concrete syntax uses parentheses and prefix operators like a Lisp, while most of the type theory community uses infix or mixfix operators, even when discussing the simple core language. This was done partly to make it easier to parse Pie, partly for familiarity for readers coming from the other "Little" books, and partly because Dan and I both like it. This is mainly a cosmetic difference.
One other less-cosmetic syntactic difference is that most operators in Pie have fixed arities, while more practical languages typically give things like constructors a function type, allowing them to be partially applied. In this way, Pie is more like earlier paper presentations of dependent types, where each type was introduced independently, and function types weren't used to present non-function operators. In other words, things that might have (dependent) function types in Coq's core might have their typing given by inference rules in Pie.
All of the practical systems feature a predicative hierarchy of universes, while Pie has only a single universe. Additionally, most systems have universe polymorphism of some sort, and some have cumulativity. Neither of those are relevant if there's only one universe. An earlier development version of Pie had a predicative, cumulative hierarchy, but we tested all the code in the book and found that we never used more than one universe, so we got rid of the rest for the sake of simplicity. This means that all of those systems are strictly more expressive than Pie. Having the predicative hierarchy also allows them to get rid of the "is a type" judgment and replace it with an "inhabits a universe" in most contexts.
Also, many systems have dedicated proposition universes with special characteristics. For instance, Agda's and Lean's Props are irrelevant, meaning that any two proofs of the same proposition are definitionally equal (what we call "the same" in TLT), as is Coq's SProp.
Pie comes pre-equipped with a fixed set of inductive types: natural numbers, lists, vectors, sums, products, equality, unit, and empty types. This was enough to encode all the things that we wanted to demonstrate, and we found that an implementation of a full inductive types feature was too complicated to explain (if we had to explain the strict positivity condition, the book would have probably been 50 pages longer, and it was already longer than we had hoped).
In these other systems, you can define your own inductive types. This makes them vastly easier to use for non-trivial mathematical content and for most programs. Lean generates eliminators like Pie's ind-Nat for new inductive types, while Coq, Agda, and Idris have built-in pattern matching and recursion primitives that are checked separately.
Pie has as many eta rules as we could put in (with the exception of Vec, which would have made some normal forms unreadably huge). This was originally done to make it easier to write automated tests for student assignments, because eta rules for Pi and Absurd lead to proof irrelevance for proofs of negations.
The other systems that you're mentioning have varying degrees of eta rules, and usually provide the user with ways to control whether they should be generated, because they provide a tradeoff between type checker performance and programmer convenience.
Most existing dependently typed core languages are quite verbose, which makes it so that programs contain enough information to reconstruct their types from scratch. Pie, however, is formulated using bidirectional type checking. We did this because it provided a good balance between implementation simplicity and convenience for readers, and allowed us to avoid higher-order unification. We had originally hoped to have the complete language implementation in the book, but it just couldn't fit, so avoiding tricky techniques was important to us.
