8 ms·

In this I prefer logical reasoning to empirical evidence. Consider a function that takes a list of things and returns the last one. Let's write that function

In this I prefer logical reasoning to empirical evidence. Consider a function that takes a list of things and returns the last one. Let's write that function in Haskell. last :: [a] -> a Without looking at an implementation, let's think of how many ways this function could possibly go wrong? It could return the first element of the list instead of the last one. It could return the second to last element of the list. More generally, it could return any one of the elements of the list that was passed in. But that's it (other than the empty list case which for simplicity we can ignore because it's a condition we can statically detect). There are no other possibilities, period. Now think about implementing this function in any other language. What about Java? public Object last(Object objs[]) This function can return any of the elements of the incoming array. It could also return null. It could also return the int 42, or the string "hello". It could delete files on your hard drive, open a network connection and phone home to the NSA. I could go on and on. The point here is that you simply can't say as much about what this function could be doing as we could say about the Haskell version. This is the case for every mainstream language in wide use today. Some languages allow you to say a little more than others, but none of them come close to what Haskell gives you. Because of this, I don't really feel a pressing need for empirical evidence. Logical reasoning lets me make that claim quite confidently.

infraruby 12y ago
> There are no other possibilities, period. That's true! You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general. In general you may prefer the alternative (inductive) claim "more likely to be correct", but that claim requires empirical evidence.
- mightybyte 12y ago
  The inductive claim "more likely to be correct" is strongly supported by the evidence gained from enumerating the number of ways the functions could go wrong. Now if we want to expand our domain out from just that function to programs in general, we need an idea of how applicable those ideas are to larger programs. The biggest source of reducing error cases in my example was purity. Some parts of programs (namely the side effecting parts) can't be expressed as pure functions. So the next piece of evidence we need is an estimate of the percentage of large programs that can be expressed as pure functions. From my experience writing Haskell full-time for the last five years I can tell you that it is very substantial. Even in very impure code you can often factor out lots of small pure operations. I feel very safe in claiming that at least a third of Haskell code can be written with pure functions, and I think it's likely greater than half. (It could be a lot higher, but I'm trying to keep the confidence level fairly high.) You don't have to take my word for this. You can go off and browse through millions of lines of Haskell on [Hackage](http://hackage.haskell.org/packages/ http://hackage.haskell.org/packages/) and see for yourself. It probably wouldn't be too difficult to write an automated script to do this. Now we've seen that pure functions have a small fraction of the error conditions that impure functions have. And we've seen that maybe half of all the code we write can be expressed that way. That's a pretty dramatic reduction in the number of potential error conditions we might encounter for even complex programs. That is why I think the claim "more likely to be correct" is strongly supported by evidence.
  - infraruby 12y ago
    > It could be a lot higher I'd believe 95% LOC don't perform IO, just like any codebase in any language, though it may be easier in Haskell to identify which LOC those are. But it doesn't matter! The problem could be in the non-IO functions. Take this "scary!" line of code: rm -rf "$STEAMROOT/"* That's a correct IO function (rm -rf) using the result of an incorrect non-IO function ("$STEAMROOT/"*).
    - codygman 12y ago
      I see that as a null error. Using maybe or optional would have solved that problem.
      - infraruby 12y ago
        > Using maybe or optional would have solved that problem. If the code were written correctly then it would be correct!
        the_af 12y ago
        It's more like "if the code were written like Haskell programmers write programs, taking full advantage of static types to encode information about function return values, then it would be correct. Forgetting to handle the 'null' option would be detected at compile time."
        infraruby 12y ago
        > if the code were written like Haskell programmers write programs [...] then it would be correct and if the code were written like (true) bash programmers write programs, taking full advantage of "set -u" and "test", then it would be correct.
        the_af 12y ago
        There is a big difference: "set -u" won't reject incorrect bash programs, it will merely stop some kinds of incorrect behaviors by stopping the program and preventing it from causing greater harm. However, the program won't have completed its intended task, therefore remaining incorrect. In contrast, using Maybe to indicate "possibly no value" in Haskell (as it is standard practice; in fact there are no nulls in the language) prevents you from even writing some kinds of incorrect programs in the first place. In this sense, a program written in Haskell is a lot more likely to be correct than one written in bash, because the compiler will force you to consider cases you may have missed in a less safe language (like bash). Of course, neither language guarantees correctness. It's just that one is safer than the other by design.
- djur 12y ago
  I really wish static typing advocates would consider making inductive claims. The last few times I've asked for such evidence the response has been along the lines of "you just don't understand". It's indicative of a general intellectual orientation that I think has held back the introduction of valuable PLT concepts into mainstream languages.
- codygman 12y ago
  > You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general. Are you sure it does not hold in general? Upon repeating mightybytes example with all Haskell functions vs another language I feel like you'd get similar results due to pervasive purity and the type system.
eru 12y ago
Actually, using a non-total function like last doesn't do your claims any favours. I'd have picked map as the canonical example for free theorems.
- mightybyte 12y ago
  I chose that non-total function because it is easier to enumerate all the possible error cases than with the map function. And the error case is easily handled by the combination of incomplete pattern match and Safe Haskell. I was also trying to emphasize purity more than free theorems.

infraruby 12y ago

> There are no other possibilities, period. That's true! You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general. In general you may prefer the alternative (inductive) claim "more likely to be correct", but that claim requires empirical evidence.

mightybyte 12y ago
The inductive claim "more likely to be correct" is strongly supported by the evidence gained from enumerating the number of ways the functions could go wrong. Now if we want to expand our domain out from just that function to programs in general, we need an idea of how applicable those ideas are to larger programs. The biggest source of reducing error cases in my example was purity. Some parts of programs (namely the side effecting parts) can't be expressed as pure functions. So the next piece of evidence we need is an estimate of the percentage of large programs that can be expressed as pure functions. From my experience writing Haskell full-time for the last five years I can tell you that it is very substantial. Even in very impure code you can often factor out lots of small pure operations. I feel very safe in claiming that at least a third of Haskell code can be written with pure functions, and I think it's likely greater than half. (It could be a lot higher, but I'm trying to keep the confidence level fairly high.) You don't have to take my word for this. You can go off and browse through millions of lines of Haskell on [Hackage](http://hackage.haskell.org/packages/ http://hackage.haskell.org/packages/) and see for yourself. It probably wouldn't be too difficult to write an automated script to do this. Now we've seen that pure functions have a small fraction of the error conditions that impure functions have. And we've seen that maybe half of all the code we write can be expressed that way. That's a pretty dramatic reduction in the number of potential error conditions we might encounter for even complex programs. That is why I think the claim "more likely to be correct" is strongly supported by evidence.
- infraruby 12y ago
  > It could be a lot higher I'd believe 95% LOC don't perform IO, just like any codebase in any language, though it may be easier in Haskell to identify which LOC those are. But it doesn't matter! The problem could be in the non-IO functions. Take this "scary!" line of code: rm -rf "$STEAMROOT/"* That's a correct IO function (rm -rf) using the result of an incorrect non-IO function ("$STEAMROOT/"*).
  - codygman 12y ago
    I see that as a null error. Using maybe or optional would have solved that problem.
    - infraruby 12y ago
      > Using maybe or optional would have solved that problem. If the code were written correctly then it would be correct!
      - the_af 12y ago
        It's more like "if the code were written like Haskell programmers write programs, taking full advantage of static types to encode information about function return values, then it would be correct. Forgetting to handle the 'null' option would be detected at compile time."
        infraruby 12y ago
        > if the code were written like Haskell programmers write programs [...] then it would be correct and if the code were written like (true) bash programmers write programs, taking full advantage of "set -u" and "test", then it would be correct.
        the_af 12y ago
        There is a big difference: "set -u" won't reject incorrect bash programs, it will merely stop some kinds of incorrect behaviors by stopping the program and preventing it from causing greater harm. However, the program won't have completed its intended task, therefore remaining incorrect. In contrast, using Maybe to indicate "possibly no value" in Haskell (as it is standard practice; in fact there are no nulls in the language) prevents you from even writing some kinds of incorrect programs in the first place. In this sense, a program written in Haskell is a lot more likely to be correct than one written in bash, because the compiler will force you to consider cases you may have missed in a less safe language (like bash). Of course, neither language guarantees correctness. It's just that one is safer than the other by design.
djur 12y ago
I really wish static typing advocates would consider making inductive claims. The last few times I've asked for such evidence the response has been along the lines of "you just don't understand". It's indicative of a general intellectual orientation that I think has held back the introduction of valuable PLT concepts into mainstream languages.
codygman 12y ago
> You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general. Are you sure it does not hold in general? Upon repeating mightybytes example with all Haskell functions vs another language I feel like you'd get similar results due to pervasive purity and the type system.

eru 12y ago

Actually, using a non-total function like last doesn't do your claims any favours. I'd have picked map as the canonical example for free theorems.

mightybyte 12y ago
I chose that non-total function because it is easier to enumerate all the possible error cases than with the map function. And the error case is easily handled by the combination of incomplete pattern match and Safe Haskell. I was also trying to emphasize purity more than free theorems.