3 ms·

Yes. It could be much better but Dependent Haskell has been stymied by pearl clutching in the community about “pragmatism,” and “scaring away new users.” And a

Yes. It could be much better but Dependent Haskell has been stymied by pearl clutching in the community about “pragmatism,” and “scaring away new users.” And a few technical hurdles. I want Dependent Haskell to happen. I think that when you need it, you need it. And when you only have partial support for it you end up with a very confusing set of libraries and conventions to encode dependent types in Haskell that is probably more off-putting than proper language support (singletons, GADTs, type classes and associated type families and.. and.. and..). That being said, Haskell isn’t exactly funded by a company like Microsoft. It’s a small community and the teams driving these projects are small and staffed with keen volunteers for the most part. I don’t think DH will happen but I hope it will get through.

HKH2 2y ago
Isn't Idris basically Haskell with DT?
- wk_end 2y ago
  At the language level...sort of? Idris is strict, unlike Haskell. As of Idris 2, it also has a substructural type system which tracks how often terms are used, which is kind of Rust-y and can allow for better runtime performance by ensuring that proofs can be erased (IIUC). But besides just being a language, Haskell is a whole ecosystem. It's not an amazing ecosystem, but it's good enough for serious work. Idris is not and may never be. A fully-supported Dependent Haskell would be huge for dependent types in practice.
  - jech 2y ago
    > Idris is strict, unlike Haskell. "The next Haskell will be strict." — Simon Peyton-Jones