Statically-typed functional languages…have a property that exists almost nowhere else: once it compiles, it usually works first try.
— Real problems with functional languages, and their influence on Dark
This is a claim I hear from time to time about statically-typed functional languages. It sounds appealing—suspiciously appealing. Can it be possible that a compiler can ensure that a program is error-free?
Say we’ve written a function that takes an array of integers, performs a calculation using them, and returns the resulting integer. It’s a pure function so it has no side effects. A statically-typed language will ensure we do in fact return an integer, that we don’t try to perform any operations on integers that only apply to floats, and probably that we handle any possibility of missing/null values.
Does that mean the function “works”? That it is “correct”? Well, that depends on the intent of the function. Most likely we care about the specific integer that’s returned; for example, we probably don’t want it to always be 13. And in my admittedly-limited experience, it doesn’t seem to usually be argued that a static type system can enforce that the calculations in a function are what is intended. (Idris seems to be an interesting exception, with types predicated on values. I would be surprised if its type system can cover all calculations. And in any case the languages I hear “if it compiles it works” argued for don’t have types predicated on values.)
So if a function is intended to perform a certain computation based on the inputs, but instead it returns any incorrect value—whether a hard-coded 13 or a subtly-wrong value—I think it’s a stretch of most normal use of the words to say that that function “works” or is “correct”.
Let’s look at another example. Say you have a stock-trading application. It has a function recommendBuy() that takes some inputs and recommends a company whose stock you should buy. One day, users report that your function recommended they buy stock from company that was clearly seen at the time to be rapidly losing value, and has continued to do so. To these users, it will be little consolation if you say that your program “works” because recommendBuy() returned a company structure and not a JPEG image!
So it seems like the phrase “when the program compiles, it usually works” can’t mean what it sounds like it on its face for all applications all the time. What can it mean, then, and for which programs?
- Maybe the programs this phrase applies to have only trivial calculations. In such a domain, the vast majority of application errors would likely come from mistakes wiring the program together; the calculations themselves would in practice almost never be wrong. In such a program, if the types are consistent, the program is most likely correct. (Of course this program’s correctness can’t be guaranteed, as it would be easy to produce an example of a program that returns incorrect values of the correct type.) If this is the situation, the phrase “when it compiles it works” isn’t intended to mean “when any program written in this language compiles, it’s usually correct.” It might be clearer to say “in this language, if a program with simple calculations compiles, then it’s usually correct.”
- Maybe in this phrase the terms “correctness” and “works” are being used in a more technical sense that is typical. Maybe the definition of “correctness” is precisely “does not have any type/null-pointer/no-method/unhandled-error issues.” But if this is the case then the statement “when it compiles, it works” is much more limited than it might first seem: effectively it means “when it compiles it does not contain type errors.” This guarantee does have real advantages; it’s just not as extensive as the phrase “when it compiles, it works” suggests. When speaking to people who don’t already share the speaker’s definition of “working” and “correctness,” it’s probably best to clarify that meaning to avoid misleading. Speaking of misleading…
- Marketing. Maybe for some folks the phrase “when it compiles it works” isn’t intended to be precise; it’s intended to generate interest in statically-typed languages. It’s over-the-top, but if the phrase raises awareness of statically-typed languages then people will benefit from the lesser guarantees they do offer. If someone is using the phrase in this misleading way then it would be easy for me to throw stones, but I should be careful—I expect that when it comes to my preferred languages I probably tolerate hyperbole for the sake of marketing as well.
I’m sure in some future project I’ll get to use a statically-typed functional language in more depth, but right now I’m not feeling a particular draw to look into them. And one thing that isn’t a motivator to do so is insufficiently nuanced statements like these. I hope I’d be motivated by a more precise statement about which kinds of programs derive which level of benefit from static types. Maybe I’m overly optimistic about my openness. Even if so, I’d love to hear those more precise statements so I could get proven wrong!