> The dynamic world lets us have inconsistent code that partially works
This is precisely why I have nightmares about refactoring dynamic codebases.
This is precisely why I have nightmares about refactoring dynamic codebases.
Static type checking generally represents an even lower form of error detection than functional and unit testing does. Sure, it can be convenient to have it, but lately I see a lot of static language novices around here talking about their recent and limited experience with type checking as if they are suddenly experts in the tradeoffs between static and dynamic languages.
So generally, the more invariants you manage to capture in your types, the more categories of bugs you can statically prove will never happen.
That isn't true. Static typing offers machine checked proofs of the absence of a whole class of trivial errors; and potentially any invariants you've managed to teach it.
My point was that testing does not negate the need for static types, as implied by the previous poster.
Claim: "Getting vaccinated stops a whole class of diseases which might kill you"
Your rebuttal: Although "class" sounds big, in fact there are only a countable number of viruses that vaccines save you from. The number of ways in which you can die is astronomical.
In the above analogy, as in your original statement, you're completely missing the point that the class of errors / class of diseases is an important class and easily preventable, therefore you should do it.
In fact, I think what you've said is the reverse of true. Static typing means that there's a chance of an error at each node in the program's tree because a statically typed and statically compiled language ensures that the program can be rendered as an AST before you ship it to your user.
A dynamically typed interpreted language can have an error at literally any character in the entire thing, and you don't have "compile-time" to tell you it's not an error.
The class of errors that you're saving yourself from is "every single character of this program could be wrong in a way that results in it not even being representable as an AST; there are astronomically many ways that can occur".
In addition, it now goes wrong much later. You have to ensure that you've hit every path with testing before you can be even somewhat confident it's valid code, let alone logically correct and bug-free in other ways. A compiled statically-typed language you waste no more time than a compile-cycle to get that minimal assurance.
Claim: "Using a plastic liner stops urine from getting into the mattress".
My rebuttal: "That's well and good, but I'm sure I didn't wet my bed past the age of three."
Source: I'm typing this from a bed I'm sharing with an infant.
(I don't actually mean this to be an argument, just fun. "Other people will make type errors" is not the argument I'd make.)
The number of possible programs is astronomical (though still countable!). The number of possible programs with the correct type is substantially smaller. If we can construct our types and type checking such that the errors we are likely to make are likely to result in ill-typed programs, then we can substantially reduce the number of uncaught errors.
More generally, in your comparison you seem to be expecting that a unique error be detected in a unique place. There is no particular reason multiple (or manifold) errors should not be expected to produce an error in the same "nodes in the program's tree".
Agreed!
> But rather this: let's take a correct program of size N (N nodes in the syntax tree) and insert a single error into it and give the modified program to someone to find the error (without giving them the original, of course).
I think that's a good approximation. There is some additional structure it discards; I care most about errors that people are likely to make, and about surfacing changes required in likely refactoring. But I expect something that does well at the one is likely to do well enough at the other.
> If it's a type error, it can be found by searching the space of N nodes. If it can be any defect whatsoever, the search space is the entire state space of the program emanating from all combinations of all possible inputs.
Which is exactly why we want to make as many errors "type errors" as possible (modulo tradeoffs). We'd much, much rather search that smaller space.
You certainly don't need to write tests that Math.floor will return NaN when you pass it something that's not a number...
A floor function that returns NaN when given a string, instead of throwing a type mismatch exception, is crap design, and a strawman example of that type of checking. It's not an appropriate use of NaN!
Static typing, by contrast, covers all type errors, which can take care of quite a bit if you know how to use the type system to your advantage. On top of that, if you don't rely on a refactoring tool (which I recommend avoiding for anything non-trivial) then the compiler will guide you to all the spots where that type is being used, which gives you an opportunity to re-evaluate the correctness of the code that uses it.
Is it more work? Yes. Is that a bad thing? Many would argue it's a good thing.
I personally don't feel that the benefits outweigh the cost; namely that I have to babysit a compiler and stop development while I fix compiler errors that are irrelevant to the thing I'm working (if I'm working on widget A and I broke widget B by changing a type, I don't want to fix widget B right now).
If a feature is better implemented after a certain refactoring, then you can do that at the same time locally but still separate it out into different commits.
You don't want to stop and fix "unrelated" errors, but if B was broken by a type change in A then it is almost certain that B is affected by the changes in A. Right now, when you are making the changes in A, is the best time to address the fallout, because you have the reason for the change and all its subtleties in mind.
The vast majority of the bugs my team addressed after our last major refactor in our Node codebase were of this kind: either completely forgotten or unknown components affected, or fixes that were not fully aware of the changes made. Knowing at the time of the change all of the places that change affects is extremely powerful. Tests only get you this for the easy cases you've thought of. Static typing doesn't get you that entirely, but it gets you a lot closer than dynamic typing.
So I'd argue the opposite. Dynamic languages taught me to fear refactoring because they're is always the danger that you missed something buried somewhere that will come back to bite you in really subtle ways. I never get the satisfying feeling of unifying the code under a new logical consistency because there may still be these loose ends lurking around.
Normal Devs write mediocre tests on a good day. You will find a significant percent that assert nothing or are tautological. Then when your requirements change or you are refactoring you will find that we have tested the implementation and made really unfortunate assumptions.
If you invite everyone to join you, a lot of the things you hold dear will get lost. It's super frustrating to have to trust people who can't be.
I worked with static languages for a long time, and I have been doing test automation for a long time (10 years). There are many things I understand about writing good tests, many of them counterintuitive things, including some big mistakes everyone seems to have to experience to believe.
I can't articulate it yet, I'm still processing, but recently some of the classes of error I'm finding in my and other's tests have convinced me that tests can't practically and efficiently verify everything important, and that maybe testing in this way and to this extent isn't the solution we need.
Often what makes a good test is contrary to how we write production code. Testing well is pretty damned hard for people. And I now despair of ever convincing the hoi polloi not to eagerly paint us into corners.
For instance, consider a function which calculates the GCD of two integers. Everything in that function is an integer. Your compiler tests it for you: nope, no strings or floats in there: nothing but integers, check!
It's basically one test, and it has nothing to do with whether that function calculates the GCD correctly. It will pass even if that function calculates the LCM due to misunderstood requirements.
[0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...
Agreed.
Granted it's not enormous, but if you think it's trivial you'll probably be surprised by the range of things you can encode in the Haskell type system.
Ordinary code does not encode very interesting things about itself via its typing. Well typed usually just means "there is no trivial mistake here", on about the same level as a missing semicolon in a C struct declaration.
I have some interest in types (mostly practical, some theoretical) but I have no graduate degree, I still regularly encounter both theory and type voodoo I don't understand, and I wouldn't consider myself a "type system expert".
On a recent project I was able to use the type checker to help me catch things including 1) passing a bid price where I meant an ask price, 2) using an index into the wrong array, 3) calling a function not permitted to run on the thread in question (because of data access or deliberate marking).
This wasn't Haskell - it was C.