5 ms·

You're assuming we are only talking about very simple types, and simple program semantics. In the vast majority of dynamic languages, variables are unityped wi

You're assuming we are only talking about very simple types, and simple program semantics. In the vast majority of dynamic languages, variables are unityped with several tags (string, number, object, etc.) so they can trivially never experience a type error, with or without full path coverage (with the possible exception of attempting to access undefined variables, which is still not considered a type error in all languages). However, full path coverage does not guarantee that a value assigned a certain tag (which often drives which interfaces are provided) will have that same tag in all executions, and tags are often extremely imprecise descriptions of the value (often they are only precise enough to identify data layout), which means that many straightforward operations like property access and operator application have to be turned into potentially-throwing expressions or perform automatic casting to avoid causing a runtime error (both of which hinder many optimizations and making it hard to reason about your program's behavior). For instance, if you grab a value out of an array, assuming that the value you grab is an object with a certain property, and then access that property, requiring 100% path coverage still admits programs where the property will not be found (or where the property will be found, but have a different type than what is expected). Failing to account for the possibility that a tag is wrong is exactly what sum types rule out; failing to account for the existence of a property is what records (product types) rule out; the possibility of failing to grab an element from an array in the first place is what indexed data types (GADTs) rule out. None of these are type errors in most dynamic languages, and hence none can be replaced by 100% path coverage, except under very limited circumstances (which I can attest are not satisfied by real-world programs).

kazinator 10y ago
> so they can trivially never experience a type error (car a), a contains 42. Application bombs. > However, full path coverage does not guarantee that a value assigned a certain tag ... will have that tag in all executions. Not having the same tag in all executions isn't necessarily an error, and the guarantee is not required. It being vanishingly improbable that there isn't a type error is good enough. A guarantee in this area has limited value; it doesn't anywhere near prove correctness. > For instance, if you grab a value out of an array, assuming that the value you grab is an object with a certain property, and then access that property, requiring 100% path coverage still admits programs where the property will not be found (or where the property will be found, but have a different type than what is expected). I'm skeptical. An example program (Common Lisp, Ruby, Python, Scheme, ...) would be useful, which is fully exercised, via external inputs, such that no errors occur, yet more inputs can be found that trigger a slot-not-found type problem, or a wrongly typed value pulled from a slot. It's not that I don't think the program is possible, but that it has to be contrived. I don't care about catching fraud, only mistakes.
- Jweb_Guru 10y ago
  > (car a), a contains 42. Application bombs. That's an example of having the wrong tag, not type. > Not having the same tag in all executions isn't necessarily an error, and the guarantee is not required. It being vanishingly improbable that there isn't a type error is good enough. A guarantee in this area has limited value; it doesn't anywhere near prove correctness. I absolutely agree that it isn't necessarily an error (though I do not agree on "good enough"; see below), but I was responding to your own assertion that the guarantee you got was just as good as what you got in a statically typed system, which it's not. Simple statically typed systems verify that the tag is the same by only allowing one tag, eliminating certain classes of error caused by trying to access data as though it were a particular type when it's not (at the cost of limiting the flexibility of your program); more complex ones allow multiple tags if desired, but require you to check to make sure that the tag is what you expect before going on to perform operations on the wrapped data. > I'm skeptical. An example program (Common Lisp, Ruby, Python, Scheme, ...) would be useful, which is fully exercised, via external inputs, such that no errors occur, yet more inputs can be found that trigger a slot-not-found type problem, or a wrongly typed value pulled from a slot. It's not that I don't think the program is possible, but that it has to be contrived. I don't care about catching fraud, only mistakes. It's really, really easy to do this. JSON parse a list of objects (your external input) that are expected to have the same shape. Then walk through the list, accessing a certain property (say, name). It is very easy to write a test of this that achieves 100% path coverage (harder if you need to count exercising every path of the JSON parser, but not material for the purposes of my point). It is also very easy to construct an input for which this will fail. It happens routinely when you store something in a json blob store or accept input over an API endpoint (I've seen it numerous times) so your skepticism that it can happen in real programs is unwarranted. If you want, I can write out a program that does it, but the description I just gave should suffice. Note that this can happen even if you carefully check to make sure that all input is of valid shapes and explicitly put them in structures (let's say you have three or four shapes that you consider valid in most lists). You can get a similar failure in a language like Java if you try to, e.g., downcast to a subtype of Object, while iterating through the list, without first checking what type it is (something I've seen people do not infrequently, occasionally with reassuring comments about how it can't fail; the comments are often wrong). Examples of array indexing failures with 100% path coverage is even easier, as should be evident from the numerous array-out-of-bounds errors that exist in C; the only difference is that they don't turn into buffer overflows in memory-safe languages, they're still there. Overall, I find your skepticism that bugs like this show up to be pretty unwarranted, especially since I work in dynamically typed languages every day, and my coworkers and I cause bugs like this in production pretty frequently, including in repositories with 100% code coverage.

kazinator 10y ago

> so they can trivially never experience a type error (car a), a contains 42. Application bombs. > However, full path coverage does not guarantee that a value assigned a certain tag ... will have that tag in all executions. Not having the same tag in all executions isn't necessarily an error, and the guarantee is not required. It being vanishingly improbable that there isn't a type error is good enough. A guarantee in this area has limited value; it doesn't anywhere near prove correctness. > For instance, if you grab a value out of an array, assuming that the value you grab is an object with a certain property, and then access that property, requiring 100% path coverage still admits programs where the property will not be found (or where the property will be found, but have a different type than what is expected). I'm skeptical. An example program (Common Lisp, Ruby, Python, Scheme, ...) would be useful, which is fully exercised, via external inputs, such that no errors occur, yet more inputs can be found that trigger a slot-not-found type problem, or a wrongly typed value pulled from a slot. It's not that I don't think the program is possible, but that it has to be contrived. I don't care about catching fraud, only mistakes.

Jweb_Guru 10y ago
> (car a), a contains 42. Application bombs. That's an example of having the wrong tag, not type. > Not having the same tag in all executions isn't necessarily an error, and the guarantee is not required. It being vanishingly improbable that there isn't a type error is good enough. A guarantee in this area has limited value; it doesn't anywhere near prove correctness. I absolutely agree that it isn't necessarily an error (though I do not agree on "good enough"; see below), but I was responding to your own assertion that the guarantee you got was just as good as what you got in a statically typed system, which it's not. Simple statically typed systems verify that the tag is the same by only allowing one tag, eliminating certain classes of error caused by trying to access data as though it were a particular type when it's not (at the cost of limiting the flexibility of your program); more complex ones allow multiple tags if desired, but require you to check to make sure that the tag is what you expect before going on to perform operations on the wrapped data. > I'm skeptical. An example program (Common Lisp, Ruby, Python, Scheme, ...) would be useful, which is fully exercised, via external inputs, such that no errors occur, yet more inputs can be found that trigger a slot-not-found type problem, or a wrongly typed value pulled from a slot. It's not that I don't think the program is possible, but that it has to be contrived. I don't care about catching fraud, only mistakes. It's really, really easy to do this. JSON parse a list of objects (your external input) that are expected to have the same shape. Then walk through the list, accessing a certain property (say, name). It is very easy to write a test of this that achieves 100% path coverage (harder if you need to count exercising every path of the JSON parser, but not material for the purposes of my point). It is also very easy to construct an input for which this will fail. It happens routinely when you store something in a json blob store or accept input over an API endpoint (I've seen it numerous times) so your skepticism that it can happen in real programs is unwarranted. If you want, I can write out a program that does it, but the description I just gave should suffice. Note that this can happen even if you carefully check to make sure that all input is of valid shapes and explicitly put them in structures (let's say you have three or four shapes that you consider valid in most lists). You can get a similar failure in a language like Java if you try to, e.g., downcast to a subtype of Object, while iterating through the list, without first checking what type it is (something I've seen people do not infrequently, occasionally with reassuring comments about how it can't fail; the comments are often wrong). Examples of array indexing failures with 100% path coverage is even easier, as should be evident from the numerous array-out-of-bounds errors that exist in C; the only difference is that they don't turn into buffer overflows in memory-safe languages, they're still there. Overall, I find your skepticism that bugs like this show up to be pretty unwarranted, especially since I work in dynamically typed languages every day, and my coworkers and I cause bugs like this in production pretty frequently, including in repositories with 100% code coverage.