Hasn't this long been settled? See e.g. https://www.destroyallsoftware.com/talks/ideology . Spoiler alert: We need both.
The article was published three years before this talk.
Analysis of whether unit testing obviates static type checking (2012)
21–30 of 65 posts
Re: Analysis of whether unit testing obviates static type checking (2012)
#22The answer is yes, obviously, due to the Curry-Howard isomorphism. Likewise static type checking obviates unit testing. Granted, most static type systems aren’t Turing complete so there are some assertions that can’t be made at the type level that can be made at the unit test level, however there are absolutely a handful of languages with type systems that are. Indeed, any language with first-class functions can implement runtime type checking via higher-order predicates and thus obviate the need for unit tests. Is this news?
Re: Analysis of whether unit testing obviates static type checking (2012)
#23The better the type system is, the more bugs it prevents, so one has to spend less time unit testing. Sadly, it also means the language is harder to learn, so the rest of us are stuck with horrible, unsafe languages.
This hasn't exactly been my experience, Python isn't easier to learn than e.g. Java because of the lack of static typing, it's easier because the language is more expressive. I actually think there is literally no downside to making typing opt out rather than opt in - beginners benefit from the compiler saying they accidentally swapped two arguments around - how could they not? I have helped beginners with untyped Py…
The downside is increased short-term dev time and code, and thus increasing rigidity of the code. In most cases this tradeoff is still worth it, but sometimes speed and flexibility is a higher priority, hence why I prefer opt-in
Re: Analysis of whether unit testing obviates static type checking (2012)
#24Type checking allows the compiler to prove certain properties hold for your code, and so this can be used to catch certain classes of bugs. Unit tests don't have that power. But which classes of bugs are caught depends on the type system. Not all type systems are the same. In most statically typed languages, division is not total, and so a function using division can type check, but also crash the program at runtime. In such cases, unit tests can complement types, so you can profit from both. Furthermore, in most languages, the type system is too coarse to prove the sort of correctness that unit tests try to corroborate. If types are a specification, then a sorting function with the type signature `[Int] -> [Int]` doesn't tell us much. There are, in principle, an infinite number of functions that have that type, most of which are not sorting functions. Unit tests can give us some modest, practical confidence of correctness that such a type system cannot. On the other hand, dependent types do permit us to construct return types that guarantee that some ordering relation holds, so it is possible to make the specification more precise in such cases. Such precision may not always be economical or easy to achieve, however. Type inference can assist us in this task, though.
But one of the aspects of types that I find useful is the documentation they provide. In a dynamic language, you often have to guess what the types of functions are by reading the implementation, and not just of the function in question, but the functions composing that function. As a code base grows in size, this can become annoying. With code base size, modularity becomes increasingly important, and modularity benefits greatly from clearly defined and stable interfaces. Also, types can enable something like LSP to make suggestions about what can appear in a given place. With type inference, this can be quite powerful, allowing you to build code in an interactive fashion (proof assistants make use of this behavior).
Unit tests can also provide value as documentation, in the sense that they can function as tested and working examples of, say, how a library could be used.
So, in other words, both types and unit tests have value, and the value they offer will vary depending on the type system and how types are being leveraged in a given situation. There exists an overlap in the practical value provided by types and by unit tests, and where there is overlap, I would say types have the upper hand in principle, if not always in practice.
Re: Analysis of whether unit testing obviates static type checking (2012)
#25Original title: Unit testing isn't enough. You need static typing too. From 2012.
Not that unit testing is enough, but the unit testing that these projects happened to do isn't enough. I suggest that testing that's enough to have confidence that a non-trivial program is correct is going to cover just about everything static type checking could find as well (except in dead code, and how does that matter?) Or, to put it another way, if you didn't care enough about the correctness of your code to tes…
> if you didn't care enough about the correctness of your code to test it adequately, why would you care that static type checking could find some bugs?
I think you got this backwards. If you didn't care enough about the correctness of your code to even do something as simple and straightforward as using a proper type system, why would you spend enormous amount of time to write and then support unit tests just so that they could find some bugs?
Re: Analysis of whether unit testing obviates static type checking (2012)
#26The better the type system is, the more bugs it prevents, so one has to spend less time unit testing. Sadly, it also means the language is harder to learn, so the rest of us are stuck with horrible, unsafe languages.
This hasn't exactly been my experience, Python isn't easier to learn than e.g. Java because of the lack of static typing, it's easier because the language is more expressive. I actually think there is literally no downside to making typing opt out rather than opt in - beginners benefit from the compiler saying they accidentally swapped two arguments around - how could they not? I have helped beginners with untyped Py…
Anecdotally as someone who writes a lot of Typescript - which has a very expressive type system, most of the time when I need to help someone who's "fighting" with the type system the issue is that they've written a bug but the error message just isn't particularly clear. Which is loads better than them writing a bug and then only discovering it in production.
Mentally parsing the type errors is an art though - generally you want to ignore pretty much all but the bottom 1 or 2 lines - the rest is a bunch of very verbose information at a much higher level of abstraction than you care about.
Re: Analysis of whether unit testing obviates static type checking (2012)
#27Type checking allows the compiler to prove certain properties hold for your code, and so this can be used to catch certain classes of bugs. Unit tests don't have that power. But which classes of bugs are caught depends on the type system. Not all type systems are the same. In most statically typed languages, division is not total, and so a function using division can type check, but also crash the program at runtime.…
> But one of the aspects of types that I find useful is the documentation they provide.
For me this is one of the core aspects. Self-documenting code makes me so much more productive, and being able to reason about code thanks to the types without having to consult the documentation is very powerful.
Any time I work with JavaScript, Python or similar I invariably waste time having to do print(dir(foo)) or similar, just to figure out what the hell some function returned and what I can do with it.
Re: Analysis of whether unit testing obviates static type checking (2012)
#28Earlier quoted context omitted.
This hasn't exactly been my experience, Python isn't easier to learn than e.g. Java because of the lack of static typing, it's easier because the language is more expressive. I actually think there is literally no downside to making typing opt out rather than opt in - beginners benefit from the compiler saying they accidentally swapped two arguments around - how could they not? I have helped beginners with untyped Py…
Anecdotally as someone who writes a lot of Typescript - which has a very expressive type system, most of the time when I need to help someone who's "fighting" with the type system the issue is that they've written a bug but the error message just isn't particularly clear. Which is loads better than them writing a bug and then only discovering it in production. Mentally parsing the type errors is an art though - gener…
This exactly… I’ve had several devs come to me with things like “react won’t let me do this” … which is really typescript and really it’s that they are doing something wrong in any lang and it is just good news that the type system caught it
Re: Analysis of whether unit testing obviates static type checking (2012)
#29The answer is yes, obviously, due to the Curry-Howard isomorphism. Likewise static type checking obviates unit testing. Granted, most static type systems aren’t Turing complete so there are some assertions that can’t be made at the type level that can be made at the unit test level, however there are absolutely a handful of languages with type systems that are. Indeed, any language with first-class functions can impl…
Static typing, short of dependent types (and even then you have to use them to their full extent), does not obviate any form of testing unless your programs are trivial. For any non-trivial program, testing is still needed unless you're going to go through formal proofs (which could be embedded into dependent type systems). Otherwise, you can have something which type checks but which still contains logical errors.
Re: Analysis of whether unit testing obviates static type checking (2012)
#30Type checking allows the compiler to prove certain properties hold for your code, and so this can be used to catch certain classes of bugs. Unit tests don't have that power. But which classes of bugs are caught depends on the type system. Not all type systems are the same. In most statically typed languages, division is not total, and so a function using division can type check, but also crash the program at runtime.…
This is the most well thought out commentary on this topic I have ever read. Thank you.