An interview with Joey Hess

Posted Jan 19, 2016 23:24 UTC (Tue) by smoogen (subscriber, #97)
Parent article: An interview with Joey Hess

It is a bit long:

It's a myth that strongly typed or functional programs don't need testing. Although they really do sometimes work correctly once you get them to compile, that's a happy accident, and even if they do, so what — some future idiot version of the savant who managed that feat will be in the code later and find a way to mess it up.

but for me this is my quote of the week (and possibly the month). Thank you both Lars and Joey.

to post comments

An interview with Joey Hess

Posted Jan 20, 2016 0:00 UTC (Wed) by Sesse (subscriber, #53779) [Link] (4 responses)

Seriously, did anybody ever believe that? I know functional programming is surrounded by a certain aura of… mystique, but nobody in their right mind would ever say that C or Java code doesn't need testing just because it's strongly typed? :-)

/* Steinar */

An interview with Joey Hess

Posted Jan 20, 2016 0:05 UTC (Wed) by smoogen (subscriber, #97) [Link]

I have seen programmers say it about pretty much language... usually about their own code but extending it to the language or coding stance or "well that person was just stupid, if he knew the language that would never have happened."

An interview with Joey Hess

Posted Jan 20, 2016 15:05 UTC (Wed) by nybble41 (subscriber, #55106) [Link]

"Strongly typed" isn't enough, you also need an expressive type system, like in Haskell. Of course, you also need to make use of it properly. It's possible to write dynamically-typed (or unityped) code in almost any language.

It's not so much that the code doesn't need testing, as that the type system renders many common errors impossible, and thus does quite a bit of the testing for you in the form of static proofs at compile time. There are usually other properties not captured in the types which still need to be proved through traditional runtime tests.

In a dynamically-typed language, for example, you ought to have tests to show that a function which expects an integer responds correctly when passed a string, or some other non-integer type. In C you wouldn't write such a test, because the compiler won't let the user pass anything but an integer. Haskell is similar, except that its type system can encode much more interesting properties, so if you use it properly there are many more things that the compiler can prove about the code. As a semi-advanced example, say you have this GADT representing a simple language for managing the state of some variable:

data StateA s r where {
SetState :: a -> StateA a ();
GetState :: StateA a a;
}

The first type parameter represents the type of the state, and the second the type of the result from the action. The SetState constructor captures a value of the same type as the state, and the result type of GetState must match the state type. If you also have a function of type `runStateA :: StateA s r -> s -> (r, s)`, the compiler will take care of proving that if `runStateA (SetState 3) (5 :: Int)` terminates, it produces a value of type `((), Int)`, where the first element must be `()` and the second value can only be 3 or 5—as those are the only values of type `s` that runStateA has access to. The expression `runStateA GetState "Hello"` can only evaluate to `("Hello", "Hello")`; aside from non-termination, the runtime behavior is fully constrained by the types. The compiler will also prove that there are no side-effects or dependencies on anything other than the parameters to the function.

This does not eliminate all testing; you still need to show that `runStateA (SetState y) x == ((), y)`, since the types allow for SetState to be implemented as a no-op. It is also necessary to show that the function terminates, since the types won't prevent unbounded recursion or runtime exceptions. However, there is very little else that can actually go wrong in the implementation of runStateA.

An interview with Joey Hess

Posted Jan 28, 2016 12:00 UTC (Thu) by HelloWorld (guest, #56129) [Link] (1 responses)

People don't say that because C is not strongly typed. In fact C's type system is among the worst ones around.

An interview with Joey Hess

Posted Jan 28, 2016 16:43 UTC (Thu) by nybble41 (subscriber, #55106) [Link]

> People don't say that because C is not strongly typed.

Exactly. For example, C has implicit conversions between any two integer types, even when the conversion may lose information or lead to undefined behavior, a null value which can inhabit any pointer type, and implicit conversions to/from pointer-to-void. Java at least requires an explicit cast to narrow the type. It still suffers from the major weakness that null is treated as a valid reference value, and its implicit integer conversions can still lose information. They are both more strongly typed than, say, Perl or Bash, but even Java's type system is much weaker than Haskell's, or most of the ML family for that matter.

An interview with Joey Hess

Posted Feb 4, 2016 13:43 UTC (Thu) by dvandeun (guest, #24273) [Link]

You could say that the myth is partially true: it is very likely that a refactored Haskell program is correct as soon as you get it too compile (assuming that the original was correct), and that is thanks to type checking.