Dependent Haskell

Emulating dependent types (and, more generally, advanced type-level programming) has been a hot topic in the Haskell community recently. Some incredible work has been done in this direction: GADTs, open and closed type families, singletons, etc. The plan is to copy even more features to the type level, like type classes and GADTs, and simplify the promotion of value-level functions.

On the other hand, there’s a good deal of scepticism around this idea. «If you want to program like in Agda, why don’t you program in Agda?»

First, libraries. It took us many years to arrive at the state of hackage that is suitable for industrial usage — and we still don’t have satisfactory answers to many problems.

My guess is that it will take at least as long as that for the dependently typed community to arrive at this point — not only because of the smaller community, but also because they will look for even more type-safe solutions, which is naturally a harder problem.

Second, the compiler/runtime. How optimized is the generated code? Is there a profiler? How about concurrency and parallelism? Is there an FFI? How good is the garbage collector?

These questions are especially acute for Idris, which chose to have its own compiler. Code extraction into Haskell or OCaml may be a more viable alternative, but without having several real-world projects that are implemented this way it’s very hard to assess it properly.

No doubt, these (or other) languages will get there sooner or later. But it seems that practical dependently typed programming will become viable in Haskell much sooner than in Agda or Idris.