Hacker News new | ask | show | jobs
by aaronlevin 4442 days ago
You can encode a specification within Haskell's type system and get guarantees that are very difficult in other languages. Gabriel's pipes library is a great example of this (see a Pipe's associativity laws).
2 comments

twic: yes, if you take my statement literally you are correct: it is possible to introduce bugs in a Haskell program.
Oh, sure. Haskell's type system is famously powerful. But the simple fact is that it does not preclude bugs. It is possible to have bugs in Haskell programs!
Nobody who knows what they're talking about says that Haskells types (or even Idris/Agda/Coq's types) "preclude bugs" but instead that they "eliminate some classes of bugs so long as you don't behave really pathologically".

That's a much weaker statement, but still a valuable property.

I did not say it was impossible to write Haskell with bugs. I simply stated that you are not guaranteed that a particular implementation of a design pattern adheres to the patterns semantics, therefore introducing a bug. With good usage of Haskell's type system, you can wholly avoid such bugs, and a great example of this, as I stated, is the associativity laws within the pipes library.

Semantics! :)

That's like saying that because it's possible that the roof may occasionally leak you shouldn't have a roof over your head at all.
No language "precludes bugs". You can get bugs because you didn't leverage Haskell's type system ("let's use String for everything"), logic bugs, or simply bugs caused by a faulty understanding of the problem. What you're not going to get is NPEs, or unwanted side-effects. Since it takes very little work in Haskell to ensure statically that two numbers which represent two different notions (say, mass and velocity) have different types, it's going to be lot easier to get a robust program.

But no, Haskell is not a silver bullet, and comes with a number of significant drawbacks.