An interview with Joey Hess
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'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.
Posted Jan 20, 2016 0:00 UTC (Wed)
by Sesse (subscriber, #53779)
[Link] (4 responses)
/* Steinar */
Posted Jan 20, 2016 0:05 UTC (Wed)
by smoogen (subscriber, #97)
[Link]
Posted Jan 20, 2016 15:05 UTC (Wed)
by nybble41 (subscriber, #55106)
[Link]
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 {
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.
Posted Jan 28, 2016 12:00 UTC (Thu)
by HelloWorld (guest, #56129)
[Link] (1 responses)
Posted Jan 28, 2016 16:43 UTC (Thu)
by nybble41 (subscriber, #55106)
[Link]
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.
Posted Feb 4, 2016 13:43 UTC (Thu)
by dvandeun (guest, #24273)
[Link]
An interview with Joey Hess
An interview with Joey Hess
An interview with Joey Hess
SetState :: a -> StateA a ();
GetState :: StateA a a;
}
An interview with Joey Hess
An interview with Joey Hess
An interview with Joey Hess