Lambda the Ultimate

I'm not sure about ATS in particular, but I think it follows a similar route to DML.

I think Hongwei Xi, the main researcher behind ATS, was also behind DML, but it's my understanding that ATS was created as an alternative to Pure Type Systems, while retaining its dependent typing power. I could be wrong though, hence the request for clarification. :-)

DML only has a restricted form of dependent types, added to a conventional language.

Yes, I'm aware of this. I've seen a vague reference or two to ATS also supporting "restricted dependent types", but it was never clarified in more laymen's terms.

I also feel Ontic is important.

Indeed, I've heard a few rumblings on Ontic here and there, but it doesn't seem like much work is happening in that direction.

Then there are the various proof assistants - Coq, LEGO, etc. I don't have much experience with these.

ATS has support for combining programming with theorem proving, which is why it seems so strange that it's been discussed so little here. It seems very interesting.

I feel the strongest difference is what kind of programs you can write with which expressiveness in specifications.

• For DML it is ML with automatic proving for arithmetic expressions in types. The other allow roughly the same expressiveness in specifications.
• Epigram is powerful just as Coq and LEGO, it is a really dependently typed programming language where proof and algorithmic code are intermingled in an elegant way.
• ATS separates proving and coding a little more and proposes other paradigms than functional programming. The main difference i see between Epigram and ATS is on the objective. The first proposes a new way of programming while the second integrates all paradigms in an unifying one using dependent types and relying explicitely on the manipulation of proof objects.
• In Coq (and probably LEGO), you could write the same programs as in Epigram, except it would generally be a nightmare for a number of practical and theoretical reasons. Epigram is a programming language giving you adapted syntax and constructs to program, and a nice typing and editing system. Here tactics to prove/program are part of the language (rec, <=, case, etc...).
  On the other hand, Coq and LEGO are proof assistants, so their main focus is on proving, not on the easy manipulation of terms. That's kind of where Curry-Howard stops for them, you can write terms with simple types easily, but once you want to give a rich specification to a program you're alone. You can use the tactic language to prove arbitrarily complex goals but it's a bad idea to use them for creating programs.

Thanks for the explanation! It would seem then, that ATS may be more verbose, but still theoretically as powerful as Epigram. The "backwards-compatible" paradigms are certainly interesting though, if only to see how they're typed, and it should yield an idea of how useful they actually are.

I use the term "dependent types" more broadly, to refer to any language with fancy type-level data.

For marketing purposes, it's good to have one term for the high-level functionality that the programmer sees: rich type-level data that can be used to specify and verify properties of programs. And "dependent types" seems like as good and historically relevant a term for this as anything else (anyone have counter-proposals)?

The technical methods of providing this functionality are a second-level concern---though of course it's important for researchers to be able to convey a language design quickly, which requires more detailed terminology (e.g., I've heard "phase-sensitive dependent types" for DML-style, or "full spectrum dependency" for Epigram). However, I think the language design space is more complicated than the syntactic condition you described above: For example, if I presented the syntax of the simply typed lambda-calculus with one syntactic category, and then sorted out the difference between expressions and types in the typing judgement, your definition would deem it dependently typed. Alternatively, what if a language allows _some_ programs to be used in types, but not others (e.g., by making a restricting the types at which dependency is allowed)? Or what if a language that allows run-time computation with "type constructors", a static syntactic category? There are lots of variations on restricted forms of dependent types, but we need one word for the overall concept.

...that what's going on in ATS is not merely a restriction of what (e.g) Coq or Agda does. The dependent quantifiers in ATS have an intersection-style interpretation, rather than a function-style interpretation, which means that they validate Girard's "shocking isomorphisms" (such as (forall a. A + B) iso to (forall a. A) + (forall a.B)).