I want to know what the people who are familiar with type theory but are not proponents of either static or dynamic type systems are up to. Did they move on to management? Switch to physics or painting? Retire?
Serious answer: type theory as a subject almost never discusses any idea like dynamic types (they wouldn't even be considered "types"). Presumably, if you only ever study it academically then you might actually have never even heard of dynamic types.
The founding act of denotational semantics was Scott's model of the untyped lambda calculus, which is surely the paradigmatic dynamically typed language. Moreover, its creation led to an immense body of work on type theory, because there are two two distinct, but related, intuitions underpinning what a type is.
On the one hand, you can think of starting with some given notion of computation (the lambda-calculus, say, or x86 machine code), and then you can think of types as picking out particular subsets of the set of valid programs. (In jargon, this is "types as retracts".)
In this view, a type is a property of a program. On the one hand, you can say that only things which pass type-checking are programs, and things which don't type check are simply not well-formed programs. In this view, a type is a kind of grammaticality constraint.
If you don't have a model of the untyped lambda calculus, you can't speak formally about the first view, which is very limiting. This is because being able to shift between the views is important for thinking flexibly about different kinds of problems.
Of course, you can also try to combine these two views. A few years back, Noam Zeilberger and Paul-Andre Mellies wrote a gorgeous paper, "Functors are Type Refinement Systems", which lays out the principles of how these two views interact.
I hear what you're saying---and appreciate the references---but I guess what I intended to discuss above was the "practice of dynamic types/tags" as is carried out in software development.
LC is clearly "untyped" in that it doesn't carry any type system, but that's a distinct idea from "dynamically typed introspection". That's an engineering system.
So maybe my error is to read into "dynamic types" as something more than the most utilitarian reading, but I also think that's usually what the "debate" ends up being about.
Agreed, it's trivial to embed. This is the sense to which type theory doesn't really have a ton to "say" about dynamic types. See my other response for a bit more of a fleshed out idea here.
Short of it is that I'm reading "dynamic typing" as the engineering discipline involved in building systems that introspect that sum in meaningful ways.
Woodworking. When I code I use an awful mixture of bash, Nix, Haskell, and JavaScript, all mashed together. Sometimes it turns into something truly horrible like a Nix derivation with a bash script that calls a Haskell program to generate JavaScript. Or I end up trying to use an Agda DSL to prove my bash script correct and then it gets executed through a Nix derivation that embeds Emacs to evaluate the Agda via the editor mode because the goddamn compiler didn’t work. Whatever. I fucking hate computers
The long-term benefit of typing doesn't show up in examples that fit in tweets: if the desired behavior is encoded in the types, the checks appear for free everywhere you use them, and you don't risk forgetting to test something in the n+1th function that you remembered to test in the nth.
I really enjoyed this style of writing. It respectfully expressed why he disagreed with someone else, but acknowledged that both he and said person achieved their results and had tests which covered that fact. Nothing inflammatory or overly partisan, thanks :)
> Is [not testing nil/invalid inputs] a risk? Sure, but only if some other part of the system was written without tests. If you call this function from a module that you wrote with tests, using something as effective as the TDD discipline, you won’t be passing nil or negative numbers, or any other form of invalid arguments. So I’m not going to worry about that. It’s on you.
The problem with this way of thinking is that it makes tracking down a bug much harder, and even if all software is correct at the end it will still make development slower.
Imagine a bunch of functions A, B, ... and Z where A depends on B and so on. If every one of those doesn't test what happens on incorrect inputs, then an incorrect input to A may cause an exception in Z. You would have to track all the way back up to find the cause of the issue.
For the given simple example, not testing negative of nil inputs may be fine because just looking at the code is enough to document it, but on a larger scale, failure conditions can be very obscure.
Simply put in a long chain of software, you will want to define on what values your function is valid and only accept those (so users don't think something works because only one case does). And to keep your code correct to that specification, you need to make sure it errors.
I've spent a lot of time now writing code in both Haskell and Elixir. Where I have found that static typing really shines is when you do large scale refactoring. Especially in a large code base it is much, much faster to fix compiler errors after refactoring, than to run the tests and figure out why each one is failing. In Haskell by the time my tests all compile after a refactor, they are already passing.
Yup. In a codebase without static types, large-scale refactors are probably just not practical, which may be why fans of dynamic types don't have this problem; they can't, and thus don't, do substantial refactors without rewriting.
The trick is to write the code so that one piece of code does not affect another piece of code. You can write static code in a dynamic language by making all functions pure functions eg. no side effects.
What about invalid arguments? What if someone calls: (random-elements -23 nil)? Should I write tests for those cases?
The function already handles negatives by returning an empty list for any count less than one. This isn’t tested; but the code is pretty clear. In the case of the nil, an exception will be thrown. That’s OK with me. This is a dynamically typed language. You get exceptions when you mess up the types.
Is that a risk? Sure, but only if some other part of the system was written without tests. If you call this function from a module that you wrote with tests, using something as effective as the TDD discipline, you won’t be passing nil or negative numbers, or any other form of invalid arguments. So I’m not going to worry about that. It’s on you.
This attitude coming from an experienced software developer is hard to fathom. Sure, if you're an experienced and meticulous developer that fully embraces TDD and you only work with other experienced and meticulous developers that full embrace TDD on the same type of software handling the same types of problems over and over, then sure, you might be able dodge a pretty high percentage of bugs a pretty high percentage of the time.
But most teams in the real world have a mix of inexperienced and experienced developers, meticulous and careless developers, developers that embrace TDD to varying degrees, and work on a variety of problems in a mix of domains with which the team members have varying degrees of experience.
So now your choices are:
1) code each and every function in a way that gives you high confidence that it works for the happy path and rely on the discipline of your team to ensure that no unhappy paths are hit
or, for approximately the same level of effort:
2) code each and every function in a way that gives you high confidence that it works for the happy path and which you have an extremely high degree of confidence that no unhappy paths even exist at all
in a unit-test scenario, you are writing tests based on the language and its properties.
he is applying risk based assessment which tests are required to provide a high quality implementation.
If a system misbehaves you will catch in higher level tests in the test pyramid eventually.
The bug was found regarding the null pointer, he can and should add a dedicated unittest to reproduce the issue when he fixes the bug, since there is evidence that his assessment was wrong. This is not bad but usually quite efficient if this doesn't occur often or has a large impact on the system's user base.
In a software solution you can't prove 100% correctness - neither through "standard" type-systems nor through tests.
> If a system misbehaves you will catch in higher level tests in the test pyramid eventually.
You might catch it eventually, or you might not. That's the problem with hoping you write enough tests.
> he can and should add a dedicated unittest to reproduce the issue when he fixes the bug
His argument is that dynamic language don't 'really' require writing more exhaustive tests than in an expressive static language. In this scenario, not only would he need to write an extra test but he also needs to spend time after the fact tracking down an error thrown in a higher-level function.
> In a software solution you can't prove 100% correctness
This isn't about proving 100% correctness, it's about what happens when you pass a non-list into a list processing function. More expressive type systems allow you to reduce the number of nonsensical questions you have to answer.
> ... even using a dynamically typed language I don’t have to write the test for nil because I know that nil will never be passed. I don’t need to make states unrepresentable, if I know those states will never be represented.
It would be interesting to actually study and measure how much time even teams doing TDD spend on dealing with these kinds of errors. In my experience, they're pretty common.
In the 90’s we had a large rush of new people writing libraries for the first or second time.
One common source of frustration was instability in the exceptions thrown due to bad states, from bad inputs to networking issues to disk permissions.
You’d get a new point version and suddenly have to rewrite your error handling code so the user still got a reasonable message and/or call to action.
Lesson? Errors are part of your public interface. Write at least enough tests to pin the behavior.
It also helps with false positives for tests. Because if you introduce a null pointer exception for negative numbers while trying to add features or improve performance, that’s probably not what you expected. Certainly not what your users expect.
Test your shit. It takes less energy than the mental gymnastics of justifying why you aren’t.
I don't quite agree... I feel like, theoretically, yes we should feed bad data to all the functions and use property-based tests to ensure the features hold. However, in the real-world if you're using a language like Clojure for day to day development your team is probably skilled enough to write basic functions without meticulously checking every little thing for errors. There has to be a trade off between 99.9999% confidence of your functions and fast development velocity. For most products the application code matters a lot more than tests.
There should still be strong checks on the external interfaces to your system with bad data tests, schemas, property based testing, etc. For a normal function inside your system it's mostly overkill to be testing those things. Integration tests should validate that your functions call each other correctly and some acceptance tests could generate data from one interface and check that it flows through the system well. There could be corrupted types that you use for testing with Clojure's spec library that either return the expected type or a random corrupted type. Those combinations should adequately exercise the functions to find most of the errors.
What stands out for me is the casual acceptance of this behavior for negative parameters. It returns an empty list so it’s all good? No way! Asking for a list of negative length is a conceptual error. This should at least be an assert. That ensures nobody accidentally starts relying on bad behavior by prohibiting it. Of course, if you can use the type system to do this by using an unsigned type (and one without implicit non-failing conversions from signed types such as C has) then so much the better.
I think the author has the foundation of a good idea: don’t write tests for things that aren’t supposed to happen. (This is not the same as writing tests for error handling: errors are supposed to happen!) But he builds the wrong thing on top. You don’t just ignore things that aren’t supposed to happen and hope that they don’t. You make sure they don’t happen, either by asserting at runtime or making them logically impossible at compile time.
Once you reach that point, then you see that a type is just an assert that’s nicer to write, checked earlier, and is more comprehensive. The tradeoff is that they are less expressive, so you still need traditional asserts sometimes.
> You make sure they don’t happen, either by asserting at runtime or making them logically impossible at compile time.
One thing I find common with arguments from people like the author is that they don't consider types can be more powerful than the ones they're used to dealing with in the languages they use. It seems impossible to them that one could simply encode the parameter as being a type which does not allow for negative values or `nil`. As you say, asserting at compile time that the program is correct.
I guess this is a specific example of the Blub Paradox.
I saw this a lot when Swift came out. Suddenly a lot of Objective-C programmers were learning a new language with a fairly different type system, and it was tough. The Optional type was an especially strong pain point.
What I found particularly interesting is that C (and Objective-C) has optional types. All pointer types are optionals. What it lacks is optional non-pointer types, and non-optional pointer types. Because optionality is an inherent part of pointer types in the language, you never learn to think about optionality separately. It's like a fish in water: it's so common you don't even see it.
I suppose it would show up even more strongly with someone used to a language like Ruby. If C programmers have a hard time really grasping the idea of optionality because the language doesn't make it explicit, then a Ruby programmer might have trouble with static types at all. (And, to be fair, the same no doubt applies in the other direction: someone coming from a strong statically typed language probably has some hurdles to understanding dynamic type systems.)
The author claims that the number of tests required are only those tests that are necessary to describe the correct behavior of the system and that this is true whatever the programming language is dynamic or statically typed. But with these assertions you highlighted What about invalid arguments? What if someone calls: (random-elements -23 nil)?, the author shows that he don't give any value to static typing at all. He simply believes that what is tested with types don't matter: So I’m not going to worry about that. It’s on you..
I think he misses the fact that types are a cheap syntactic way to bring confidence on very diverse aspects of a system: compatibility of values or binary representations but also correctness of dynamic behaviors (see how Rust controls memory with scope type variables) or even algorithmic complexity (see A typed, algebraic approach to parsinghttps://www.cl.cam.ac.uk/~nk480/parsing.pdf).
The odds that this test will fail are on the order of a million to one. I could better those odds if I thought it necessary.
That seems... pretty bad? Am I missing something?
If you have 1000 tests like that in a large codebase with a continuous build, you’re going to get an irritating number of random failures.
It’s not really a concern until you have a really large codebase. But if you leave it until you have a really large codebase, it’s a lot more effort to go back and fix the flaky tests.
50 tests that fail 1% of the time will cause almost half of your builds to fail. And the odds of two failing in a row are about one in four. As the number of builds per day increases, the probability of a given day having multiple failed builds in a row (causing you to look closely at the build and commit logs) approaches 100%
"My answer to that is that even using a dynamically typed language I don’t have to write the test for nil because I know that nil will never be passed. I don’t need to make states unrepresentable, if I know those states will never be represented."
You don't know that nil or whatever "won't ever be passed" in dynamically types language!
The fact that Bob Martin, a supposedly experienced software developer, genuinely, sincerely argues a variation of "I don't need to handle this case, since I just know that this can't happen because... Obviously no one, certainly not me would do that" is inconceivable.
Does he not even consider what happens when someone else, i.e. no him, passes "unrepresented" values to his function? WTH?
When I’m writing Haskell I still practice Test Driven Development but I usually start with Type Driven Development.
The richer the type system, the more expressive the propositions I can encode, and the easier it is to write a proof — a term with a type that matches the proposition. Leaving me free to write only the tests that matter and eliminating the need to start with specifying degenerate cases.
You can express concepts like non-empty lists, constraints on kinds and types which encode the propositions you’d normally test by example using unit tests. It’s simply not necessary in some cases to start designing programs with unit tests when you have a type system like Haskell’s (or Idris’, Agda’s, or Lean’s, etc)
The hidden thing about Haskell that makes it super-powerful for expressing safe programs (in my experience) is not only that you can express tight propositions in the types. It's that Haskell makes it very easy to write total functions over wider types.
When writing OOP code you often start with a number of base assumptions about the input and build the code around them. With Haskell, you make no such assumptions initially and either encode total functions (most of them!) or tighten the types until they match the true system requirements.
There are some Prelude functions which violate this understanding (`head` being a classic example). Writing code without these as much as possible makes your code almost guaranteed robust right out of the gate.
I would like to ask the question what we are actually trying to achieve with both types and with tests. The answer is to, in case of error, find the error as soon as possible instead of in production when the angry customer calls us. The sooner the error is found the smaller the problem is. If it is found in compilation it says 'you have an error on line 43'. If it is found in automated tested it says 'there is something fishy about functionality such-and-such'. Pushing forward finding the error from compile time to automated test time is a postponement and therefore not an improvement. Also, I really wish I could imagine encountering a production system with a test coverage approaching 100% but I have never been that lucky. In that case your type system is still protecting you but the tests that people failed to write are not doing very much.
>My answer to that is that even using a dynamically typed language I don’t have to write the test for nil because I know that nil will never be passed. I don’t need to make states unrepresentable, if I know those states will never be represented.
If only programming actually worked this way... You can never know what "will never be passed" unless you prove it, and types offer that proof.
Tons of bugs in languages that allow null to break their type system, for example, concern null pointer dereferencing...
I'm bewildered because every senior dev I've ever spoken to has been somewhat unanimous about the use of types and tests. Reading this I'm wondering if there's a special context where this proposed approach is more suitable? Possibly a single dev, tiny sealed program?
For every other system, be it with more than 1 developer or that will grow to more than 10s of functions, types and tests eliminate being anchored to the code you've written in the past.
The #1 be benefit to them is you can forget about what you've written. It's unlikely you'll remember in 6 months time that one function where you can't pass in negatives or Nil. Do you want to have to read the internals of every function you're calling? Isn't that a violation of some open/closed principal?
There is nothing sweeter than defining your intent in code contracts and confirming those contracts work before letting you or anyone else use them. If you don't want negatives being passed to your function, maybe unsigned integers aren't a good idea. Maybe make it explicit that you're sending in an 'age' value by defining it as a value object with its own validation. Make it blow up in the hands of the consumer as fast as possible. If you're waiting until runtime to tell you these things then you're not going to enjoy development.
And your peers will hate maintaining your junk code.
I'd say there's also a big difference in the sort of correctness that static types guarantee vs the correctness that tests give you. Tests, to borrow some phrasing from Donald Rumsfeld, are only really effective against "known unknowns" not "unknown unknowns." Tests are only as thorough as the test writer and the "known unknown" cases they can come up with to test against. But as software developers we've all been in the situation where some case that you didn't think to test for is what winds up causing a bug (an "unknown unknown").
Static type systems on the other hand, can give you much greater guarantees of correctness (if they're sound). Due to the Curry-Howard isomorphism we know that programs in sound static type systems are the same as mathematical proofs. That's a much stronger guarantee than what you're given by testing alone. The problem of missing a case in your testing goes away if you have a mathematical proof that that case cannot occur. You've taken away some of the burden of thoroughness from the programmer and given it to the compiler instead.
In a perfect programming utopia we would all encode the desired properties of our programs in static types and have no need for testing because we'd have proofs of correctness. The problem of course is that writing those kinds of proofs into types is very time consuming and tedious and isn't realistic for most software development. So we still need tests to cover what is too expensive or complicated to type.
I think it is pretty easy to illustrate why fewer tests are needed in certain statically-typed languages.
JS
function max(a, b) {
if (a < b) {
return b;
}
return a;
}
console.log(max(1, 2));
// 2
console.log(max(2, 1));
// 2
console.log(max([1,2,3]));
// [1,2,3]
Rust
fn max<T: PartialOrd>(a: T, b: T) -> T {
if a < b {
b
} else {
a
}
}
println!("{}", max(1, 2));
// 2
println!("{}", max(2, 1));
// 2
println!("{}", max([1, 2, 3]));
// Compiler error
In JS, it would be prudent to test for reasonable misuse of this kind (return undefined, throw Error, etc). The author claims _This is a dynamically typed language. You get exceptions when you mess up the types._ That isn't true in this case and it is not clear from the code what would/should happen.
A common philosophy in JavaScript is to make it just work. For example if an array is passed, sort it and return the max value, which was probably what the programmer intended.
Which would need even more tests, because now there a set of types that will work (e.g. numbers, arrays of numbers), with code to make them work and tests on that; and other types do not work, and tests on that.
Yes, you write a new test for each new feature. But if you do the same thing in a statically typed language, once you've allowed arrays, and what not, how do you know if the function still works, besides carefully studying it.
Well, you don't make it "just work" for all conceivable input shapes. You make it work for the one and only accepted input shape, which is 1) much easier to make work, 2) means that you don't miss possible input shapes, and 3) is much easier to test thoroughly.
The max value of what? The array in one of the arguments? What if there are two arrays? Or an array and a number? Or a multi-dimensional array of numbers and any of the above?
I think this attempt to come up w/ reasonable interpretations for unanticipated usages of a function is kind of a rabbit hole. Beyond that I think it's also problematic to assume that all usages of a function in a language without a type system are intended usages, i.e. that programmers _mean_ to pass arrays whenever an array appears as one of the arguments.
Sometimes you want to call a function with something else, or are not using an IDE (no argument hinting), and just call the function intuitively. Instead of converting the input, or writing a middle-man, you edit the function to accept it as is. You don't even have to pass values in the right order, the function will figure it out.
There's nothing wrong w/ polymorphic functions, but there has to be a reasonable rule to apply for what kinds of shapes of data are permitted. Trying to aggressively handle unforeseen cases instead of indicating an error doesn't actually help anyone, it's akin to swallowing exceptions. It's why falsey values and automatic type conversion are some of the most problematic features in javascript.
Your example of how to handle max for array arguments is exactly the kind of thing I would discourage in js code, because it overloads the meaning of "maximum" to data that don't have a natural way of assigning an ordering if heterogeneous arguments are permitted (actually it sounds like you're saying something like max([1], [9]) should return "9", which doesn't correspond to an intuitive understanding of "maximum" at all given it returns something that isn't either of the passed arguments). Whereas the rust code can use the "PartialOrd" trait to ensure we only try to produce a maximum of like elements with a defined ordering relation. That's fine for a limited number of cases where its easy to show type equivalence in js, but I think it's problematic as a general design principle, and because you don't have ways to express the limits of polymorphism I've seen this kind of thing proliferate to unsafe uses of a function very quickly.
Only after you have tried to call the function with an array many times, that's when it would make sense. And there's another option too, to instead add a check and a friendly error. But it should be a fairly rare thing to do.
Naming things can be hard and maybe more so if you do not have type annotations. But being used to dynamic languages I always find type annotations a chore. And I think it's better to have a good name and no types, then a bad name and types. eg. max(...numbers) vs x(y:number, z:number) -> number . Even though x is more verbose it can be anything, but with max(...numbers) I can be fairly sure.
If you're writing a standard library (or similar) then you do want tests to check that runtime errors are reported correctly with a nice error message, because you that is what the customers of your library see.
Within a single app of reasonable size, this isn't so important.
Deciding type-safety of code also requires solving the halting problem, but haskell still tries!
I guess the question could be practical. Some functions are supposed to handle infinite lists: rfold, map, etc. How are these functions (or other, nontrivial ones) tested in practice, to ensure that they do not become accidentally strict?
> Deciding type-safety of code also requires solving the halting problem, but haskell still tries!
does it? afaik typechecking is decidable for most type systems, and only becomes undecidable with something like dependent types (or c++ templates) but i could be wrong
just noticed i forgot to reply to the rest of your comment! i'm not sure how it's done in practice (except for "thinking about it really hard"). i came up with something though:
`map` should be easy, because it's productive, i.e. it yields one result-element after processing every input element. so we could just test it by doing something like
map f [1, 2, error "too strict!"
and checking if it blows up when we force the first 2 elements – if it does, it must've processed the third element (error) as well, so it's too strict; if it didn't, it hasn't touched the last element, so it's as lazy as we wanted (only processes the stuff we asked for) and would work for infinite lists too (i think).
we could also do something similar for `foldr`:
foldr (:) [] [1, 2, error "too strict!"]
which just reconstructs the original list. then we can apply the same reasoning as above.
You can have types in haskell that represent finite length lists. Here's a blog post giving an overview of several methods of doing so (and several examples of libraries in the wild that provide this): https://blog.jle.im/entry/fixed-length-vector-types-in-haske...
There's a tradeoff here between generality and how important it is to encode all invariants about a piece of data. Many haskell list processing functions are expressed in terms of right folds, which makes infinite lists fairly unproblematic to work with so long as only part of the list is demanded in the end, however for some cases you may want the type system to ensure you can't receive an infinite list.
I believe the point of QuickCheck is actually to try and minimize the size of the test cases as much as possible by finding the minimal failing test case. So it explicitly tries to avoid testing larger and larger inputs or outputs, even if they could be potentially infinite.
If you want the ability to encode bounds inside the type itself, then you'll need to look at various extensions like DataKinds, TypeFamilies, etc, or at a dependently typed language like Idris.
The promise of better type systems os that more of your code will be secured by types, not that everything will be covered. That is why there are still people working on newer type systems (e.g. dependent types, linear types, etc).
For the specific example you give, you can either use liquid haskell, which is an annotation system bringing richer types to haskell, or use another lang that has dependent types off the shelf.
There is a misguided notion on testing. Testing cannot establish correctness on a program unless you test every possible input and output. A test only proves a specific test case is correct, that's it, this is not actual program correctness.
Type checking is an actual proof that is light years ahead of a test in the fact that you need zero test cases to prove your program is correct in terms of types.
To achieve the same affect with testing you must test your function with every possible input for every possible type. An untyped addition function must test for what happens when you give that function a pointer to every possible permutation of a nested hashmap of strings and arrays otherwise you are not establishing correctness. What you are actually doing is taking a statistical sample of random inputs and guessing that the function is correct based off of that sample.
For greater predictability the test samples should be randomized following statistical procedures but this is rarely followed as most testers don't actually understand that they are taking a small statistical sample of a domain that covers an almost unlimited amount of possible inputs.
Tests are essentially selected with high programmer bias so a lot of bugs make it through.
I agree that you don't generally /need/ to test preconditions of internal code (although you should document them). However, if you're writing a library with an API that will be called by others, you should make sure your code fails fast, and you should assert that behavior in your tests.
Adding extra code to ensure you fail fast is often well worth it in future debugging time, even for internal code.
>Static typing is an attempt to make software more mathematical. Type correctness is deductive and provable. However, type correctness does not imply behavioral correctness. Even when fully type correct the behavior must be demonstrated empirically.
I think this is the crux of the problem and my experience agrees on this statement.
At the end of the day, its Behaviour that matters the most.
68 comments
[ 57.2 ms ] story [ 206 ms ] threadhttps://ro-che.info/ccc/17
On the one hand, you can think of starting with some given notion of computation (the lambda-calculus, say, or x86 machine code), and then you can think of types as picking out particular subsets of the set of valid programs. (In jargon, this is "types as retracts".)
In this view, a type is a property of a program. On the one hand, you can say that only things which pass type-checking are programs, and things which don't type check are simply not well-formed programs. In this view, a type is a kind of grammaticality constraint.
If you don't have a model of the untyped lambda calculus, you can't speak formally about the first view, which is very limiting. This is because being able to shift between the views is important for thinking flexibly about different kinds of problems.
Of course, you can also try to combine these two views. A few years back, Noam Zeilberger and Paul-Andre Mellies wrote a gorgeous paper, "Functors are Type Refinement Systems", which lays out the principles of how these two views interact.
http://noamz.org/papers/funts.pdf
LC is clearly "untyped" in that it doesn't carry any type system, but that's a distinct idea from "dynamically typed introspection". That's an engineering system.
So maybe my error is to read into "dynamic types" as something more than the most utilitarian reading, but I also think that's usually what the "debate" ends up being about.
Also, type theory is a mathematical/logical theory first, the connection to programming languages was discovered long after it was developed.
Short of it is that I'm reading "dynamic typing" as the engineering discipline involved in building systems that introspect that sum in meaningful ways.
The problem with this way of thinking is that it makes tracking down a bug much harder, and even if all software is correct at the end it will still make development slower.
Imagine a bunch of functions A, B, ... and Z where A depends on B and so on. If every one of those doesn't test what happens on incorrect inputs, then an incorrect input to A may cause an exception in Z. You would have to track all the way back up to find the cause of the issue.
For the given simple example, not testing negative of nil inputs may be fine because just looking at the code is enough to document it, but on a larger scale, failure conditions can be very obscure.
Simply put in a long chain of software, you will want to define on what values your function is valid and only accept those (so users don't think something works because only one case does). And to keep your code correct to that specification, you need to make sure it errors.
The function already handles negatives by returning an empty list for any count less than one. This isn’t tested; but the code is pretty clear. In the case of the nil, an exception will be thrown. That’s OK with me. This is a dynamically typed language. You get exceptions when you mess up the types.
Is that a risk? Sure, but only if some other part of the system was written without tests. If you call this function from a module that you wrote with tests, using something as effective as the TDD discipline, you won’t be passing nil or negative numbers, or any other form of invalid arguments. So I’m not going to worry about that. It’s on you.
This attitude coming from an experienced software developer is hard to fathom. Sure, if you're an experienced and meticulous developer that fully embraces TDD and you only work with other experienced and meticulous developers that full embrace TDD on the same type of software handling the same types of problems over and over, then sure, you might be able dodge a pretty high percentage of bugs a pretty high percentage of the time.
But most teams in the real world have a mix of inexperienced and experienced developers, meticulous and careless developers, developers that embrace TDD to varying degrees, and work on a variety of problems in a mix of domains with which the team members have varying degrees of experience.
So now your choices are:
1) code each and every function in a way that gives you high confidence that it works for the happy path and rely on the discipline of your team to ensure that no unhappy paths are hit
or, for approximately the same level of effort:
2) code each and every function in a way that gives you high confidence that it works for the happy path and which you have an extremely high degree of confidence that no unhappy paths even exist at all
It's just not a tough decision for me.
Indeed in many dynamically typed languages an argument of the ‘wrong’ type is silently coerced in possibly unexpected ways.
he is applying risk based assessment which tests are required to provide a high quality implementation.
If a system misbehaves you will catch in higher level tests in the test pyramid eventually.
The bug was found regarding the null pointer, he can and should add a dedicated unittest to reproduce the issue when he fixes the bug, since there is evidence that his assessment was wrong. This is not bad but usually quite efficient if this doesn't occur often or has a large impact on the system's user base.
In a software solution you can't prove 100% correctness - neither through "standard" type-systems nor through tests.
If you want to show formal correctness of a program have a look at https://cs.stackexchange.com/questions/13785/formal-program-...
You might catch it eventually, or you might not. That's the problem with hoping you write enough tests.
> he can and should add a dedicated unittest to reproduce the issue when he fixes the bug
His argument is that dynamic language don't 'really' require writing more exhaustive tests than in an expressive static language. In this scenario, not only would he need to write an extra test but he also needs to spend time after the fact tracking down an error thrown in a higher-level function.
> In a software solution you can't prove 100% correctness
This isn't about proving 100% correctness, it's about what happens when you pass a non-list into a list processing function. More expressive type systems allow you to reduce the number of nonsensical questions you have to answer.
> ... even using a dynamically typed language I don’t have to write the test for nil because I know that nil will never be passed. I don’t need to make states unrepresentable, if I know those states will never be represented.
It would be interesting to actually study and measure how much time even teams doing TDD spend on dealing with these kinds of errors. In my experience, they're pretty common.
One common source of frustration was instability in the exceptions thrown due to bad states, from bad inputs to networking issues to disk permissions.
You’d get a new point version and suddenly have to rewrite your error handling code so the user still got a reasonable message and/or call to action.
Lesson? Errors are part of your public interface. Write at least enough tests to pin the behavior.
It also helps with false positives for tests. Because if you introduce a null pointer exception for negative numbers while trying to add features or improve performance, that’s probably not what you expected. Certainly not what your users expect.
Test your shit. It takes less energy than the mental gymnastics of justifying why you aren’t.
There should still be strong checks on the external interfaces to your system with bad data tests, schemas, property based testing, etc. For a normal function inside your system it's mostly overkill to be testing those things. Integration tests should validate that your functions call each other correctly and some acceptance tests could generate data from one interface and check that it flows through the system well. There could be corrupted types that you use for testing with Clojure's spec library that either return the expected type or a random corrupted type. Those combinations should adequately exercise the functions to find most of the errors.
I think the author has the foundation of a good idea: don’t write tests for things that aren’t supposed to happen. (This is not the same as writing tests for error handling: errors are supposed to happen!) But he builds the wrong thing on top. You don’t just ignore things that aren’t supposed to happen and hope that they don’t. You make sure they don’t happen, either by asserting at runtime or making them logically impossible at compile time.
Once you reach that point, then you see that a type is just an assert that’s nicer to write, checked earlier, and is more comprehensive. The tradeoff is that they are less expressive, so you still need traditional asserts sometimes.
One thing I find common with arguments from people like the author is that they don't consider types can be more powerful than the ones they're used to dealing with in the languages they use. It seems impossible to them that one could simply encode the parameter as being a type which does not allow for negative values or `nil`. As you say, asserting at compile time that the program is correct.
I saw this a lot when Swift came out. Suddenly a lot of Objective-C programmers were learning a new language with a fairly different type system, and it was tough. The Optional type was an especially strong pain point.
What I found particularly interesting is that C (and Objective-C) has optional types. All pointer types are optionals. What it lacks is optional non-pointer types, and non-optional pointer types. Because optionality is an inherent part of pointer types in the language, you never learn to think about optionality separately. It's like a fish in water: it's so common you don't even see it.
I suppose it would show up even more strongly with someone used to a language like Ruby. If C programmers have a hard time really grasping the idea of optionality because the language doesn't make it explicit, then a Ruby programmer might have trouble with static types at all. (And, to be fair, the same no doubt applies in the other direction: someone coming from a strong statically typed language probably has some hurdles to understanding dynamic type systems.)
I think he misses the fact that types are a cheap syntactic way to bring confidence on very diverse aspects of a system: compatibility of values or binary representations but also correctness of dynamic behaviors (see how Rust controls memory with scope type variables) or even algorithmic complexity (see A typed, algebraic approach to parsing https://www.cl.cam.ac.uk/~nk480/parsing.pdf).
That seems... pretty bad? Am I missing something?
If you have 1000 tests like that in a large codebase with a continuous build, you’re going to get an irritating number of random failures.
It’s not really a concern until you have a really large codebase. But if you leave it until you have a really large codebase, it’s a lot more effort to go back and fix the flaky tests.
You don't know that nil or whatever "won't ever be passed" in dynamically types language!
The fact that Bob Martin, a supposedly experienced software developer, genuinely, sincerely argues a variation of "I don't need to handle this case, since I just know that this can't happen because... Obviously no one, certainly not me would do that" is inconceivable.
Does he not even consider what happens when someone else, i.e. no him, passes "unrepresented" values to his function? WTH?
The richer the type system, the more expressive the propositions I can encode, and the easier it is to write a proof — a term with a type that matches the proposition. Leaving me free to write only the tests that matter and eliminating the need to start with specifying degenerate cases.
You can express concepts like non-empty lists, constraints on kinds and types which encode the propositions you’d normally test by example using unit tests. It’s simply not necessary in some cases to start designing programs with unit tests when you have a type system like Haskell’s (or Idris’, Agda’s, or Lean’s, etc)
When writing OOP code you often start with a number of base assumptions about the input and build the code around them. With Haskell, you make no such assumptions initially and either encode total functions (most of them!) or tighten the types until they match the true system requirements.
There are some Prelude functions which violate this understanding (`head` being a classic example). Writing code without these as much as possible makes your code almost guaranteed robust right out of the gate.
If only programming actually worked this way... You can never know what "will never be passed" unless you prove it, and types offer that proof.
Tons of bugs in languages that allow null to break their type system, for example, concern null pointer dereferencing...
For every other system, be it with more than 1 developer or that will grow to more than 10s of functions, types and tests eliminate being anchored to the code you've written in the past.
The #1 be benefit to them is you can forget about what you've written. It's unlikely you'll remember in 6 months time that one function where you can't pass in negatives or Nil. Do you want to have to read the internals of every function you're calling? Isn't that a violation of some open/closed principal?
There is nothing sweeter than defining your intent in code contracts and confirming those contracts work before letting you or anyone else use them. If you don't want negatives being passed to your function, maybe unsigned integers aren't a good idea. Maybe make it explicit that you're sending in an 'age' value by defining it as a value object with its own validation. Make it blow up in the hands of the consumer as fast as possible. If you're waiting until runtime to tell you these things then you're not going to enjoy development.
And your peers will hate maintaining your junk code.
Static type systems on the other hand, can give you much greater guarantees of correctness (if they're sound). Due to the Curry-Howard isomorphism we know that programs in sound static type systems are the same as mathematical proofs. That's a much stronger guarantee than what you're given by testing alone. The problem of missing a case in your testing goes away if you have a mathematical proof that that case cannot occur. You've taken away some of the burden of thoroughness from the programmer and given it to the compiler instead.
In a perfect programming utopia we would all encode the desired properties of our programs in static types and have no need for testing because we'd have proofs of correctness. The problem of course is that writing those kinds of proofs into types is very time consuming and tedious and isn't realistic for most software development. So we still need tests to cover what is too expensive or complicated to type.
JS
Rust In JS, it would be prudent to test for reasonable misuse of this kind (return undefined, throw Error, etc). The author claims _This is a dynamically typed language. You get exceptions when you mess up the types._ That isn't true in this case and it is not clear from the code what would/should happen.In rust, you don't need any tests like this.
I think this attempt to come up w/ reasonable interpretations for unanticipated usages of a function is kind of a rabbit hole. Beyond that I think it's also problematic to assume that all usages of a function in a language without a type system are intended usages, i.e. that programmers _mean_ to pass arrays whenever an array appears as one of the arguments.
Your example of how to handle max for array arguments is exactly the kind of thing I would discourage in js code, because it overloads the meaning of "maximum" to data that don't have a natural way of assigning an ordering if heterogeneous arguments are permitted (actually it sounds like you're saying something like max([1], [9]) should return "9", which doesn't correspond to an intuitive understanding of "maximum" at all given it returns something that isn't either of the passed arguments). Whereas the rust code can use the "PartialOrd" trait to ensure we only try to produce a maximum of like elements with a defined ordering relation. That's fine for a limited number of cases where its easy to show type equivalence in js, but I think it's problematic as a general design principle, and because you don't have ways to express the limits of polymorphism I've seen this kind of thing proliferate to unsafe uses of a function very quickly.
Naming things can be hard and maybe more so if you do not have type annotations. But being used to dynamic languages I always find type annotations a chore. And I think it's better to have a good name and no types, then a bad name and types. eg. max(...numbers) vs x(y:number, z:number) -> number . Even though x is more verbose it can be anything, but with max(...numbers) I can be fairly sure.
Within a single app of reasonable size, this isn't so important.
1. Why didn't QuickCheck test the infinite case?
2. How do we write tests that fail (instead of hang) if an infinite list is mishandled?
It seems like infinite lists act somewhat analogously to nulls: rndSelect cannot handle them, and that fact is not obvious in its type.
easy, just solve the halting problem!
I guess the question could be practical. Some functions are supposed to handle infinite lists: rfold, map, etc. How are these functions (or other, nontrivial ones) tested in practice, to ensure that they do not become accidentally strict?
does it? afaik typechecking is decidable for most type systems, and only becomes undecidable with something like dependent types (or c++ templates) but i could be wrong
`map` should be easy, because it's productive, i.e. it yields one result-element after processing every input element. so we could just test it by doing something like
and checking if it blows up when we force the first 2 elements – if it does, it must've processed the third element (error) as well, so it's too strict; if it didn't, it hasn't touched the last element, so it's as lazy as we wanted (only processes the stuff we asked for) and would work for infinite lists too (i think).we could also do something similar for `foldr`:
which just reconstructs the original list. then we can apply the same reasoning as above.There's a tradeoff here between generality and how important it is to encode all invariants about a piece of data. Many haskell list processing functions are expressed in terms of right folds, which makes infinite lists fairly unproblematic to work with so long as only part of the list is demanded in the end, however for some cases you may want the type system to ensure you can't receive an infinite list.
If you want the ability to encode bounds inside the type itself, then you'll need to look at various extensions like DataKinds, TypeFamilies, etc, or at a dependently typed language like Idris.
For the specific example you give, you can either use liquid haskell, which is an annotation system bringing richer types to haskell, or use another lang that has dependent types off the shelf.
Type checking is an actual proof that is light years ahead of a test in the fact that you need zero test cases to prove your program is correct in terms of types.
To achieve the same affect with testing you must test your function with every possible input for every possible type. An untyped addition function must test for what happens when you give that function a pointer to every possible permutation of a nested hashmap of strings and arrays otherwise you are not establishing correctness. What you are actually doing is taking a statistical sample of random inputs and guessing that the function is correct based off of that sample.
For greater predictability the test samples should be randomized following statistical procedures but this is rarely followed as most testers don't actually understand that they are taking a small statistical sample of a domain that covers an almost unlimited amount of possible inputs.
Tests are essentially selected with high programmer bias so a lot of bugs make it through.
Adding extra code to ensure you fail fast is often well worth it in future debugging time, even for internal code.
I think this is the crux of the problem and my experience agrees on this statement.
At the end of the day, its Behaviour that matters the most.