> Essentially this means we have made the large majority of bugs impossible to be made in this language
Oh, please. Such a statement ignores the actual kinds of bugs that plague real complex systems. The abilities of static type systems to prevent bugs is dramatically overstated. Consider this:
Now, we all have our bugs, and this is not to beat up on Haskell for having them, but presumably they use their own tools to the greatest extent possible to ensure correctness. What type system is remotely close to being able to help prevent the kinds of bugs in this list? None, and none will any time soon. Because the biggest problems in software are problems of misconception - we've (usually correctly) implemented an incomplete or incorrect idea!
Type systems focus on solving the problems we can solve. Unfortunately, they're not the problems we have.
I spent 2 days last week hunting a bizarre bug that turned out to be ultimately due to a type ambiguity in how JDBC maps Java types to Oracle types. Admittedly this is not a language issue (well, it is on a deeper level), but it's the same sort of problem.
I don't know how much time I've lost in Java to checking, catching, and debugging stupid RuntimeExceptions that would easily be fixed by having a good type system, or writing idiotic boilerplate design patterns that you simply would not have to write if you had a good type system (or were using Clojure).
No language in the world will save you from having to think about your program's desired behavior, but that doesn't mean we should make it hard on ourselves to even implement the behavior we think we want.
> No language in the world will save you from having to think about your program's desired behavior, but that doesn't mean we should make it hard on ourselves to even implement the behavior we think we want.
Therein lies the rub. Is there no cost to static typing? Is it not complex? Is it sufficiently expressive? Does it never make it harder to implement the behavior we think we want?
Should everyone write everything in every program in as provable a way as possible? If not, why not?
As the example here shows, there is a cost in effort expended and complexity:
I'm quite glad people are working on these things, and they have genuine benefits. But to overstate the benefits and ignore the costs (as did the post to which I replied) is not productive.
>Does it never make it harder to implement the behavior we think we want?
I should ask why you're aiming at "never"? I prefer to quantify "how often it makes writing harder". It is more useful.
I think that types could make writing behaviour we want even easier. For example, you could use "session types" and be sure that your routers always understand each other. You can write complex algorithm while establishing its complex invariants in types and be sure you're correct.
I agree that this won't solve all bugs, maybe not even the majority. But I am convinced it solves a significant amount of bugs. Personally I find that an expressive type system can aid significantly in discovering your own misconceptions and clarifying what you intend to do.
When coding Haskell I tend to start by envisioning the type I need my program to have and then fill the code from there.
Oh, please. Such a statement ignores the actual kinds of bugs that plague real complex systems. The abilities of static type systems to prevent bugs is dramatically overstated. Consider this:
http://hackage.haskell.org/trac/ghc/query?status=new&sta...
Now, we all have our bugs, and this is not to beat up on Haskell for having them, but presumably they use their own tools to the greatest extent possible to ensure correctness. What type system is remotely close to being able to help prevent the kinds of bugs in this list? None, and none will any time soon. Because the biggest problems in software are problems of misconception - we've (usually correctly) implemented an incomplete or incorrect idea!
Type systems focus on solving the problems we can solve. Unfortunately, they're not the problems we have.