Dependent Types
“Dependent types” is a language for defining type checkers.
“Dependent types” is a programming language.
“Dependent types” is a DSL.
AGDA is a manifestation of a programming language for writing type-checker code. The main feature of AGDA is that it has a syntax for describing type checkers. A secondary feature of AGDA is that it also includes syntax for other kinds of code.
AGDA attempts to ensure that type-checker code is self-consistent.
A postulate in AGDA is a break-out to a lower-level. A type system cannot be fully defined in pure AGDA, and postulates allow one to describe the “boundaries” of a type description. I use the term “foreign” for these kinds of postulated types.
Haskell conflates type definition and data implementation in the same notation (language). Because of this conflation, Haskell appears to be complicated.