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.
- ATS (successor to Dependent ML and Xanadu)
- Agda (successor to Cayenne)
- Guru (successor to RSP1)
- 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.
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.