Typesafe =! Correct

by chromatic

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.


11 Comments

Adam Turoff
2006-03-07 13:47:24
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.

chromatic
2006-03-07 14:19:21
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....
Adam Turoff
2006-03-07 18:17:02
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.

AndreasRomeyke
2006-03-08 04:17:19
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.
Dave
2006-03-08 05:37:16
*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."

A. Coward
2006-03-08 07:44:41
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.

nothingmuch
2006-03-08 14:44:36
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

Stevan Little
2006-03-08 14:53:48


This reminds me of one of my favorite quotes of all time:



On two occasions I have been asked by members of Parliament, "Pray, Mr. Babbage, if you put into the machine wrong figures, will the right answers come out?" I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question.


-- Charles Babbage, 1792-1871


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.

chromatic
2006-03-08 15:26:29
Even without user input, the typing would still be incorrect. Change main to:


main :: IO ()
main = putStrLn (show (badSqrt (0 - 10)))


(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 approximate where x will never equal y if 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.

Stevan Little
2006-03-08 17:00:36


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 :)

Alan Kelon
2006-03-19 20:01:08
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.