A common language for dependently-typed programming?

The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types.

1. Epigram
2. ATS (successor to Dependent ML and Xanadu)
3. Agda (successor to Cayenne)
4. Ωmega
5. NuPrl
6. Twelf
7. Isabelle
8. Coq
9. Delphin
10. Concoqtion
11. Aldor
12. Guru (successor to RSP1)

And now, a list of caveats about the above list:

• Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq.
• This list does not include several languages that are new or new variants (PIE, Matita), not checked at compile-time (Sage), or not actively maintained (most proof assistants, Charity).
• Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Aldor can't understand most type equalities, making its dependent types somewhat weak, though Atypical and Aldor-- aimed to remedy this five years ago. Agda and Epigram have New Exciting Versions 2 coming out, so they suffer from the Osborne Effect.

Is it time yet to do anything about the cornucopia of options? When Haskell began, there were many similar options; the list above is heterogeneous. Is that because it's too early in to tell what the Right choices will be? Is this problem fundamentally harder than the one that inspired the Haskell precursors?

I'm not sure, though deciding how to ensure termination seems particularly tricky. Nonetheless, there are other decisions that aren't as directly related to the central dependent type issues, like syntax, functional purity (though this is related to termination), and editing environment. Maybe these issues will divide the ecosystem into a few niches, each dominated by one player. In the meantime, it's tough to choose.

Conor's Rule?

Edwin Brady writes in "How to write programs in two easy steps", that

I think it's also an area where dependently typed languages like Epigram will shine, because it will one day be possible to write verified interpreters for domain specific languages …

I immediately thought "I can write dependently typed programs right now with GADTs, and I can do so in GHC Haskell, Scala, or the upcoming C#". This is, of course, only mostly true, since none of these does termination checking, and the syntax is awkward.

The same blog post later references Greenspun's Tenth Rule:

Any sufficiently complicated C or Fortran program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp

and I thought that my programs follow a similar pattern with dependent types: I'm always simulating them informally. Based on Section 6.1: "The Trouble with Faking It" in Conor McBride's Faking It (Simulating Dependent Types in Haskell) (mirror), I wonder if there's any truth to something we might call

Conor's Rule

Any sufficiently complicated Haskell or ML program contains an ad hoc, informally-specified, bug-ridden, half-completed simulation of dependent types.