4 ms·

> Same can be said of static type checking so what is your point? That isn't true. Static typing offers machine checked proofs of the absence of a whole class

by willtim 10y ago

> Same can be said of static type checking so what is your point? That isn't true. Static typing offers machine checked proofs of the absence of a whole class of trivial errors; and potentially any invariants you've managed to teach it. My point was that testing does not negate the need for static types, as implied by the previous poster.

kazinator 10y ago
Although "class" sounds big, in fact there is only a countable number of places (nodes in the program's tree) where you can have a type error. The space in which any error whatsoever can occur is astronomical.
- TheDong 10y ago
  Let me give an analogy: Claim: "Getting vaccinated stops a whole class of diseases which might kill you" Your rebuttal: Although "class" sounds big, in fact there are only a countable number of viruses that vaccines save you from. The number of ways in which you can die is astronomical. In the above analogy, as in your original statement, you're completely missing the point that the class of errors / class of diseases is an important class and easily preventable, therefore you should do it. In fact, I think what you've said is the reverse of true. Static typing means that there's a chance of an error at each node in the program's tree because a statically typed and statically compiled language ensures that the program can be rendered as an AST before you ship it to your user. A dynamically typed interpreted language can have an error at literally any character in the entire thing, and you don't have "compile-time" to tell you it's not an error. The class of errors that you're saving yourself from is "every single character of this program could be wrong in a way that results in it not even being representable as an AST; there are astronomically many ways that can occur". In addition, it now goes wrong much later. You have to ensure that you've hit every path with testing before you can be even somewhat confident it's valid code, let alone logically correct and bug-free in other ways. A compiled statically-typed language you waste no more time than a compile-cycle to get that minimal assurance.
  - dllthomas 10y ago
    "Compiled" and "dynamically typed" are not opposites.
  - kazinator 10y ago
    Let me give an analogy: Claim: "Using a plastic liner stops urine from getting into the mattress". My rebuttal: "That's well and good, but I'm sure I didn't wet my bed past the age of three."
    - dllthomas 10y ago
      But then you find yourself sharing a bed with an infant. Source: I'm typing this from a bed I'm sharing with an infant. (I don't actually mean this to be an argument, just fun. "Other people will make type errors" is not the argument I'd make.)
- dllthomas 10y ago
  It seems like the reasoning here is exactly the wrong way round. The number of possible programs is astronomical (though still countable!). The number of possible programs with the correct type is substantially smaller. If we can construct our types and type checking such that the errors we are likely to make are likely to result in ill-typed programs, then we can substantially reduce the number of uncaught errors. More generally, in your comparison you seem to be expecting that a unique error be detected in a unique place. There is no particular reason multiple (or manifold) errors should not be expected to produce an error in the same "nodes in the program's tree".
  - kazinator 10y ago
    I'm looking at it as a search problem. I don't care about the likelihood of a randomly generated program with correct syntax being correctly typed because people don't program that way. But rather this: let's take a correct program of size N (N nodes in the syntax tree) and insert a single error into it and give the modified program to someone to find the error (without giving them the original, of course). If it's a type error, it can be found by searching the space of N nodes. If it can be any defect whatsoever, the search space is the entire state space of the program emanating from all combinations of all possible inputs.
    - dllthomas 10y ago
      > I don't care about the likelihood of a randomly generated program with correct syntax being correctly typed because people don't program that way. Agreed! > But rather this: let's take a correct program of size N (N nodes in the syntax tree) and insert a single error into it and give the modified program to someone to find the error (without giving them the original, of course). I think that's a good approximation. There is some additional structure it discards; I care most about errors that people are likely to make, and about surfacing changes required in likely refactoring. But I expect something that does well at the one is likely to do well enough at the other. > If it's a type error, it can be found by searching the space of N nodes. If it can be any defect whatsoever, the search space is the entire state space of the program emanating from all combinations of all possible inputs. Which is exactly why we want to make as many errors "type errors" as possible (modulo tradeoffs). We'd much, much rather search that smaller space.

by willtim 10y ago

kazinator 10y ago

Although "class" sounds big, in fact there is only a countable number of places (nodes in the program's tree) where you can have a type error. The space in which any error whatsoever can occur is astronomical.

TheDong 10y ago
Let me give an analogy: Claim: "Getting vaccinated stops a whole class of diseases which might kill you" Your rebuttal: Although "class" sounds big, in fact there are only a countable number of viruses that vaccines save you from. The number of ways in which you can die is astronomical. In the above analogy, as in your original statement, you're completely missing the point that the class of errors / class of diseases is an important class and easily preventable, therefore you should do it. In fact, I think what you've said is the reverse of true. Static typing means that there's a chance of an error at each node in the program's tree because a statically typed and statically compiled language ensures that the program can be rendered as an AST before you ship it to your user. A dynamically typed interpreted language can have an error at literally any character in the entire thing, and you don't have "compile-time" to tell you it's not an error. The class of errors that you're saving yourself from is "every single character of this program could be wrong in a way that results in it not even being representable as an AST; there are astronomically many ways that can occur". In addition, it now goes wrong much later. You have to ensure that you've hit every path with testing before you can be even somewhat confident it's valid code, let alone logically correct and bug-free in other ways. A compiled statically-typed language you waste no more time than a compile-cycle to get that minimal assurance.
- dllthomas 10y ago
  "Compiled" and "dynamically typed" are not opposites.
- kazinator 10y ago
  Let me give an analogy: Claim: "Using a plastic liner stops urine from getting into the mattress". My rebuttal: "That's well and good, but I'm sure I didn't wet my bed past the age of three."
  - dllthomas 10y ago
    But then you find yourself sharing a bed with an infant. Source: I'm typing this from a bed I'm sharing with an infant. (I don't actually mean this to be an argument, just fun. "Other people will make type errors" is not the argument I'd make.)
dllthomas 10y ago
It seems like the reasoning here is exactly the wrong way round. The number of possible programs is astronomical (though still countable!). The number of possible programs with the correct type is substantially smaller. If we can construct our types and type checking such that the errors we are likely to make are likely to result in ill-typed programs, then we can substantially reduce the number of uncaught errors. More generally, in your comparison you seem to be expecting that a unique error be detected in a unique place. There is no particular reason multiple (or manifold) errors should not be expected to produce an error in the same "nodes in the program's tree".
- kazinator 10y ago
  I'm looking at it as a search problem. I don't care about the likelihood of a randomly generated program with correct syntax being correctly typed because people don't program that way. But rather this: let's take a correct program of size N (N nodes in the syntax tree) and insert a single error into it and give the modified program to someone to find the error (without giving them the original, of course). If it's a type error, it can be found by searching the space of N nodes. If it can be any defect whatsoever, the search space is the entire state space of the program emanating from all combinations of all possible inputs.
  - dllthomas 10y ago
    > I don't care about the likelihood of a randomly generated program with correct syntax being correctly typed because people don't program that way. Agreed! > But rather this: let's take a correct program of size N (N nodes in the syntax tree) and insert a single error into it and give the modified program to someone to find the error (without giving them the original, of course). I think that's a good approximation. There is some additional structure it discards; I care most about errors that people are likely to make, and about surfacing changes required in likely refactoring. But I expect something that does well at the one is likely to do well enough at the other. > If it's a type error, it can be found by searching the space of N nodes. If it can be any defect whatsoever, the search space is the entire state space of the program emanating from all combinations of all possible inputs. Which is exactly why we want to make as many errors "type errors" as possible (modulo tradeoffs). We'd much, much rather search that smaller space.