Over-engineering in Haskell - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Sridhar Ratnakumar


Don't try to encode too much at the type level, the type system has its limits.

With experience, you will discover these limits.


Sridhar Ratnakumar

"Why don't I make a zettel for it?"

Cyril Valyavin

Hazem said:

Relevant post (I think)

Not really, this post is about learning Haskell by practice, not about actually using it

Cyril Valyavin

Sridhar Ratnakumar said:

"Why don't I make a zettel for it?"

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

James King

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.

Joel McCracken

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

Fintan Halpenny

They do but then the burden is still on the library author to uphold the invariants. And I don't trust myself :sweat_smile:

Joel McCracken

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