7 ms·

The discussion over whether strong typing is better than weak typing is settled [1], but not over whether static typing is better than dynamic typing. Adherents

The discussion over whether strong typing is better than weak typing is settled [1], but not over whether static typing is better than dynamic typing. Adherents of static typing thinks that the compiler should check "correctness" by verifying type invariants, adherents of dynamic typing think that is a waste of time. I'm firmly in the latter camp. Because the compiler can't check program correctness only type correctness. Type correctnes is necessary for program correctness, but NOT sufficient. Static typing adherents fail to recognize this, thus falsely believing that static typing guarantees them more than what it actually does (blub). Consider the article's birthdayGreeting example. Author is happy that static typing catcges the birthdayGreeting("John", "20") bug because "20" is not a number. But birthdayGreeting(" ", 123) is not caught (" " is not a name) and neither is birthdayGreeting("Anna," -12335). birthdayGreeting("Anna" 4.5), though, is caught, which arguably is wrong since 4.5 is an age. This is actually very important since "type bugs" are trivially easy to catch, while "semantic bugs" can stay undetected for years. An account balance stored as a uint that overflows, a number that must be prime at a certain program location, but isn't, a list that must not be empty, etc. No, not even dependent types can guarantee these invariants. If you don't believe me, read up on some catastrophic bugs. Those that have caused space ships to explode and cars to crash. To the best of my knowledge, not a single one has been caused by bona fide type errors. In the overwhelming majority of cases, the root cause has been a semantic error. [1] - Most people don't understand that typing is measured over at least two axes, strong/weak and static/dynamic, and continue to conflate weak typing with dynamic typing. C is statically typed and weakly typed. Python is strongly typed and dynamically typed. Javascript is weakly typed and dynamically typed.

scarmig 3y ago
In principal, at least, you could encode all those constraints in the birthday example into the type system. In practice, no one does, partially because existing type systems aren't ergonomic enough to express those constraints for developers to want to use them.
tasn 3y ago
> Consider the article's birthdayGreeting example. Author is happy that static typing catcges the birthdayGreeting("John", "20") bug because "20" is not a number. But birthdayGreeting(" ", 123) is not caught (" " is not a name) and neither is birthdayGreeting("Anna," -12335). birthdayGreeting("Anna" 4.5), though, is caught, which arguably is wrong since 4.5 is an age. Author here. I think your examples illustrate my point rather than provide a counter example. I mentioned later in the post that we validate when creating the type (from e.g. user input) so we know that the `Name` type is always valid (and " ") is not a name. So the type ensures that we have a valid name. So this will definitely be caught in our codebase. As for birthdayGreeting("Anna" 4.5) and birthdayGreeting("Anna," -12335), number means a float in JS so it actually would be valid, though admittedly I had full integers in mind when writing this. Another example of where stricter typing than what TS providers (which Rust does!) would have helped better define the invariant. So in short: the problem in the code there was that I was trying to show a simple example, which means I didn't define all the types as strictly as I normally would have, and it surfaced more bugs that would have been caught with types.
eyelidlessness 3y ago
Many of your examples could definitely be caught by static types, depending on the type system. But that’s less important than… > This is actually very important since "type bugs" are trivially easy to catch This, IMO, is exactly why I’m in the static type camp. It’s so trivial that you can do it declaratively, inline with the code it’s testing, with instant feedback, at every call site and in every downstream expression/statement. A type annotation doesn’t mean my semantic/domain logic is sound, I still have to test that. but it could replace dozens of trivial tests orthogonal to the logic I care about… tests which, let’s face it, few people are going to write exhaustively otherwise.
- perrygeo 3y ago
  The amount of runtime checks and/or tests required to emulate the guarantees of static types is huge. It's perplexing that some people would rather do that manually. But to the point of triviality, static types tend to lull developers into a false sense of security. There are limits to their usefulness. You still need both runtime checks and test-time assertions for your logic. You just need less of them and they provide more value per line of code. But I've never seen a type system capable of expressing the entire problem domain in an ergonomic way. Not even close. For my money, a combination of: static types, property-based testing, unit/integration tests, and an end-to-end test against prod are all required. You can compensate for the lack of one by putting more effort into another but you're really just shuffling the "correctness burden" from one place to another. I like static types because it makes the rest of testing easier. But at some point, you've got to roll up your sleeves and make sure it works IRL.
  - sanderjd 3y ago
    I question this "false sense of security" point. In my experience, people who prefer as much static analysis as possible, mostly based on types, are also more likely to be thinking about invariants and error cases more generally. I would go further to say that anyone who has really adopted a thinking-about-invariants-and-error-cases style of programming has almost certainly become frustrated with the amount of repetitive validation code required to accomplish that in projects with no static analysis of types.
alpaca128 3y ago
> Because the compiler can't check program correctness only type correctness How is this evidence for it being a waste of time? No solution is perfect yet many are worthwhile.
kpozin 3y ago
> read up on some catastrophic bugs. Those that have caused space ships to explode and cars to crash. One of the most famous type errors in recent history did in fact crash a spaceship. https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_of_failure https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_o...
MayeulC 3y ago
> Those that have caused space ships to explode It's funny you should mention this, as it immediately brings [1] to my mind. This well-known incident was due to type-checking, with acceptable ranges defined ahead of time for some types (which resonates with your comment: make birthdayGreeting accept ranges 1-150 or something, easy to do in ADA). There are a few more well-publicized issues with spacecraft that could have been caught with better type-checking, including metric/imperial conversions (why not build the unit into a type? Though the fault probably was with integration testing for [2]). Of course, you are right that type checking can't find every code issue (especially algorithmic), it doesn't replace tests. Instant feedback and type hints are invaluable during the development phase, though. In your example, one could probably replace the first name string by a person type/object, by the way. [1]: https://en.m.wikipedia.org/wiki/Ariane_flight_V88 https://en.m.wikipedia.org/wiki/Ariane_flight_V88 [2]: https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter
- bjourne 3y ago
  Neither of those were "bona fide type errors". The fact that both errors ocurred while using statically typed languages shows that. The orbiter failed because inches were interpreted as centimeters. But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. The Ariane failure was due to a cast of a double to a short resuling in an overflow. Again, not something static typing can catch because it can't statically check the value of an arbitrary double. No, even more types is not the solution. It's not pratical to wrap every measurement in a Meter or Inch type (standardization is one issue, is my Meter type the same as your Meter type?) and it doesn't significantly increase the amount of invariants checked. You still have range issues and you still won't get a statically check PrimeNumber type. I'm not familiar with ADA, but VHDL has similar range constraints which are runtime checked.
  - thfuran 3y ago
    >But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation It doesn't strike me as inherently unreasonable to use fixed point. At any rate, there are languages with built-in unit systems, so you could declare something like float length = 4.5 <m> and get an error if you try to add it to something in a different unit without having to roll your own dimensional analysis framework.
suby 3y ago
You didn't provide an argument for why static typing is not worthwhile, merely that it won't solve all of your problems -- thus, you concluded, dynamic typing is better. Yet static typing does very much catch issues, so I really don't see where you're coming from with this.
- bjourne 3y ago
  If I'm being generous then maybe 5% of my developer time is spent chasing type errors. And then most of those "type" errors would be errors that no reasonable type system would have a chance of catching - like keys missing from associative arrays. I'm competent enough to not need the compiler to tell me banalities like that age is a number or name a string. The overhead of having to deal with types is many times larger than those 5%.
  - _dain_ 3y ago
    >And then most of those "type" errors would be errors that no reasonable type system would have a chance of catching - like keys missing from associative arrays. what? in a language with ADTs and exhaustiveness checking, accessing a key from an associative array will give you back an Option type and the compiler will force you handle the code path where the key is missing. unless I've misunderstood what you meant, this is a canonical showcase of what modern static type systems are good for. and in your parent post: >a list that must not be empty, etc. No, not even dependent types can guarantee these invariants. what do you call haskell's NonEmpty then? https://hackage.haskell.org/package/semigroups-0.18/docs/src/Data-List-NonEmpty.html#NonEmpty https://hackage.haskell.org/package/semigroups-0.18/docs/src... data NonEmpty a = a :| [a] I think you're underestimating what static types can do. it's funny you mention "blub" in that post ...
    - bjourne 3y ago
      So static type system are conservative. If variable v is supposed to have type T and the compiler cannot deduce that it for sure is then a type error is generated. Hence you need option types because static type systems are not powerful enough to deduce whether a given nullable variable actually can be null or not. In effect, the compiler throws its hands in the air and says "Nope too hard, you do it for me." So the programmer has to insert runtime checks in the form of pattern matching clauses for option types even when it is trivial for a human to prove that a reference won't ever be null. The compiler admits defeat and instead forces the programmer to use runtime type checking. It's mostly the same with nominative NonEmpty types. Any value the programmer has instantiated with one of NonEmpty's type constructors have type NonEmpty - everything else don't. For sure, you could create a NonEmpty class in Java too, but it would still be up to the programmer to enforce the type's semantic during program execution. If the variable L has type NonEmpty (list) then it's bloody obvious to a programmer that the expression pop(push(push(L, x), y)) also has type NonEmpty. To a compiler figuring that one out is mostly impossible.
digging 3y ago
I don't understand how you go from "this tool only does 90% of the work I need it to" to "I'll do the whole thing by hand" instead of "I'm fine doing 10% by hand".
- freilanzer 3y ago
  Because arguments like these don't make sense in the first place. "The compiler won't let me compile my code in a static language after changes" does not mean that the compiler in a statically typed language is a hindrance but rather that the same program in a dynamic language has the same structure, but it's hidden and not checked. In other words, the compiler is a safety harness for those factors it can check - even if it cannot check for semantic errors.
sanderjd 3y ago
The specific examples you chose to illustrate this point are interesting, because to me, it is clear that what you want is a `Name` type that always represents a valid name and an `Age` type that always represents a valid age. Then you can put the validation in a single place (the constructors of those types) and write many methods like `birthdayGreeting` that can happily use values of those types without needing to take on the responsibility of validating them. I honestly don't know of a good way to implement this pattern without type checking or at least optional type hints and static analysis. Instead, you can do validation of the input values in every single method, which is hugely burdensome, or you can assume callers are passing you valid values and write tests to make sure it isn't too catastrophic if they don't. I don't find either of these solutions satisfying.
mrkeen 3y ago
Thanks for mentioning blub I guess. If you program in a dynamic language, then you have no choice but to perceive all bugs as runtime bugs. Because every bug you witnessed was a runtime bug, so why would types have helped you? When I program in a typed language, the compiler rejects programs I write all the time. Things like: putting code that can't be rolled-back in the middle of a transaction.
marwis 3y ago
How does [1] in any way support the claim made in first paragraph?
mecha_ghidorah 3y ago
> I'm firmly in the latter camp. Because the compiler can't check program correctness only type correctness. Type correctnes is necessary for program correctness, but NOT sufficient. Static typing adherents fail to recognize this, thus falsely believing that static typing guarantees them more than what it actually does (blub). Uhm. What? I'm a static typing proponent and I have never believed that the compiler will guarantee program correctness. Nobody believes that. They believe it largely eliminates a certain category of error, which it does. You're entitled to your opinion on dynamic vs static typing, but this particular point of yours is just a wild straw man
arp242 3y ago
> I'm firmly in the latter camp. Because the compiler can't check program correctness only type correctness. Type correctnes is necessary for program correctness, but NOT sufficient. Static typing adherents fail to recognize this, That's just not true. Absolutely no one claims that static typing guarantees correctness, because that's ridiculous and obviously nonsense.

scarmig 3y ago

In principal, at least, you could encode all those constraints in the birthday example into the type system. In practice, no one does, partially because existing type systems aren't ergonomic enough to express those constraints for developers to want to use them.

tasn 3y ago

> Consider the article's birthdayGreeting example. Author is happy that static typing catcges the birthdayGreeting("John", "20") bug because "20" is not a number. But birthdayGreeting(" ", 123) is not caught (" " is not a name) and neither is birthdayGreeting("Anna," -12335). birthdayGreeting("Anna" 4.5), though, is caught, which arguably is wrong since 4.5 is an age. Author here. I think your examples illustrate my point rather than provide a counter example. I mentioned later in the post that we validate when creating the type (from e.g. user input) so we know that the `Name` type is always valid (and " ") is not a name. So the type ensures that we have a valid name. So this will definitely be caught in our codebase. As for birthdayGreeting("Anna" 4.5) and birthdayGreeting("Anna," -12335), number means a float in JS so it actually would be valid, though admittedly I had full integers in mind when writing this. Another example of where stricter typing than what TS providers (which Rust does!) would have helped better define the invariant. So in short: the problem in the code there was that I was trying to show a simple example, which means I didn't define all the types as strictly as I normally would have, and it surfaced more bugs that would have been caught with types.

eyelidlessness 3y ago

Many of your examples could definitely be caught by static types, depending on the type system. But that’s less important than… > This is actually very important since "type bugs" are trivially easy to catch This, IMO, is exactly why I’m in the static type camp. It’s so trivial that you can do it declaratively, inline with the code it’s testing, with instant feedback, at every call site and in every downstream expression/statement. A type annotation doesn’t mean my semantic/domain logic is sound, I still have to test that. but it could replace dozens of trivial tests orthogonal to the logic I care about… tests which, let’s face it, few people are going to write exhaustively otherwise.

perrygeo 3y ago
The amount of runtime checks and/or tests required to emulate the guarantees of static types is huge. It's perplexing that some people would rather do that manually. But to the point of triviality, static types tend to lull developers into a false sense of security. There are limits to their usefulness. You still need both runtime checks and test-time assertions for your logic. You just need less of them and they provide more value per line of code. But I've never seen a type system capable of expressing the entire problem domain in an ergonomic way. Not even close. For my money, a combination of: static types, property-based testing, unit/integration tests, and an end-to-end test against prod are all required. You can compensate for the lack of one by putting more effort into another but you're really just shuffling the "correctness burden" from one place to another. I like static types because it makes the rest of testing easier. But at some point, you've got to roll up your sleeves and make sure it works IRL.
- sanderjd 3y ago
  I question this "false sense of security" point. In my experience, people who prefer as much static analysis as possible, mostly based on types, are also more likely to be thinking about invariants and error cases more generally. I would go further to say that anyone who has really adopted a thinking-about-invariants-and-error-cases style of programming has almost certainly become frustrated with the amount of repetitive validation code required to accomplish that in projects with no static analysis of types.

alpaca128 3y ago

> Because the compiler can't check program correctness only type correctness How is this evidence for it being a waste of time? No solution is perfect yet many are worthwhile.

kpozin 3y ago

> read up on some catastrophic bugs. Those that have caused space ships to explode and cars to crash. One of the most famous type errors in recent history did in fact crash a spaceship. https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_of_failure https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_o...

MayeulC 3y ago

> Those that have caused space ships to explode It's funny you should mention this, as it immediately brings [1] to my mind. This well-known incident was due to type-checking, with acceptable ranges defined ahead of time for some types (which resonates with your comment: make birthdayGreeting accept ranges 1-150 or something, easy to do in ADA). There are a few more well-publicized issues with spacecraft that could have been caught with better type-checking, including metric/imperial conversions (why not build the unit into a type? Though the fault probably was with integration testing for [2]). Of course, you are right that type checking can't find every code issue (especially algorithmic), it doesn't replace tests. Instant feedback and type hints are invaluable during the development phase, though. In your example, one could probably replace the first name string by a person type/object, by the way. [1]: https://en.m.wikipedia.org/wiki/Ariane_flight_V88 https://en.m.wikipedia.org/wiki/Ariane_flight_V88 [2]: https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter

bjourne 3y ago
Neither of those were "bona fide type errors". The fact that both errors ocurred while using statically typed languages shows that. The orbiter failed because inches were interpreted as centimeters. But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. The Ariane failure was due to a cast of a double to a short resuling in an overflow. Again, not something static typing can catch because it can't statically check the value of an arbitrary double. No, even more types is not the solution. It's not pratical to wrap every measurement in a Meter or Inch type (standardization is one issue, is my Meter type the same as your Meter type?) and it doesn't significantly increase the amount of invariants checked. You still have range issues and you still won't get a statically check PrimeNumber type. I'm not familiar with ADA, but VHDL has similar range constraints which are runtime checked.
- thfuran 3y ago
  >But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation It doesn't strike me as inherently unreasonable to use fixed point. At any rate, there are languages with built-in unit systems, so you could declare something like float length = 4.5 <m> and get an error if you try to add it to something in a different unit without having to roll your own dimensional analysis framework.

suby 3y ago

You didn't provide an argument for why static typing is not worthwhile, merely that it won't solve all of your problems -- thus, you concluded, dynamic typing is better. Yet static typing does very much catch issues, so I really don't see where you're coming from with this.

bjourne 3y ago
If I'm being generous then maybe 5% of my developer time is spent chasing type errors. And then most of those "type" errors would be errors that no reasonable type system would have a chance of catching - like keys missing from associative arrays. I'm competent enough to not need the compiler to tell me banalities like that age is a number or name a string. The overhead of having to deal with types is many times larger than those 5%.
- _dain_ 3y ago
  >And then most of those "type" errors would be errors that no reasonable type system would have a chance of catching - like keys missing from associative arrays. what? in a language with ADTs and exhaustiveness checking, accessing a key from an associative array will give you back an Option type and the compiler will force you handle the code path where the key is missing. unless I've misunderstood what you meant, this is a canonical showcase of what modern static type systems are good for. and in your parent post: >a list that must not be empty, etc. No, not even dependent types can guarantee these invariants. what do you call haskell's NonEmpty then? https://hackage.haskell.org/package/semigroups-0.18/docs/src/Data-List-NonEmpty.html#NonEmpty https://hackage.haskell.org/package/semigroups-0.18/docs/src... data NonEmpty a = a :| [a] I think you're underestimating what static types can do. it's funny you mention "blub" in that post ...
  - bjourne 3y ago
    So static type system are conservative. If variable v is supposed to have type T and the compiler cannot deduce that it for sure is then a type error is generated. Hence you need option types because static type systems are not powerful enough to deduce whether a given nullable variable actually can be null or not. In effect, the compiler throws its hands in the air and says "Nope too hard, you do it for me." So the programmer has to insert runtime checks in the form of pattern matching clauses for option types even when it is trivial for a human to prove that a reference won't ever be null. The compiler admits defeat and instead forces the programmer to use runtime type checking. It's mostly the same with nominative NonEmpty types. Any value the programmer has instantiated with one of NonEmpty's type constructors have type NonEmpty - everything else don't. For sure, you could create a NonEmpty class in Java too, but it would still be up to the programmer to enforce the type's semantic during program execution. If the variable L has type NonEmpty (list) then it's bloody obvious to a programmer that the expression pop(push(push(L, x), y)) also has type NonEmpty. To a compiler figuring that one out is mostly impossible.

digging 3y ago

I don't understand how you go from "this tool only does 90% of the work I need it to" to "I'll do the whole thing by hand" instead of "I'm fine doing 10% by hand".

freilanzer 3y ago
Because arguments like these don't make sense in the first place. "The compiler won't let me compile my code in a static language after changes" does not mean that the compiler in a statically typed language is a hindrance but rather that the same program in a dynamic language has the same structure, but it's hidden and not checked. In other words, the compiler is a safety harness for those factors it can check - even if it cannot check for semantic errors.

sanderjd 3y ago

The specific examples you chose to illustrate this point are interesting, because to me, it is clear that what you want is a `Name` type that always represents a valid name and an `Age` type that always represents a valid age. Then you can put the validation in a single place (the constructors of those types) and write many methods like `birthdayGreeting` that can happily use values of those types without needing to take on the responsibility of validating them. I honestly don't know of a good way to implement this pattern without type checking or at least optional type hints and static analysis. Instead, you can do validation of the input values in every single method, which is hugely burdensome, or you can assume callers are passing you valid values and write tests to make sure it isn't too catastrophic if they don't. I don't find either of these solutions satisfying.

mrkeen 3y ago

Thanks for mentioning blub I guess. If you program in a dynamic language, then you have no choice but to perceive all bugs as runtime bugs. Because every bug you witnessed was a runtime bug, so why would types have helped you? When I program in a typed language, the compiler rejects programs I write all the time. Things like: putting code that can't be rolled-back in the middle of a transaction.

marwis 3y ago

How does [1] in any way support the claim made in first paragraph?

mecha_ghidorah 3y ago

> I'm firmly in the latter camp. Because the compiler can't check program correctness only type correctness. Type correctnes is necessary for program correctness, but NOT sufficient. Static typing adherents fail to recognize this, thus falsely believing that static typing guarantees them more than what it actually does (blub). Uhm. What? I'm a static typing proponent and I have never believed that the compiler will guarantee program correctness. Nobody believes that. They believe it largely eliminates a certain category of error, which it does. You're entitled to your opinion on dynamic vs static typing, but this particular point of yours is just a wild straw man

arp242 3y ago

> I'm firmly in the latter camp. Because the compiler can't check program correctness only type correctness. Type correctnes is necessary for program correctness, but NOT sufficient. Static typing adherents fail to recognize this, That's just not true. Absolutely no one claims that static typing guarantees correctness, because that's ridiculous and obviously nonsense.