@serokell #SerokellChat A5:
Over-engineering.
Don't try to encode too much at the type level, the type system has its limits.
With experience, you will discover these limits.
I would love to see a collection of examples or some broad guidelines, like what leads to failure. People typically share positive experiences, so it's a rarity
@Rizary some things may be to cumbersome to encode in Haskell's type system - e.g. unless you're fine with defunctionalization techniques, doing non-trivial type-level stuff may be hard, similarly many ideas require some sort of dependent types emulation - and that requires a lot of TH/boilerplate
It's not that those encodings would be bad idea in principle, but they don't pay for themselves when it comes to added complexity they introduce in current Haskell
It's not even that they should be fully avoided - Galois has some experience with using them: http://davidchristiansen.dk/pubs/dependent-haskell-experience-report.pdf
The tldr; on the paper: if you value correctness and refactoring going to full dependent Haskell is a net win in a large, complex project where tiny details like bounded bit-wise operations can have big consequences if you get them wrong. The project they're talking about, Crucible, is used in validating secure code.
The difficulties are the usual suspects: it requires a certain amount of expertise to contribute at a high-level to the codebase. Tool support is good but the interactive tools struggle with dependent Haskell. They encountered GHC bugs (80k SLOC of bleeding-edge dependent Haskell is not the baseline most features are tested against), the type system is limited in the expressivity of proofs it can verify.
They were using older versions of GHC at the time and they didn't use a dependently typed language because their code was performance sensitive and Haskell has decent profilers.
I feel like "smart constructors" are a really nice technique to get a lot of benefits like this without needing to make things so much more complicated
Yeah, that is hard. It is weird doing normally-partial stuff (like dividing by an arbitrary num) but not worrying about a bottom because you've validated that its OK (like if you implemented division and a NonZero smart constructor)
https://twitter.com/int_index/status/1255146184450007042
@serokell #SerokellChat A5: Over-engineering. Don't try to encode too much at the type level, the type system has its limits. With experience, you will discover these limits.
- Vladislav Zavialov (@int_index)"Why don't I make a zettel for it?"
Relevant post (I think)
https://williamyaoh.com/posts/2020-04-19-permissive-vs-restrictive.html
Hazem said:
Not really, this post is about learning Haskell by practice, not about actually using it
Sridhar Ratnakumar said:
I would love to see a collection of examples or some broad guidelines, like what leads to failure. People typically share positive experiences, so it's a rarity
What it means by encode too much at the type level?
@Rizary some things may be to cumbersome to encode in Haskell's type system - e.g. unless you're fine with defunctionalization techniques, doing non-trivial type-level stuff may be hard, similarly many ideas require some sort of dependent types emulation - and that requires a lot of TH/boilerplate
It's not that those encodings would be bad idea in principle, but they don't pay for themselves when it comes to added complexity they introduce in current Haskell
It's not even that they should be fully avoided - Galois has some experience with using them: http://davidchristiansen.dk/pubs/dependent-haskell-experience-report.pdf
The tldr; on the paper: if you value correctness and refactoring going to full dependent Haskell is a net win in a large, complex project where tiny details like bounded bit-wise operations can have big consequences if you get them wrong. The project they're talking about, Crucible, is used in validating secure code.
The difficulties are the usual suspects: it requires a certain amount of expertise to contribute at a high-level to the codebase. Tool support is good but the interactive tools struggle with dependent Haskell. They encountered GHC bugs (80k SLOC of bleeding-edge dependent Haskell is not the baseline most features are tested against), the type system is limited in the expressivity of proofs it can verify.
They were using older versions of GHC at the time and they didn't use a dependently typed language because their code was performance sensitive and Haskell has decent profilers.
I feel like "smart constructors" are a really nice technique to get a lot of benefits like this without needing to make things so much more complicated
They do but then the burden is still on the library author to uphold the invariants. And I don't trust myself :sweat_smile:
Yeah, that is hard. It is weird doing normally-partial stuff (like dividing by an arbitrary num) but not worrying about a bottom because you've validated that its OK (like if you implemented division and a NonZero smart constructor)
@TheMatten i see.. Thank you, I'll read that paper
http://okmij.org/ftp/Haskell/dependent-types.html