LWN: Comments on "An interview with Joey Hess"

An interview with Joey Hess

dvandeun — Thu, 04 Feb 2016 13:43:53 +0000

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.

An interview with Joey Hess

nybble41 — Thu, 28 Jan 2016 16:43:41 +0000

> 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

HelloWorld — Thu, 28 Jan 2016 12:00:02 +0000

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

oever — Thu, 21 Jan 2016 22:36:22 +0000

be able to branch and merge at the distro level

I did not look at it in those terms, but mostly it is true. NixOS allows branching at almost the distribution level. Every distribution can be branched — look at the distribution family tree — but in Nix(OS) you can install packages which differ from the main system, even starting at libc, by just forking the NixPkgs repo. And switching between the branches is easy without rebooting or logging out.

An interview with Joey Hess

yxejamir — Thu, 21 Jan 2016 16:46:24 +0000

My best idea, mostly untried, is to be able to branch and merge at the distro level:

More people need to start looking into distros like GuixSD and NixOS, where one can do exactly that. Everyone should be moving in that direction, especially anyone who is currently using the likes of Puppet and SaltStack for configuration management.

An interview with Joey Hess

bytelicker — Thu, 21 Jan 2016 14:57:25 +0000

Great interview!

I really like the part were Joey talks about being away from the "big city". I'd like to retire early and move to the woods.

An interview with Joey Hess

nybble41 — Wed, 20 Jan 2016 15:05:27 +0000

"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

smoogen — Wed, 20 Jan 2016 00:05:49 +0000

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

Sesse — Wed, 20 Jan 2016 00:00:14 +0000

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

smoogen — Tue, 19 Jan 2016 23:24:43 +0000

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.