4 ms·

> saying "if it compiles it works" is one of the most damaging things people say about Haskell I've recently been getting a lot of logic errors with code at wo

> saying "if it compiles it works" is one of the most damaging things people say about Haskell I've recently been getting a lot of logic errors with code at work I'm working on for a typeclass instance, so the "if it compiles it works" phrase has been banging around my head. It's not always true with how most Haskell is written, however even the current logic errors I'm having, I can imagine how I could turn them into type errors or how I could encode the logic in the types. However you can still get a logic error with your types as well. I think it's still a win as long as encoding those logic errors doesn't increase complexity too much.

iamcurious 11y ago
To truly encode it you need dependent types, but even then you might get a beautiful specification and a program that is proved to satisfy it, only to find that you had the specification wrong. Wow, is programming hard!
- codygman 11y ago
  I mostly agree, but I'll say (usually at the cost of more complexity upfront) you can encode quite a bit of logic into Haskell's type system. But yes, you can easily create a beautiful specification for the wrong thing. I think that is worlds better than accidentally creating the right thing. We want precision right? Not to brute force try solutions until one seems to work that blows up later?
  - iamcurious 11y ago
    you can encode quite a bit of logic into Haskell's type system You are right, it has limits, but we can push those limits quite a bit. A nice trick is to avoid Bool and look for richer types instead. For instance, avoid <= :: a -> a -> Bool. Use compare :: a -> a -> Ordering. We want precision right? Not to brute force try solutions until one seems to work that blows up later? Not sure. I like precision. I like to study it, I like to be able to use, I hate when other people don't use it, but I have come a long way building the discipline to use it consistently. Some days I still choose nasty hacks.

iamcurious 11y ago

To truly encode it you need dependent types, but even then you might get a beautiful specification and a program that is proved to satisfy it, only to find that you had the specification wrong. Wow, is programming hard!

codygman 11y ago
I mostly agree, but I'll say (usually at the cost of more complexity upfront) you can encode quite a bit of logic into Haskell's type system. But yes, you can easily create a beautiful specification for the wrong thing. I think that is worlds better than accidentally creating the right thing. We want precision right? Not to brute force try solutions until one seems to work that blows up later?
- iamcurious 11y ago
  you can encode quite a bit of logic into Haskell's type system You are right, it has limits, but we can push those limits quite a bit. A nice trick is to avoid Bool and look for richer types instead. For instance, avoid <= :: a -> a -> Bool. Use compare :: a -> a -> Ordering. We want precision right? Not to brute force try solutions until one seems to work that blows up later? Not sure. I like precision. I like to study it, I like to be able to use, I hate when other people don't use it, but I have come a long way building the discipline to use it consistently. Some days I still choose nasty hacks.