While there are/were several languages with dependent types, like Agda, Coq or Epigram, none seemed to gain wider adoption. Despite that dependent types allow very strong type safety, up to writing complete program specifications. Did anyone analyze what are the main blockers for such languages to become more mainstream?

  • You only have the capacity to learn a little beyond what you currently know, :. I think we will need much wider FP adoption before these DT really stats to make gains – jk. Aug 16 '16 at 8:45
  • 4
    That one is a PhD project, one is is a specialized proof assistant and one isn't being maintained probably have more to do with it than the presence of a certain feature. – Blrfl Aug 16 '16 at 9:43
  • 3
    1. Correct software is not a priority. 2. Lame ML-style syntax. 3. Lack of skilled developers. – Den Aug 16 '16 at 10:58
  • 3
    @Den: I Upvoted your comment for "Correct software is not a priority." – Giorgio Aug 16 '16 at 17:41

It's not enough for a language to have a nice feature, it also needs a compelling application. For example, functional programming languages didn't really take hold commercially until the growth of big data in general and Scala and Apache Spark in particular, and it is still largely limited to those niches.

Personally, I think dependent typing's "killer app" is its potential for tooling. If you've ever watched one of Edwin Brady's Type-driven development talks, you'll know what I mean. He can write a type signature, then hit a few shortcut keys to write the function body. With some refinement and UX, I think that could make dependent typing a must-have language feature at some point.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.