I am not sure if they serve the same purpose or how the venn diagrams overlap on this, but in 2000 I loved the idea of the assersion in Ada, and I love even more the idea the type system can prove your number is between 1 and 10 (etc.).
I reckon it occasionally will catch a bug, but more than that is perfect documentation. I don't want delay to be an int, I want it to be a RateLimitBackoffDelaySeconds which is between >0 and <60, for example.
https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...
https://davidchristiansen.dk/pubs/dependent-haskell-experien...
The video is on YouTube somewhere. Having used Haskell and some dependently typed Haskell around the same time, I thought it was a fair assessment of state of play.
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.
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.