Ask HN: A well-typed program won't go wrong? | Hacker News Reader

Ask HN: A well-typed program won't go wrong?

4 pointsAnimalMuppet13 comments

I've read a few times here on HN the saying "a well-typed program won't go wrong" or some slight variation. I don't think that can be correct, so I'm going to state my objection, and see if I'm right, or if someone can educate me.

Let's say I'm writing a recursive factorial function in Haskell. But, because it's early morning and the caffeine hasn't kicked in yet, I mess up the recursive call. I say "+ 1" instead of "- 1".

What is Haskell's type system going to say about this mistake? I believe it will say nothing at all, because the problem isn't the type of the value, it's the value of the value. But what's the program going to do? It's going to run until it exhausts memory, and then it's going to die in disgrace.

It seems to me that there are only four possibilities here:

1. Haskell's type system can in fact catch this error at compile time.

2. Despite its celebrated type system, Haskell is not a sufficient base for building a well-typed program, but some other language would be. (Coq? Agda? Some not-yet-existent language?)

3. Dying in disgrace rather than returning the correct value does not count as "going wrong".

4. The statement "a well-typed program won't go wrong" is false.

Of those options, I believe that number 4 is correct, but I am willing to listen to reasoned arguments to the contrary.

OK, let's knock this on the head very quickly please and avoid a flamefest.

According to "Generalized Arrows"[1] by Adam Megacz Joseph the slogan "Well typed programs do not go wrong" was coined by type theorist Robin Milner and means something very specific: 'To "go wrong" means to exhibit undefined behavior. For example, programs written in strongly statically typed programming languages cannot crash, write to random memory locations, or read past the end of a buffer.' If you want precise details please read Milner's "A Theory of Type Polymorphism in Programming"[2].

Note that this does not imply that well typed functional programs do not contain bugs. Futhermore it only applies to a very specific ML-like language with a precisely defined denotational semantics. It is not known to apply to Haskell as no one has even written down the denotational semantics for Haskell. Furthermore it is trivially easy to write crashing programs in most Haskell implementations by taking advantage of any of a variety of non-standard features and functions.

Please let us not build up and knock down straw men about Haskell claiming to prevent all bugs.

[1] http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-13...

[2] http://tfeng.me/papers/milner78theory.pdf

Then does ML's type system detect my "+ 1" error? Or does ML not crash once memory is exhausted? Or does "crash" in your second paragraph really mean "crash due to reading an invalid memory location"? (I'm not trying to be argumentative here; I'm trying to understand. I don't understand ML well enough to answer my questions.)

I accept Milner's claim, with his definition of "go wrong". The problem then becomes that people repeat the claim, but not the definition, and so people like me hear the claim, don't know the technical definition of "go wrong", and assume that the general meaning of the words is being used.

If people are saying "well typed programs don't go wrong" to mean something other than the precise technical statement then you or I will have to correct them. However you will have to point me to some examples first. I couldn't find any.

A well-typed program is isomorphic to a proof -- google "propositions as types". This is not the same as saying your program is correct.

For your specific question, google "dependent types", which are types that depend on a value.

In your case, Haskell can type check positive integers:

http://mvanier.livejournal.com/3820.html

I think at least 3, and maybe all four, are true from various perspectives:

1. I think that the scenario here is one that Haskell can type check, though it takes some work. But I'm not sure.

2. Haskell's type system is better than many, but limited. Coq/Agda/Idris are more powerful.

3. One common definition of "going wrong" is "returning an incorrect answer". Crashing isn't going wrong in that framework. (I don't necessarily agree with it, though I've seen it; at any rate, there is a good reason to think that crashing is a lesser problem than executing and returning incorrect results.)

4. While there may be definitions of "well-typed programs" and "go wrong" for which this is true, ISTR that they are either ones which make it so that a type system that completely supports general computation is not possible, or ones ones which require excluding a lot of errors from "going wrong".

Whenever I read an argument online about any subject, I always mentally replace "X won't do Y" with "X has a smaller chance of doing Y". Being overly pedantic has never helped me at all.

A wise policy.

I don't know what "well typed" means, but I assume you mean something like "correct use of the type system". If so, then 4 is "correct" in the sense that the type system eliminates or mitigates certain categories of programming errors, but not all categories of errors.

FWIW, I don't know Haskell, but off the top of my head in Ada if I couldn't use a subrange type, I might use a Contract (Pre or Post condition) to insure I was iterating correctly, if I thought to include one without appropriate caffenation.

    > I've read a few times here on HN the saying
    > "a well-typed program won't go wrong" or some
    > slight variation.

Actually, I don't remember seeing that stated here on HN. Could you provide some references? I don't know anyone who says that. Seriously strict typing can prevent certain types of errors, and can ensure that the code runs. But if I implement quicksort when I intended to implement heapsort, how can typing help?

No, I can't give references. I recall seeing that claim at least twice in the last six months or so, but that's a wide area to search. (And, not having references, I can't be sure whether it was the same person making the claim each time.)

OK, fair enough. In any field there are people who make extravagant claims with no evidence, based purely on their own enthusiasms(+). I believe, in this case, and in agreement with other commenters, that the claim is wrong.

(+) Probably including this one.

There are a few people discussing or mentioning the phrase, but I didn't find anyone actually making the claim.

https://www.google.com/search?q=a+well-typed+program+won't+g...

#4 is correct.

In terms of reducing errors, Haskell goes a long way, but it does not eliminate all errors.

Reply on news.ycombinator.com