6 ms·

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

by Aqueous 11y ago

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.

wz1000 11y ago
Unless you're programming in a dependently typed language and have proven your code correct :P
- kazinator 11y ago
  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.
  - Silfen 11y ago
    Humans tend to make more mistakes. Convincing, say, Coq's typechecker of your proof is stronger evidence of correctness than convincing yourself.
    - pron 11y ago
      It is possible to prove program correctness -- by a computer -- that doesn't involve the type system.
      - eru 11y ago
        Depends on your definition of type system. Anyway, what methods did you have in mind?
        pron 11y ago
        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.
        tome 11y ago
        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. OK, actually a lot!
BadassFractal 11y ago
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.
yummyfajitas 11y ago
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.
- ubernostrum 11y ago
  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. Turns out... we don't really do that so much.
  - eru 11y ago
    > 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_trees_in_haskell_using_gadts_existential/ 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.
stephencanon 11y ago
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.
- mrbrowning 11y ago
  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.
- deleted 11y ago
  [deleted]
dllthomas 11y ago
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.
dllthomas 11y ago
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.)"
deleted 11y ago
[deleted]
nmrm2 11y ago
Your comment is confusing. 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.

by Aqueous 11y ago

wz1000 11y ago

Unless you're programming in a dependently typed language and have proven your code correct :P

kazinator 11y ago
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.
- Silfen 11y ago
  Humans tend to make more mistakes. Convincing, say, Coq's typechecker of your proof is stronger evidence of correctness than convincing yourself.
  - pron 11y ago
    It is possible to prove program correctness -- by a computer -- that doesn't involve the type system.
    - eru 11y ago
      Depends on your definition of type system. Anyway, what methods did you have in mind?
      - pron 11y ago
        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.
        tome 11y ago
        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. OK, actually a lot!

BadassFractal 11y ago

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.

yummyfajitas 11y ago

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.

ubernostrum 11y ago
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. Turns out... we don't really do that so much.
- eru 11y ago
  > 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_trees_in_haskell_using_gadts_existential/ 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.

stephencanon 11y ago

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.

mrbrowning 11y ago
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.
deleted 11y ago
[deleted]

dllthomas 11y ago

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.

dllthomas 11y ago

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.)"

deleted 11y ago

[deleted]

nmrm2 11y ago

Your comment is confusing. 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.