> The answer to why Haskell should add dependent types is that it's an interesting research question, and that Haskell is designed to answer research questions.

> The answer to why Haskell should add dependent types is that it's an interesting research question, and that Haskell is designed to answer research questions. Interesting, yes, but I believe it will also have practical benefits for engineers using the language as well. I hope Haskell will migrate to dependent types because it will unify the language. Some of the more frustrating features of Haskell are due to it having a separate language for types and terms. When people see a huge list of language pragmas and the singleton libraries being pulled out this is what I hear people frequently complain about when they say Haskell is too complicated. If you can remove the barrier between types and terms then most of that added complexity goes away. A good example of this is Lean. It's implemented in a dependently typed programming language because it unifies types and terms which makes writing the compiler and programs more simple. I think this could also be extended to Haskell. It will be difficult, and presented as a "grand challenge," because unlike Lean, Haskell has many more libraries and applications that depend on it and we all know how breaking compatibility goes. > They are separate because the concerns of engineers and researchers are vastly different. In the twenty some years that I've been fortunate enough to write software for a living I don't believe this is true. I find that in software engineering that research and application inform one another and have a tight feedback loop. I read papers and often I implement them to help solve problems. Often in implementing that research I find feedback to give the authors or I find new problems that require some research in order to solve. Pure mathematicians have it a bit harder. I lament that John Conway may never live to see the solution to some of the problems he's posed. But I think we have it pretty good. The logicians have done most of the work for us. And we can implement new theories quite fast. BTW I'm not saying you can't comment on or criticize Haskell, this is an interesting discussion. I am a little sensitive to people being contemptuous of the hard work others put into Haskell and was probably either misreading your comments or responding to that. For the people that do work on Haskell I think these are the great challenges for us to solve this decade. Algebraic effects have been used in production at Github and elsewhere and there's still work to do to make them shine but it's generally good stuff and moving in a positive direction. Same with dependent types. Regardless, thank you for being patient. I appreciate your work and your writing here and elsewhere. All the best.