Informative article but I take issue with the following:
'It doesn't make sense to do the same kinds of exhaustive unit testing in Haskell as you'd do in Ruby or Smalltalk. It's a waste of time. It's interesting to note that the whole TDD movement comes from people who are working in dynamically typed languages.'
Unit testing in dynamically typed languages serves two purposes: 1) to prove code correctness, and 2) to prove code soundness/completeness, to show that the result of a function is correct for most or all input parameters. In statically typed languages 1) is already taken care of by the type system. If your code compiles then there are no glaring type errors in it and your code is correct. However, you still have #2 to worry about.
I work in Scala a lot where there is a static type system. I still have extensive unit tests, and I can't tell you how many times it's saved me when I've changed code in one area of the codebase, thought it was sound and complete, and then immediately become informed it's caused tests to fail, even though it compiled correctly. For instance I'll change code in a model and think that the controller will still behave the same way - and unit testing demonstrates immediately that it doesn't. This is especially true when I didn't write the controller that depends on the model. Testing also helps you rigorously test corner cases - when does this code throw an exception, when does it return a negative number, etc.? It really helps you get a good sense of when a piece of code is done, and move onto the next code.
Unit testing is indispensible both in static and dynamically typed languages, and I don't think lots of coverage is a waste of time in static languages.
If you have proven your code correct, it doesn't matter what language it is in or whether it has a type system at all. Proven correct in the absence of a type system is proven correct.
Any of the model checking methods (abstract interpretation etc.). The real life example I like to give is the detection (and correction) a few months ago of the bug in TimSort, possibly the most widely used sorting algorithm in the world (since its inclusion in Java in 2011). It was found using symbolic execution, and I'd like to see a programming language that is able to both express the algorithm in its efficient form (it is only used because of its speed) and prove its correctness using the type system in a way that is any easier than how it was actually verified.
If you stretch the definition of type a bit, any expressible property of your program (such as "this function sorts list") is a type and anything that allows you to automatically prove those properties is a type checker.
Agreed. It's more of a gradual transition towards fewer tests. The more constraints about the system you push into the type system, the less you need to test, hence the dream of dependent types etc etc. You still want to have sanity checks in place in case your constraints make no sense, even if they're being correctly imposed.
The point is that a lot of tests which are necessary in Ruby/Python are unnecessary in Scala. For example:
assert(len(f(x)) > 0)
In Scala, you just have `def f(x: X): NonEmptyList[Y]`.
Or a more complicated example that I've run into recently. You have a set of predicates, some of which can be evaluated in the browser, some not - e.g. IsFirefox & EverVisitedUrl(url). You then (server side) evaluate EverVisitedUrl(url), get a partial result IsFirefox & True = IsFirefox, and then push whatever is left to javascript `isBrowserFirefox()`.
In python/ruby/etc, you'd need extensive tests to make sure this translation is properly handled. In Scala, if your function doesn't have type `FreeBool[ArbitraryPredicate] => FreeBool[JavascriptEvaluatablePredicate]`, your code won't compile.
I think a lot of static-language people assume that dynamic-language people write a lot of type-assertion statements in their code and then write a lot of tests to ensure those assertions hold.
With a suitably enlarged definition of (static) type, a lot of tests become type-assertions.
Eg red black trees have interesting balancing requirements: no t
See eg Red Black Trees are another interesting example. A red black tree is a binary search tree, and all its nodes are coloured either red or black. You can not have two red nodes in a row on any path, but all paths from root to any leave have to have the same number of black nodes.
Testing that these two properties hold after an arbitrary number of inserts sounds like a good candidate for a unit tests, and doesn't sound like a type assertion, does it?
In any case, Haskell has great support for unit tests, too. (Because in general you can't and at any rate don't want to encode everything you care about in the type system.)
Have a look at QuickCheck. There are ports for various other languages, too. QuickCheck is a generalization of the table-driven approach to unit-testing: it's about generating those tables automatically, and automatically simplifying any inputs found that lead to buggy behaviour.
I'm as much a dynamic language person as a static language person - I write as much python as I do Scala. The point is that the guarantees you can get go well beyond simply assert(type(x) == str). See the examples in my previous post - you can guarantee at the type level that a list isn't empty, or that a boolean formula only contains predicates that can be rendered to javascript.
Unit tests almost never prove correctness or completeness. For a non-trivial program, the best you can hope to demonstrate is correctness for the arguments tested in the state determined by the test environment. If you want to prove correctness, you need proofs.
By and large, unit tests exist to quickly find bugs.
As I like to put it: unit tests don't affirm the correctness of code with respect to a specification, they merely affirm that certain implications of the specification hold with the code under test. In that sense, the general tendency to assume correctness in the face of passing test suite is basically an instance affirming the consequent on a huge scale.
The key is "the same kind of exhaustive unit testing". Unit tests can serve many purposes, in terms of raising your confidence that code is correct. In a language with minimal static type checking, a big part of what a good unit test suite will be doing is checking type invariants. In a language where those type invariants are checked for you, you don't need those particular unit tests.
Upon revisiting the article, I am downvoting your comment. Your objection is addressed in the very passage you cite, you merely truncated it misleadingly (and incorrectly - changes made to a quote should be placed in square brackets, and a move from an ellipsis to a period is a change). The truncated portion reads:
"It's interesting to note that the whole TDD movement comes from people who are working in dynamically typed languages... I'm not saying that unit testing is a bad idea with static types; only that it's entirely appropriate to scale it back a little.)"
What is the difference between "code correctness" and "to show that the result of a function is correct for all input parameters"? In common parlance these are the same thing.
Also, what does it even mean for a piece of code to be sound or complete? Sound with respect to what? Complete with respect to or relative to what?
I think the words that you want are "correct wrt a specification" instead of sound and "total" instead of complete?
Testing cannot prove correctness, period. The proof is a set of unit tests that cover every single input and also a proof that the set of inputs you tested is the entire domain. Basically no in-the-wild unit testing does even the former.
What you mean to say, I think, is, "testing is indispensable when your specification language isn't sufficient for specifying all correctness properties for your code."
Which is about right, but the way that you worded this post was extraordinarily confusing.
Thanks for posting this, I was thinking about this topic recently while at Angular U Conference and seeing how TypeScript is becoming the de facto language in that community for Angular 2 development.
Claim: Dynamic and static type systems are two completely different things, whose goals happen to partially overlap.
Immediately contradicted: A static type system is a mechanism by which a compiler examines source code and assigns labels (called "types") to pieces of the syntax, and then uses them to infer something about the program's behavior.
This is possible to do with a program that is understood as being dynamically typed.
Moreover, whenever a type can be assigned to a piece of syntax, it will agree with the dynamic type.
"For most computing environments, performance is the problem of two decades ago."
I've been hearing that performance isn't a problem for the last 20 years, yet it seems like I still spend a lot of time waiting for computers and devices to respond. I've worked in mobile and embedded (arguably not a small segment) for a while, and every major product I've released has had a last minute optimization scramble. The growth of these spaces (and now wearable devices) is only making this worse.
>On the other hand, there are a few environments where performance still matters. Languages in use there are rarely dynamically typed, but I'm not interested enough in them to care much.
Well considering Rust I'm guessing Mr K might have different views now.
This article wasn't written by Steve Klabnik — merely "reprinted".
> Recently, it was brought up on Proggit that Chris Smith's "What to Know Before Debating Type Systems" was no longer online. This is a really great article, and in an effort to make sure it survives, I've grabbed the archive.org cache and am 'reprinting' it here. If you're into programming languages, read this and level up!
Have you done any Android development? Do you have any confidence that Android isn't held together with duct tape and baling wire under the hood? I sure don't.
I think perceived performance problems of today are caused by the incremental evolution of legacy systems leading to rube goldberg machines, not due to how fast a programming language can execute.
Sure, for example, HTML app performance is often constrained more by layout and DOM manipulation than straight line code execution.
On the other hand, a lot of these systems aren't that old. I don't think Android is a Rube Goldberg pile of legacy. But Google acquired a company to get the V8 JS interpreter team for WebKit/Blink, and the Android team just created ART to replace Dalvik. These are smart people who've done a lot of performance measurement and optimization. If the VM didn't matter, it seems like a lot of money and time spent for nothing, right?
From a theoretical perspective, preventing infinite loops is in a very deep sense the most basic possible thing you can do with static types! The simply-typed lambda calculus, on which all other type systems are based, proves that programs terminate in a finite amount of time.
Is this not claiming that static typing (and/or lambda calculus) solves the halting problem?
Far from it; rather, that the simply typed lambda calculus is not Turing complete. One cannot represent a Turing machine in the simply typed lambda calculus, exactly because non terminating programs cannot be expressed.
One can add a fix point to the calculus (such as the titular Y combinator), but that introduces inconsistency to the type system.
What is actually happening here is not quite what you think. There is a subset of programs for which you can prove it halts, notably lower-bounded by e.g. Idris' totality checker (which is a part of its type system).
No. Rather, some typed variants of the lambda calculus are not Turing-complete. They prevent infinite loops without running into the halting problem by being strictly less powerful than normal programming langauges.
It's worth noting that this is not an either/or problem. Some modern dependently typed languages take a more nuanced approach: they have a less-powerful core with enforced termination¹ and a way to write potentially non-terminating code that's isolated from everything else by the type system. It's the same approach that Haskell uses successfully for IO—it allows IO, but only in a controlled and explicitly delimited part of the program.
In a very real sense, we can treat potential non-termination as yet another effect and manage it accordingly.
¹ Actually, they're even more nuanced than this: programs either have to provably terminate or be provably "productive", which means they produce some new output from new input in finite time. This allows languages to support beneficial infinite loops like the event loop in an operating system while preventing purely harmful busy loops that never get anywhere.
"One reason is that the average skill level of programmers who know Ruby is higher than those who know Java, for example."
Had to double check the year on this one. Things must certainly have changed... For instance, Java is a staple of most CS curriculum. If not Java then often Python. /Never/ have I heard of Ruby being the primary language of choice by a CS department. (Nothing against Ruby, just an observation.)
On the other hand, what is the most popular language/framework for a beginning programmer to learn today? Ruby/Rails or Node? Whereas Java is the quintessential Corporate language.
I'm obviously making some generalizations here. But things certainly seemed to have changed a lot!
Certainly! I noticed is assertion and was confused - until I checked the year. Then I listed some of the points relating to my confusion. What is apparent is that I am just missing some historical context. At some point, as the author asserts, Ruby appears to have been a more academic/corporate(?) language than Java. I did not know that.
1. This debate is not (or no longer) binary. There is a whole spectrum of static typing richness, from dynamic typing to well beyond Idris. The debate, then, is not whether we should be at any of the extreme, but where along the spectrum (including, maybe, the extremes). The interesting question to pose to proponents of very rich type systems, then, is "should we always use the richest type system possible?", and if not, why not? The whole debate -- which, again, is not binary -- hides in two of the questions the author lists in the end: "How easy can it be made to program in a language... ?" Nobody argues that the richer the type system the more properties can be proven (except for one major caveat I mention in item 3). The debate isn't about what character strings containing programs can be rejected or accepted. Programming language design is 5% theory and 100% psychology. What string the compiler accepts is a question for PL theorists. What language is "better" is a question that is 100% psychological, and has absolutely nothing to do with one theory or another. It's a question PL researchers are simply not qualified to answer (Also, even before psychology, it may well be that moving from one point along the spectrum towards richer typing has a cost -- simple, economic cost in development time or in performance -- that is higher than the benefit of extra correctness. Most programs need to be correct only up to a point. Why should they pay for a type system that will make them more correct than they need to be?)
2. The question, "How close can we bring those test suites to the unattainable ideal of never accepting a broken program?" directed at dynamic typing can also be directed at static typing. True, a statically typed language may reject all programs, but practical ones will accept broken ones as well as reject correct ones, simply because there are properties the type system won't verify.
3. Testing isn't the only way to verify dynamically typed programs -- or any program along the typing-spectrum -- for properties that aren't enforced by its type system. There are quite good formal verification methods that don't rely on types. True, the author uses a confusing, self-referential (undecidable? :)) definition for types: "a type is a label used by a type system to prove some property of the program's behavior" that is hard to argue with ("a type is something the type system uses"), but there are "property annotations" in the form of pre- and post-conditions used by verifiers, that aren't normally regarded as types (they don't form a particularly nice algebra), and may be used at any point along the spectrum to prove properties beyond the reach of the particular type system. The implication that types are the only way to prove correctness is wrong.
41 comments
[ 4.3 ms ] story [ 111 ms ] thread'It doesn't make sense to do the same kinds of exhaustive unit testing in Haskell as you'd do in Ruby or Smalltalk. It's a waste of time. It's interesting to note that the whole TDD movement comes from people who are working in dynamically typed languages.'
Unit testing in dynamically typed languages serves two purposes: 1) to prove code correctness, and 2) to prove code soundness/completeness, to show that the result of a function is correct for most or all input parameters. In statically typed languages 1) is already taken care of by the type system. If your code compiles then there are no glaring type errors in it and your code is correct. However, you still have #2 to worry about.
I work in Scala a lot where there is a static type system. I still have extensive unit tests, and I can't tell you how many times it's saved me when I've changed code in one area of the codebase, thought it was sound and complete, and then immediately become informed it's caused tests to fail, even though it compiled correctly. For instance I'll change code in a model and think that the controller will still behave the same way - and unit testing demonstrates immediately that it doesn't. This is especially true when I didn't write the controller that depends on the model. Testing also helps you rigorously test corner cases - when does this code throw an exception, when does it return a negative number, etc.? It really helps you get a good sense of when a piece of code is done, and move onto the next code.
Unit testing is indispensible both in static and dynamically typed languages, and I don't think lots of coverage is a waste of time in static languages.
Anyway, what methods did you have in mind?
OK, actually a lot!
Or a more complicated example that I've run into recently. You have a set of predicates, some of which can be evaluated in the browser, some not - e.g. IsFirefox & EverVisitedUrl(url). You then (server side) evaluate EverVisitedUrl(url), get a partial result IsFirefox & True = IsFirefox, and then push whatever is left to javascript `isBrowserFirefox()`.
In python/ruby/etc, you'd need extensive tests to make sure this translation is properly handled. In Scala, if your function doesn't have type `FreeBool[ArbitraryPredicate] => FreeBool[JavascriptEvaluatablePredicate]`, your code won't compile.
Turns out... we don't really do that so much.
With a suitably enlarged definition of (static) type, a lot of tests become type-assertions.
Eg red black trees have interesting balancing requirements: no t
See eg Red Black Trees are another interesting example. A red black tree is a binary search tree, and all its nodes are coloured either red or black. You can not have two red nodes in a row on any path, but all paths from root to any leave have to have the same number of black nodes.
Testing that these two properties hold after an arbitrary number of inserts sounds like a good candidate for a unit tests, and doesn't sound like a type assertion, does it?
See https://www.reddit.com/r/haskell/comments/ti5il/redblack_tre... for how to encode those properties into the types.
In any case, Haskell has great support for unit tests, too. (Because in general you can't and at any rate don't want to encode everything you care about in the type system.)
Have a look at QuickCheck. There are ports for various other languages, too. QuickCheck is a generalization of the table-driven approach to unit-testing: it's about generating those tables automatically, and automatically simplifying any inputs found that lead to buggy behaviour.
These are things I'd have lots of unit tests for.
Here is another example of using static types to fix a problem I constantly run into in Python (adding vectors from the wrong vector spaces together): https://www.chrisstucchio.com/blog/2014/type_safe_vector_add...
By and large, unit tests exist to quickly find bugs.
"It's interesting to note that the whole TDD movement comes from people who are working in dynamically typed languages... I'm not saying that unit testing is a bad idea with static types; only that it's entirely appropriate to scale it back a little.)"
What is the difference between "code correctness" and "to show that the result of a function is correct for all input parameters"? In common parlance these are the same thing.
Also, what does it even mean for a piece of code to be sound or complete? Sound with respect to what? Complete with respect to or relative to what?
I think the words that you want are "correct wrt a specification" instead of sound and "total" instead of complete?
Testing cannot prove correctness, period. The proof is a set of unit tests that cover every single input and also a proof that the set of inputs you tested is the entire domain. Basically no in-the-wild unit testing does even the former.
What you mean to say, I think, is, "testing is indispensable when your specification language isn't sufficient for specifying all correctness properties for your code."
Which is about right, but the way that you worded this post was extraordinarily confusing.
Immediately contradicted: A static type system is a mechanism by which a compiler examines source code and assigns labels (called "types") to pieces of the syntax, and then uses them to infer something about the program's behavior.
This is possible to do with a program that is understood as being dynamically typed.
Moreover, whenever a type can be assigned to a piece of syntax, it will agree with the dynamic type.
I.e. not "completely different things".
> This is possible to do with a program that is understood as being dynamically typed.
Well and good, but it usually isn't. So the article's point is valid.
I've been hearing that performance isn't a problem for the last 20 years, yet it seems like I still spend a lot of time waiting for computers and devices to respond. I've worked in mobile and embedded (arguably not a small segment) for a while, and every major product I've released has had a last minute optimization scramble. The growth of these spaces (and now wearable devices) is only making this worse.
Well considering Rust I'm guessing Mr K might have different views now.
> Recently, it was brought up on Proggit that Chris Smith's "What to Know Before Debating Type Systems" was no longer online. This is a really great article, and in an effort to make sure it survives, I've grabbed the archive.org cache and am 'reprinting' it here. If you're into programming languages, read this and level up!
On the other hand, a lot of these systems aren't that old. I don't think Android is a Rube Goldberg pile of legacy. But Google acquired a company to get the V8 JS interpreter team for WebKit/Blink, and the Android team just created ART to replace Dalvik. These are smart people who've done a lot of performance measurement and optimization. If the VM didn't matter, it seems like a lot of money and time spent for nothing, right?
Is this not claiming that static typing (and/or lambda calculus) solves the halting problem?
One can add a fix point to the calculus (such as the titular Y combinator), but that introduces inconsistency to the type system.
It's worth noting that this is not an either/or problem. Some modern dependently typed languages take a more nuanced approach: they have a less-powerful core with enforced termination¹ and a way to write potentially non-terminating code that's isolated from everything else by the type system. It's the same approach that Haskell uses successfully for IO—it allows IO, but only in a controlled and explicitly delimited part of the program.
In a very real sense, we can treat potential non-termination as yet another effect and manage it accordingly.
¹ Actually, they're even more nuanced than this: programs either have to provably terminate or be provably "productive", which means they produce some new output from new input in finite time. This allows languages to support beneficial infinite loops like the event loop in an operating system while preventing purely harmful busy loops that never get anywhere.
Had to double check the year on this one. Things must certainly have changed... For instance, Java is a staple of most CS curriculum. If not Java then often Python. /Never/ have I heard of Ruby being the primary language of choice by a CS department. (Nothing against Ruby, just an observation.)
On the other hand, what is the most popular language/framework for a beginning programmer to learn today? Ruby/Rails or Node? Whereas Java is the quintessential Corporate language.
I'm obviously making some generalizations here. But things certainly seemed to have changed a lot!
1. This debate is not (or no longer) binary. There is a whole spectrum of static typing richness, from dynamic typing to well beyond Idris. The debate, then, is not whether we should be at any of the extreme, but where along the spectrum (including, maybe, the extremes). The interesting question to pose to proponents of very rich type systems, then, is "should we always use the richest type system possible?", and if not, why not? The whole debate -- which, again, is not binary -- hides in two of the questions the author lists in the end: "How easy can it be made to program in a language... ?" Nobody argues that the richer the type system the more properties can be proven (except for one major caveat I mention in item 3). The debate isn't about what character strings containing programs can be rejected or accepted. Programming language design is 5% theory and 100% psychology. What string the compiler accepts is a question for PL theorists. What language is "better" is a question that is 100% psychological, and has absolutely nothing to do with one theory or another. It's a question PL researchers are simply not qualified to answer (Also, even before psychology, it may well be that moving from one point along the spectrum towards richer typing has a cost -- simple, economic cost in development time or in performance -- that is higher than the benefit of extra correctness. Most programs need to be correct only up to a point. Why should they pay for a type system that will make them more correct than they need to be?)
2. The question, "How close can we bring those test suites to the unattainable ideal of never accepting a broken program?" directed at dynamic typing can also be directed at static typing. True, a statically typed language may reject all programs, but practical ones will accept broken ones as well as reject correct ones, simply because there are properties the type system won't verify.
3. Testing isn't the only way to verify dynamically typed programs -- or any program along the typing-spectrum -- for properties that aren't enforced by its type system. There are quite good formal verification methods that don't rely on types. True, the author uses a confusing, self-referential (undecidable? :)) definition for types: "a type is a label used by a type system to prove some property of the program's behavior" that is hard to argue with ("a type is something the type system uses"), but there are "property annotations" in the form of pre- and post-conditions used by verifiers, that aren't normally regarded as types (they don't form a particularly nice algebra), and may be used at any point along the spectrum to prove properties beyond the reach of the particular type system. The implication that types are the only way to prove correctness is wrong.