3 ms·

> When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem wit

> When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in. Do you have any realistic concrete examples of this? I find this happens very rarely myself (maybe once every few thousand lines of code) and just involves adding a small amount of code along the lines of "throw 'Unexpected error' // this should never happen because ...". > The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. For me, type errors for where you've mixed up e.g. string, number or object variables or where you've forgotten to check if a variable is null/undefined before you use it are incredibly common compared to the rare times the type system gets in your way. You would have to (and most wouldn't) write many automated tests to catch all those potential errors if you weren't using a type system for similar robustness. Throwing all that away because of the rare case the type system obstructs you doesn't make any sense to me. I still think if you're regularly writing code that is hard to justify to a mainstream type checker you're more than likely doing something very wrong and writing code that is hard for others to understand. I'd love to see a realistic counterexample.

yorwba 9y ago
I did not intend to imply that I'm regularly writing code that's hard to justify to a type checker. In fact, most of the code I write is in statically typed languages (I'm not some kind of dynamic typing zealot), so I tend to avoid situations that could never typecheck before they occur. However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. Since those programs are so simple that a handful of test cases is enough for 100% path coverage, if the program runs correctly on one case, it's almost guaranteed to run correctly for all others. (Similar to Haskell's "if it compiles, it runs".) Statically checking for type correctness would be pointless, because you can just run the program to find out. It then becomes quite natural to e.g. apply type-modifying transformations in-place, which most type checkers wouldn't allow, since they assume a single fixed type rather than a progression of different types during different stages. (You can get around that, of course, but it requires constantly recreating essentially identical objects to give them a new type.) For an example of a project (not written by me) where the type checker's rejection of a correctly working program precluded the use of a type checker, see http://www.oilshell.org/blog/2016/11/30.html http://www.oilshell.org/blog/2016/11/30.html
- seanwilson 9y ago
  > However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. I agree for small utilities and code that's acting as glue between layers that it's convenient to have languages that are loose with what they accept because you can usually manually and exhaustively QA them and because you have no other choice when connecting languages without static type systems. Once you have a large and complex app though, strong typing makes you so much more productive that I honestly can't understand how anyone could argue against strong types.

yorwba 9y ago

I did not intend to imply that I'm regularly writing code that's hard to justify to a type checker. In fact, most of the code I write is in statically typed languages (I'm not some kind of dynamic typing zealot), so I tend to avoid situations that could never typecheck before they occur. However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. Since those programs are so simple that a handful of test cases is enough for 100% path coverage, if the program runs correctly on one case, it's almost guaranteed to run correctly for all others. (Similar to Haskell's "if it compiles, it runs".) Statically checking for type correctness would be pointless, because you can just run the program to find out. It then becomes quite natural to e.g. apply type-modifying transformations in-place, which most type checkers wouldn't allow, since they assume a single fixed type rather than a progression of different types during different stages. (You can get around that, of course, but it requires constantly recreating essentially identical objects to give them a new type.) For an example of a project (not written by me) where the type checker's rejection of a correctly working program precluded the use of a type checker, see http://www.oilshell.org/blog/2016/11/30.html http://www.oilshell.org/blog/2016/11/30.html

seanwilson 9y ago
> However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. I agree for small utilities and code that's acting as glue between layers that it's convenient to have languages that are loose with what they accept because you can usually manually and exhaustively QA them and because you have no other choice when connecting languages without static type systems. Once you have a large and complex app though, strong typing makes you so much more productive that I honestly can't understand how anyone could argue against strong types.