5 ms·

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 ex

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).

twic 12y ago
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!
- freyrs3 12y ago
  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.
- tel 12y ago
  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.
- mercurial 12y ago
  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.
- aaronlevin 12y ago
  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! :)
aaronlevin 12y ago
twic: yes, if you take my statement literally you are correct: it is possible to introduce bugs in a Haskell program.

twic 12y ago

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!

freyrs3 12y ago
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.
tel 12y ago
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.
mercurial 12y ago
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.
aaronlevin 12y ago
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! :)

aaronlevin 12y ago

twic: yes, if you take my statement literally you are correct: it is possible to introduce bugs in a Haskell program.