4 ms·

twelve years have passed - is DT less painful today?

clusterfook 2y ago
I am not sure, but as a Typescripter, I think I'd find refinement types easier - https://github.com/ucsd-progsys/liquidhaskell https://github.com/ucsd-progsys/liquidhaskell 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.
- IshKebab 2y ago
  As I understand the nomenclature liquid types are refinement types and they are dependent types, but typically when people say "dependent types" without qualification they mean the much more powerful (and difficult) "full" dependent types where you can do stuff like returning an int or a string depending on some runtime value. https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/ https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...
lambda_foo 2y ago
David Christiansen did a more recent experience report from 2019 about using Dependently Typed Haskell at Galois. https://davidchristiansen.dk/pubs/dependent-haskell-experience-report.pdf 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.
agentultra 2y ago
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

I am not sure, but as a Typescripter, I think I'd find refinement types easier - https://github.com/ucsd-progsys/liquidhaskell https://github.com/ucsd-progsys/liquidhaskell 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.

IshKebab 2y ago
As I understand the nomenclature liquid types are refinement types and they are dependent types, but typically when people say "dependent types" without qualification they mean the much more powerful (and difficult) "full" dependent types where you can do stuff like returning an int or a string depending on some runtime value. https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/ https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...

lambda_foo 2y ago

David Christiansen did a more recent experience report from 2019 about using Dependently Typed Haskell at Galois. https://davidchristiansen.dk/pubs/dependent-haskell-experience-report.pdf 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.

agentultra 2y ago

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