I really think this way of thinking about static typing is a very bad thing. This is not at all an actual benefit, because in any sane situation, you will use unit and integration tests that execute extremely quickly on small test data to exercise your end to end model training code.
Unit and integration tests don't write themselves, and they will always be incomplete. You can't test for everything, and what you get from them will depend on how much effort you put in.
Static typing prevents you from running code that tells the computer to do nonsensical things, and usually you'll get an error that tells you exactly what you did wrong. I see those as benefits. In languages like Ocaml or Haskell that have type inference, type annotations can even be omitted most of the time. In the effort-versus-confidence trade-off, I see static typing as low effort with a good payoff. Others might think static typing is too much work and would rather rely on tests. Both approaches are complementary; neither renders the other unnecessary or redundant.
Turning it around to act like static typing is de facto always a benefit is a very one-sided way to look at it.
Sure, it's a trade-off. Opinions will always vary as to what an ideal productive development environment looks like and what trade-offs are worthwhile, but I think your dismissal of static typing as a tool for gaining some degree of confidence that some program will probably work correctly is also one-sided.
“You can’t test for everything” seems like a really bad counter argument in this case because you’ll still need to write the integration tests anyway, and if the tests are incomplete (which they always are, it’s life, whether you’re writing statically typed code or not, shrug), you have to improve the tests. You can still have runtime errors and incorrect logic in statically typed code... so?
Now if the process of that testing gets you 99% of the same overall job safety that you’d also get by increasing the code by 10% to add static typing annotations and data structure models (in addition to raising maintenance costs according to that 10% too, and possibly adding bugs or painting yourself into rigid, hard to refactor corners even if they confer some short term bug prevention benefit via the type checking), from tests you already need to write anyway, it’s a no-brainer.
I realize there are good uses of static typing and it can come down to style preference. But truly in this case of “what if my big scientific computing system hits a type-checking-could-prevent-it sort of bug after hours of computing time,” it’s just not a good argument.
This is why people routinely write huge scientific computing systems in Python and nobody ever worries that they hit type checking relevant errors after several hours.
Some things where type checking can really help: ensuring you’ve exhaustively handled every case in an ADT, using the type system to prove state transitions, like with phantom types, using the type system to encode side-effectfulness like Haskell monads.
These things often just aren’t important for something like a large-scale machine learning training program. The types of problems you run into just don’t happen to benefit much from that stuff, while the benefits you can get from writing quick ad hoc functions that can take arguments of unconstrained types and just make unchecked assumptions about their attributes is actually quite big.
“You can’t test for everything” seems like a really bad counter argument in this case because you’ll still need to write the integration tests anyway
Types are nothing more than a proof that some property holds for your code (Curry-Howard correspondence). Tests are nothing but a proof that the property holds for the exact conditions. Types are always better then tests, the only question is how powerful your type system is and how much properties you could express as types. In F* or Idris you don't need tests, in OCaml and Haskell you need tests sometimes, when type system is not powerful enough, in python you have to write tests all the time.
“Types are always better then tests, the only question is how powerful your type system is and how much properties you could express as types.”
Again, as I’ve been saying, that is a super one-sided way to look at it. Type annotations and the use of appropriate patterns required for most modern “good” static typing are costly things. Organizing things with type class patterns and algebraic data types costs you by making you write more code and more boilerplate, and have trickier things to reason about. Some languages are worse (Scala) about how bad this boilerplate affects you than others (Haskell), but the restrictions it places to facilitate the type-based proofs of safety are real. It’s not free.
Using static typing for these things is only better when (a) the overhead of adding static typing and associated pattern code (and associated maintenance of that extra code and restrictions of how you can write ad hoc code) is not too large and (b) the type-based safety proofs couldn’t have been gotten in some cheaper way.
In a case like a big model training program (a) and (b) just don’t hold. The extra boilerplate and maintenance is very meaningful. Just look at the difference between this blog post’s OCaml code and the equivalent stuff in Keras. The restrictions on ad hoc code also matter. If I can get back a dynamically typed container of settings, like a Python dict for passing into a GPUOptions setup in TensorFlow, and not bother needing to conform to certain types before being allowed to write code that just makes direct assumptions about what attributes I can access, or what dict values will be strings that can serve as args to functions expecting strings, ..., that just saves me lots of time and lets me write way shorter code, relatively speaking, because in this use case it is extremely easy to verify that the only types of data passed in will conform to the assumptions, something that can be checked with an integration test very quickly without requiring any compromise on the handling of arbitrary attributes from config dict values.
Not every case is like this. Some times going to the trouble of setting things up with static typing to prove complicated assumptions are valid within the code is better and ends up reducing code through disciplined use. Static typing can be cost-effective.
This particular use case in the blog post, though, is not one of those cases at all.
I don’t understand why you believe that question is rhetorically interesting or connected to anything that has been discussed.
You’d have to write virtually all the same tests in this type of use case whether you are using the static typing approach or not. The tests won’t explicitly check types in the dynamic typing case, but will verify type safety for fixture settings and data indirectly, as a byproduct of all the other testing.
It seems like you are really missing the point. In use cases like a big training program, you have to write integration tests, period. The compiler is not ever a useful substitute for that in this case. Now, since we know you have to use integration tests and so the cost of writing and maintaining those tests is baked in, we can ask: will those tests also cover what a compiler could have helped with, if we’re in the dynamic programming case? Yes.
And so then the extra code we’d have to maintain and extra constraints we’d have to live with if choosing static typing turn out not to buy us anything we can’t already get with the baked-in costs of the integration tests.
Tests don’t write themselves. Why would you ever ask that type of question like you’re being cheeky and rhetorically dramatic? It reveals that you’re still stuck imagining that you’d need to write extra type-specific tests in the dynamic typing case, which misses the point of the discussion.
You’d have to write virtually all the same tests in this type of use case whether you are using the static typing approach or not.
No, I don't need to write tests, it I could prove something with types. Here is an example of quicksort, where all invariants and properties are ensured with types, so this code does not need any tests at all.
Comments
Unit and integration tests don't write themselves, and they will always be incomplete. You can't test for everything, and what you get from them will depend on how much effort you put in.
Static typing prevents you from running code that tells the computer to do nonsensical things, and usually you'll get an error that tells you exactly what you did wrong. I see those as benefits. In languages like Ocaml or Haskell that have type inference, type annotations can even be omitted most of the time. In the effort-versus-confidence trade-off, I see static typing as low effort with a good payoff. Others might think static typing is too much work and would rather rely on tests. Both approaches are complementary; neither renders the other unnecessary or redundant.
Sure, it's a trade-off. Opinions will always vary as to what an ideal productive development environment looks like and what trade-offs are worthwhile, but I think your dismissal of static typing as a tool for gaining some degree of confidence that some program will probably work correctly is also one-sided.
“You can’t test for everything” seems like a really bad counter argument in this case because you’ll still need to write the integration tests anyway, and if the tests are incomplete (which they always are, it’s life, whether you’re writing statically typed code or not, shrug), you have to improve the tests. You can still have runtime errors and incorrect logic in statically typed code... so?
Now if the process of that testing gets you 99% of the same overall job safety that you’d also get by increasing the code by 10% to add static typing annotations and data structure models (in addition to raising maintenance costs according to that 10% too, and possibly adding bugs or painting yourself into rigid, hard to refactor corners even if they confer some short term bug prevention benefit via the type checking), from tests you already need to write anyway, it’s a no-brainer.
I realize there are good uses of static typing and it can come down to style preference. But truly in this case of “what if my big scientific computing system hits a type-checking-could-prevent-it sort of bug after hours of computing time,” it’s just not a good argument.
This is why people routinely write huge scientific computing systems in Python and nobody ever worries that they hit type checking relevant errors after several hours.
Some things where type checking can really help: ensuring you’ve exhaustively handled every case in an ADT, using the type system to prove state transitions, like with phantom types, using the type system to encode side-effectfulness like Haskell monads.
These things often just aren’t important for something like a large-scale machine learning training program. The types of problems you run into just don’t happen to benefit much from that stuff, while the benefits you can get from writing quick ad hoc functions that can take arguments of unconstrained types and just make unchecked assumptions about their attributes is actually quite big.
Types are nothing more than a proof that some property holds for your code (Curry-Howard correspondence). Tests are nothing but a proof that the property holds for the exact conditions. Types are always better then tests, the only question is how powerful your type system is and how much properties you could express as types. In F* or Idris you don't need tests, in OCaml and Haskell you need tests sometimes, when type system is not powerful enough, in python you have to write tests all the time.
Again, as I’ve been saying, that is a super one-sided way to look at it. Type annotations and the use of appropriate patterns required for most modern “good” static typing are costly things. Organizing things with type class patterns and algebraic data types costs you by making you write more code and more boilerplate, and have trickier things to reason about. Some languages are worse (Scala) about how bad this boilerplate affects you than others (Haskell), but the restrictions it places to facilitate the type-based proofs of safety are real. It’s not free.
Using static typing for these things is only better when (a) the overhead of adding static typing and associated pattern code (and associated maintenance of that extra code and restrictions of how you can write ad hoc code) is not too large and (b) the type-based safety proofs couldn’t have been gotten in some cheaper way.
In a case like a big model training program (a) and (b) just don’t hold. The extra boilerplate and maintenance is very meaningful. Just look at the difference between this blog post’s OCaml code and the equivalent stuff in Keras. The restrictions on ad hoc code also matter. If I can get back a dynamically typed container of settings, like a Python dict for passing into a GPUOptions setup in TensorFlow, and not bother needing to conform to certain types before being allowed to write code that just makes direct assumptions about what attributes I can access, or what dict values will be strings that can serve as args to functions expecting strings, ..., that just saves me lots of time and lets me write way shorter code, relatively speaking, because in this use case it is extremely easy to verify that the only types of data passed in will conform to the assumptions, something that can be checked with an integration test very quickly without requiring any compromise on the handling of arbitrary attributes from config dict values.
Not every case is like this. Some times going to the trouble of setting things up with static typing to prove complicated assumptions are valid within the code is better and ends up reducing code through disciplined use. Static typing can be cost-effective.
This particular use case in the blog post, though, is not one of those cases at all.
And tests are writing themselves for you?
I don’t understand why you believe that question is rhetorically interesting or connected to anything that has been discussed.
You’d have to write virtually all the same tests in this type of use case whether you are using the static typing approach or not. The tests won’t explicitly check types in the dynamic typing case, but will verify type safety for fixture settings and data indirectly, as a byproduct of all the other testing.
It seems like you are really missing the point. In use cases like a big training program, you have to write integration tests, period. The compiler is not ever a useful substitute for that in this case. Now, since we know you have to use integration tests and so the cost of writing and maintaining those tests is baked in, we can ask: will those tests also cover what a compiler could have helped with, if we’re in the dynamic programming case? Yes.
And so then the extra code we’d have to maintain and extra constraints we’d have to live with if choosing static typing turn out not to buy us anything we can’t already get with the baked-in costs of the integration tests.
Tests don’t write themselves. Why would you ever ask that type of question like you’re being cheeky and rhetorically dramatic? It reveals that you’re still stuck imagining that you’d need to write extra type-specific tests in the dynamic typing case, which misses the point of the discussion.
No, I don't need to write tests, it I could prove something with types. Here is an example of quicksort, where all invariants and properties are ensured with types, so this code does not need any tests at all.
https://github.com/FStarLang/FStar/blob/master/examples/algo...
You could reason about your program's correctness on any level with types.