3 ms·

> I think this is the red herring at the heart of the problem. Those bugs really aren't a big deal, they happen rarely once you're proficient and they are quick

by Peaker 13y ago

> I think this is the red herring at the heart of the problem. Those bugs really aren't a big deal, they happen rarely once you're proficient and they are quickly solved on the rare occasion when they do happen. This is simply not true. I don't only work in Haskell. I also work with many colleagues on C and on Python. Virtually every bug in C or Python that we encounter, including ones we have to spend a significant amount of time debugging is a bug that cannot happen in the presence of Haskell's type system. > I'm talking about logic bugs, the kind that your compiler isn't going to find, or even that a "sufficiently smart compiler" couldn't find because it's a misunderstanding in the specification that you have to bring back to the product owner for clarification. Or bugs that occur when 2 different services on different machines are treating each other's invariants poorly. Those are the bugs I spend time on. If you had experience with advanced type systems -- your claims here would carry more weight. People who don't know advanced type systems tend to massively understate their assurance power. For example 2 different communicating services might use "session types" to verify that their protocol guarantees invariants. Or maybe the only type-checked programs are ones forced to reject invalid inputs that violate invariants. > I haven't spent any time at all with Haskell, really, but it seems like a poor trade off to have to learn a bunch and engineer things in a way that's more difficult in order to prevent the easiest bugs. They aren't the "easiest bugs" at all. For example, consider implementing a Red Black Tree. In Go, imagine you had a bug where you rotate the tree incorrectly, such that you end up with a tree of the wrong depth -- surely you would have considered this a "logic" bug. One of the harder bugs that you wouldn't expect to catch with a mere type system. In Haskell, I can write this (lines 27-37): https://github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs#L27 https://github.com/yairchu/red-black-tree/blob/master/RedBla... to specify my red black tree, with type-level enforcement of all of the invariants of the tree. With just these 10 lines, I get a compile-time guarantee that the ~120 lines implementing the tree operations will never violate the tree's invariants. This logic bug simply cannot happen. Learning a bunch of techniques is a one-time investment. After that, you will build better software for the rest of your career. Debugging far fewer bugs for the rest of your career. How could you possibly reject this trade-off, unless you expect a very short programming career?

jbooth 13y ago
I meant less interesting logic bugs, like "Oh we never considered the intersection of these 3 different business use cases". I could see a couple ways where the type system could be more powerful than unit tests, but only to the extent that your unit tests didn't cover some obvious cases to begin with. Why not just write unit tests? As for how I could possibly reject the trade-off... I mean, nobody's gonna hire me to code Haskell and my side projects are too systemy and not lispy enough to even consider it. Thanks for the code sample though, I plan on looking at this more later tonight and getting a feel for it (barely glanced just now).
- Peaker 13y ago
  > Oh we never considered the intersection of these 3 different business use cases Take a look at the history of any repository near you, for a project that uses C, Python or Java. Review bug fix commits. See how many of them relate to "business use cases" and how many relate to implementation bugs. I believe you'll find the latter is far more common. Even in the "business use cases", enforced invariants will be a tramendous help. In the infinite possibilities of all the use cases, none will be able to break any invariant forced by the type system. When you set out to prove a property of your program, you will end up finding bugs, almost regardless of what properties you are trying to prove. Writing unit tests is also useful. But if I can have 10 lines in my Red Black Tree that mean I don't have to write any test whatsoever for the tree's invariants -- I saved myself from a whole lot of work writing and later maintaining tests with every change. Generally, to get similar confidence levels from unit tests as you get from types, you'll need to write many more tests. If I had to choose whether to trust a well-typed system written in Agda (which is similar to Haskell but has an even more powerful type system) with only the most trivial testing done, or trust a highly tested system written in dynamic or a much weaker type system, I'd definitely trust Agda more. Or if I were to trust my 10 lines of type code or hundreds of lines of tests for the invariants of the tree, of course the 10 lines of code are far more reliable and easier to maintain.
  - jbooth 13y ago
    Honestly, in my case, for my day job, it's way, way more "business use case" or more frequently "misunderstanding between 2 services" than it is an implementation error. We catch 90% of implementation problems with unit testing and/or just plain sanity checking it before release. Maybe Haskell could help us by making unit testing easier/unnecessary but of course there's no switching at this point. We're probably a bit of an edge case being a very service oriented architecture. (1,000 servers, 6-7 major classes of server, handling 10B (yes B) requests a day). Most of our bugs consist of a flawed assumption that crosses 3-4 service boundaries on it's way off the rails. I'll admit I'm ignorant of Haskell but I just don't see a type system fixing that for us.

by Peaker 13y ago

jbooth 13y ago

I meant less interesting logic bugs, like "Oh we never considered the intersection of these 3 different business use cases". I could see a couple ways where the type system could be more powerful than unit tests, but only to the extent that your unit tests didn't cover some obvious cases to begin with. Why not just write unit tests? As for how I could possibly reject the trade-off... I mean, nobody's gonna hire me to code Haskell and my side projects are too systemy and not lispy enough to even consider it. Thanks for the code sample though, I plan on looking at this more later tonight and getting a feel for it (barely glanced just now).

Peaker 13y ago
> Oh we never considered the intersection of these 3 different business use cases Take a look at the history of any repository near you, for a project that uses C, Python or Java. Review bug fix commits. See how many of them relate to "business use cases" and how many relate to implementation bugs. I believe you'll find the latter is far more common. Even in the "business use cases", enforced invariants will be a tramendous help. In the infinite possibilities of all the use cases, none will be able to break any invariant forced by the type system. When you set out to prove a property of your program, you will end up finding bugs, almost regardless of what properties you are trying to prove. Writing unit tests is also useful. But if I can have 10 lines in my Red Black Tree that mean I don't have to write any test whatsoever for the tree's invariants -- I saved myself from a whole lot of work writing and later maintaining tests with every change. Generally, to get similar confidence levels from unit tests as you get from types, you'll need to write many more tests. If I had to choose whether to trust a well-typed system written in Agda (which is similar to Haskell but has an even more powerful type system) with only the most trivial testing done, or trust a highly tested system written in dynamic or a much weaker type system, I'd definitely trust Agda more. Or if I were to trust my 10 lines of type code or hundreds of lines of tests for the invariants of the tree, of course the 10 lines of code are far more reliable and easier to maintain.
- jbooth 13y ago
  Honestly, in my case, for my day job, it's way, way more "business use case" or more frequently "misunderstanding between 2 services" than it is an implementation error. We catch 90% of implementation problems with unit testing and/or just plain sanity checking it before release. Maybe Haskell could help us by making unit testing easier/unnecessary but of course there's no switching at this point. We're probably a bit of an edge case being a very service oriented architecture. (1,000 servers, 6-7 major classes of server, handling 10B (yes B) requests a day). Most of our bugs consist of a flawed assumption that crosses 3-4 service boundaries on it's way off the rails. I'll admit I'm ignorant of Haskell but I just don't see a type system fixing that for us.