One of the big myths that advocates of static typing like to wave around is the idea that having the compiler catch certain types of errors reduces the likelihood of errors in your program.
One of the big arguments of dynamic typing advocates is that you still have to write tests for your code and those types of errors don’t often come up anyway.
Now no one ought to take the arguments of C, C++, or Java programmers seriously when they start talking about the strength of their typing systems, but when certain Haskell advocates claim that “If it compiles, it’s likely correct!” then things get a little ridiculous.
It’s easy to write a perfectly type-safe Haskell program that (accidentally) gives the wrong answer… or fails to complete. (Okay, I admit I just wanted to write a program that gave the wrong answer instead of proving the halting problem by example, but bear with me.) Here’s a simple, 19-line Haskell program that could be shorter if it weren’t didactic (or I were a better Haskell program). It uses very simple Newtonian approximation to produce the square roots of given integers:
main :: IO ()
main = do
num <- getLine
putStrLn (show (badSqrt (stringToInteger num)))
stringToInteger :: String -> Integer
stringToInteger s = read s::Integer
badSqrt :: Integer -> Float
badSqrt 0 = 0
badSqrt x = approximate (fromInteger x) 1
approximate :: Float -> Float -> Float
approximate x y
| x == y = x
| otherwise = approximate new_x new_y
where
new_x = ( x + y ) * 0.5
new_y = ( x * y ) / new_x… except that it only works on positive integers.
Sure, it compiles and runs just fine. At least, it appears fine until someone asks “Hey, it handles integers! How does it do when you ask for the square root of a negative number?”
Not well.
Typesafety does not necessarily imply correctness. Maybe more charitably I should say that a “correct” program won’t necessarily behave correctly or give you the correct answers.
That doesn’t mean that program correctness is useless, that Haskell’s a bad language, or that strict typing and type inferencing are never helpful. It just means that not all errors in a program are type errors. Please use the word “correct” with respect to programs… more correctly.
Note that the claim is that if it gets past the type system, it's likely correct. It's not a guarantee that the program is either correct or bug free, as demonstrated by these two one-liners:
main = head [] -- runtime exception
main = length [1..] -- fails to terminate
See? It's not perfect. Two well-typed programs that are trivially undefined. No need to construct elaborate examples involving operations on non-negative integers. :-)
The type system cannot find every bug, and no one ever claim it did. The problem here is that the term "correct" is rather overloaded. In the Haskell sense of the word, it means "proven," not "bug-free." The distinction goes back ages, to Knuth's quote from 1977: Beware of bugs in the above code; I have only proved it correct, not tried it.
My goal was merely to provide an example that looked correct (in the "does what I want") sense, not to show the smallest possible incorrect code that passes the typechecker. To be fair as well, tests that didn't explore the boundary cases wouldn't expose this error either....
We're in violent agreement that typesafe programs are interesting, but not bug-free.
The problem lies in the interpretation of "correct". As Inigo Montoya would say, I do not thing that word means what you think it means. Within academic computer science, correct == typesafe. Outside academia, correct has a looser definition, comparable to bug-free.
Talking about Haskell (or Hindley-Milner to be more specific) outside of academia forces you to be conscious of whether you are using the constrained interpretation of "correct" (as in == typesafe), or the conventional interpretation of "correct" (as in == bug-free, or "faithfully implements the requirements").
It's the same problem in Perl/Python/Ruby/PHP using the term "compiled". You can claim that Perl isn't compiled because /usr/bin/perl doesn't produce .o files to feed to ld. But you can also claim that Perl is compiled because a script, once loaded, is converted into a bytecode representation that is processed to execute the program.
IMHO your program is incorrect because you use the wrong type for your case. Either you uses integer (means with positive and negative sign) and the result is expected incorrect, or you should create a new type pos_int_t (positive integer) which is expected input-type of your function. In that case type-safety implies correctness because the function works in the whole input-space.
*Mumble* years ago I used an example to help illustrate this point. My audience included some programmers whose testing was less than completely thorough. It went something like this.
"I have here the source for a project I wrote as a college freshman. It is a program that plays an unbeatable game of tic-tac-toe. The interface is extremely simple. It doesn't access any external resources. It played thousands of games against similar programs as a test. As a result, I'm confident that it is bug-free. Now I am going to rename it "Accounts Receivable" and recompile it. It compiles without any errors or warnings. It still never crashes or hangs. It performs exactly as before. However, I'm quite certain that it does not meet its new requirements."
Well, I'm a pedantic (ex-)mathematician, and I'd say that your program is a completely correct implementation of the Newton's Method algorithm.
However, Newton's Method is not proven to work in every situation, unlike, say, the merge sort algorithm. This probably sounds like a silly distinction, but I don't think it is. All a language can do is help you in your translation from algorithm to implementation - if you choose a bad algorithm no language feature will save you.
The best example from my own experience is using 'foreach' in Perl. I used to iterate over arrays with
for(i=0; i< arr.size; i++) { do something with arr[i] }There's lots of room for silly mistakes in there. But now that I use
foreach( $elt in @arr) { do something with $elt }it's really hard to make a mistake. The language feature (foreach) has helped me correctly translate my idea/algorithm into code.
There is a system that allows you to make runtime values more type safe in this manner. It is beyond me though, so please ask audrey for reference on this (mention esteemed philanthropy). The article which describes it has a type system that proves that an implementation of merge sort is correct.
Regardless, here is my take at using Haskell's type system in a way that many other programming languages can't, in order to make this example still better in haskell than in most other languages.
What I'm doing is creating a type that wraps around Integer, that only a specific function can provide, and this function is in the Maybe monad. This ensures that as long as I create this type only using the right function (assertPositive) the compiler will help me make sure I'm not misbehaving.
There is no silver bullet for typing runtime values, even more so for constraining runtime values, but this is not the type system's fault.
main :: IO ()
main = do
num <- getLine
putStrLn (show (maybeSqrt (stringToInteger num)))
stringToInteger :: String -> Integer
stringToInteger s = read s::Integer
newtype NaturalInteger = NI Integer
assertPositive :: Integer -> Maybe NaturalInteger
assertPositive x | x > 0 = Just $ NI x
| otherwise = Nothing
maybeSqrt x = do
num <- assertPositive(x)
return $ goodSqrt num
goodSqrt :: NaturalInteger -> Float
goodSqrt (NI 0) = 0
goodSqrt (NI x) = approximate (fromInteger x) 1
approximate :: Float -> Float -> Float
approximate x y
| x == y = x
| otherwise = approximate new_x new_y
where
new_x = ( x + y ) * 0.5
new_y = ( x * y ) / new_x
This reminds me of one of my favorite quotes of all time:
First, your code uses user input, which means you have an unknown whose type cannot be determined until runtime, so of course you can't catch type errors at compile time.
And secondly, your program is incorrectly typed. You should have created a Natural type (representing all positive integers) and that is what should be in the signature for badSqrt. Of course this doesn't matter so much because we still won't catch the error at compile time since you are asking for user input, but at least it will fail (from a type error) when it is supposed to.
Even without user input, the typing would still be incorrect. Change
mainto:(The math expression there is because I couldn't quickly figure out how to encode negative constants in my code.)
The compiler doesn't catch the math error in
approximatewherexwill never equalyif one of them is negative -- it always recurses otherwise.Again, I'm not claiming that type inferencing is bad or that Haskell is useless or this program is a good example of what to do. I'm just suggesting that even with one of the better type systems in the world, there's a huge class of errors that are still trivially easy to introduce.
Fine, but if you take user input out of the equation, that still does not make it your program well typed. Clearly your badSqrt function should only accept non-negative integers. Part of the power of Haskell (and ML and Ada and other language with nice subtyping facilities) is the ability to declare a subtype of a built in type like Integer, instead of having to do manual bounds checking like you would in Perl/Python/etc.
Now you could argue that the compiler still did not catch your error, but the fact is that your error is more that you did not give Haskell enough information. According to what you told the compiler, badSqrt can handle Intergers, even though you know that it actually can't. Even Haskell compilers cannot read minds :)
Software per si is not correct because it is only correct when it is in accordance with its specification, so is reasonable to use the word consistent software instead of correct software [Hoare 1969].
Hoare, C. A. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576-580.