Dependently typed language best suited to “real world” programming? [closed]

Question

Which dependently typed programming languages could be used for real world application development?

These are some points, that I think are important:

• documentation
• example programs
• a standard library
• or at least an easy to use foreign function interface
• a community of people using the language for real world tasks
• tool support

Answer 1

I would suggest Agda, because it has calling compatibility with Haskell. As such, it's probably the dependently typed language with the best libraries. Documentation and tutorials are a bit lackluster though, and tool support isn't too great either. To be honest, most dependently typed languages aren't very fully developed at the moment.

If you instead went with the slightly weaker demand that your language should have GADT's, there are two very well maintained options: Scala and Haskell. IMHO you get most of the benefits of dependent types by using GADT's, and you keep typechecking decidable to boot.

Scala and Haskell both have large and well documented libraries, a working tool chain, as well as FFI's (to Java and C respectively). Both also have communities using them to solve real-world problems, like parsing and web development.

Answer 2

The accepted answer contains misinformation. Typechecking in Agda is decidable unless you switch off positivity/termination/universe checking. Moreover, infinite processes are programmable in Agda, just as IO processes are programmable in Haskell: the only restriction is that infinite processes cannot be unfolded indefinitely when being executed in the course of typechecking. You can implement a Turing Machine simulator in Agda: you just can't tell the lie that it's guaranteed to terminate or persuade the typechecker to run it in an unbounded way.

I do, however, agree that dependently typed languages are still at the experimental stage when it comes to "real world" programming. We can't yet support heavy duty development, but we can sustain a significant hobby amongst those with an eye to the future, rather like functional languages in the old days.

Idris, as suggested by Twey, is the closest candidate to a "real world" dependently typed language. It's much more focused on getting stuff done than Agda is. I'd recommend Agda as the better vehicle for getting to grips with the ideas behind dependently typed programming, but Idris is the more practical option.

It is, I'm pleased to say, worth considering recent releases of Haskell as a candidate in this discussion. Since GHC 7.4, Haskell has started supporting a useful notion of type level data, and with at least the singleton technique (a kludge though that is), we can really have types depending on run-time values (by making them depend on static variables constrained to equal run-time values). Haskell is thus a real "real world" language in the early phase of experimenting with dependent types.

Answer 3

Agda is not designed to be a general-purpose programming language. ATS is a dependently-typed language that is designed for low-level programming, though it's somewhat less elegant than Agda. Idris is a fledgeling dependently-typed language designed for performant applications-level programs.