Hacker News Reader

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.

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.

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.

Agreed. I was more rebutting the "If it compiles, it works" mentality - which is not true for anything other than trivial examples. You still need to test that the compiled artifact actually works in a real setting, where "works" is domain-specific and defined by user's perception of value.

Right. But I'm saying that I don't think that mentality actually exists. I think the mentality of people who prefer static analysis is more like "if it compiles, it has passed a huge number of test cases that I'm really glad I didn't have to write myself". But "if it compiles, it works" is a more pithy short-hand for that :)

In a dynamically language you need 100% test coverage, because misspelling a variable name turns into a runtime error.

On large projects this can be a problem. I worked on a Python server some years ago, and with every large program that supports exceptions, there's a catch block somewhere that silently eats the exceptions it doesn't process. Well, some modules were loaded dynamically, so my first spelling mistake (and second and third...) took quite a while to debug because things just didn't work, the code didn't get executed, but there were no errors. This also ate syntax errors, too, since that is also an exception. So if you edited the file, you had no idea if things actually still worked (or even compiled!) until you tested the functionality from the file.

> 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.

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.

> 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

[2]: https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter

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.

>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.

Of course, fixed point would have been a reasonable choice too. But here is my point. Someone who likes testing could say "This bug would have been caught with better testing". Someone who likes static typing could say "This bug would have been caught if they had used an esoteric type system with support for physical quantities." ... Which no one uses. Thus, you have an argument between something real and realistic, and something imagined and unrealistic.

That you aren't familiar with something hardly makes it imaginary. That exact formulation of unit system is, I think, pretty uncommon, but there are widely used languages (vhdl) where uniting is more directly part of the type system and widely used uniting systems as libraries (boost) where it is not directly a language feature.

VHDL physical types are nothing more than annotated integers. Making them completely useless for general arithmetic. You could not use them for converting from say Celsius to Fahrenheiht. It's cute that you bring up Boost which contains everything and the kitchen sink as evidence of "widely used". Show me a 3d engine that uses physical units for distance calculations. No one does it because it is a horrible idea.

How about "This bug would have been caught if instead of storing the distance in a float, they stored it in a struct/class that also contained an enum defining the units". Just about any language could handle that.

> The fact that both errors ocurred while using statically typed languages shows that

Obviously it doesn't, since you can make a statically typed language program where every variable is a string map and every function takes variable args, and have no help from your compiler at any time because every type is always the right type. Sounds stupid, but in fact this is what happened in the examples.

The examples are bona fide type errors, because even though a statically typed language is used, multiple different types of numbers got the same static type causing the issue. So the people here were offered the solution to their problem from their domain (two types of numbers), choose to use dynamic typing (make both a float even though they're different things), causing the compiler to have no way of statically checking their code, and that caused a bug. It's the opposite of a counter example.

It is in fact the absence of enough typing that caused these issues. How much more typing do you need :)

In other words: types were not a deciding factor.

Ultimately bugs cannot be prevented by having a type system. We make mistakes regardless of static or dynamic types.

We can argue it's because of the lack of types, tests, oversight and so on. I'd argue nothing can force a programmer to design a perfect system.

>The examples are bona fide type errors

I'd disagree because those are logical errors. You can represent those as different types with a type system, but you could also not use a type system and convert those values properly. Whether we represent them as different types or not is an implementation choice.

Those can be considered "type errors" (or missing types? a type of primitive obsession?) in a typed language. But it's still an issue with the implementation's logic.

In other words: the seatbelt is not a deciding factor.

Ultimately deaths cannot be prevented by seatbelts. People will die regardless whether they wear a seatbelt or not.

We can argue its because of a lack of seatbelts, roll cages, airbags and so on. I'd argue nothing can force force a person to be perfectly safe while driving.

> The examples are bona fide safety issues

I'd disagree because those are driving errors. You can present those as cars missing safety features, but you could also not use those safety systems and just drive carefully. Whether we use safety systems or not is a design choice.

Those can be considered "safety issues" (or missing safety? a type of safety obsession?) in a safety design perspective. But it's still an issue with the driver's behavior.

bit of hyperbole for flavour:

If we could just ditch the heavy roll cage, we could go much faster!

I don't see how this adds to the discussion. Second time this week for me where people are connecting programing discussions with people dying.

But sure, let's pretend this is a real argument.

Typed languages are not at all like seatbelts. They aren't an easy safety feature you can use within a second and suddenly X% of bugs are prevented. No research shows that it prevents the bugs we actually care about, and they don't deal with runtime issues that actually kills people like the one discussed in this thread.

Ok let me make it more clear then:

Type checking is a programming safety feature, and its trivial to argue in any domain that a safety feature is optional. Its always trivial to argue this because safety is never a functional requirement, so it is never guaranteed to be needed for anything, and its easy to point out that regardless of safety, mistakes will happen, and that safety does not prevent all mistakes. All of this is trivial, and can be applied to any safety measure, this is why I brought up seatbelts: to show that your argument depends strongly on the context of where the safety applies, and the sacrifices that have to be made to gain that safety.

Which brings me to my second point: safety is always a tradeoff. Saying things like "perfectly safe" is completely void of meaning since nothing is ever perfectly safe, basing an argument on the fact that we cannot be perfectly safe is saying we shouldn't care about seatbelts because we're all gonna die anyway. Safety is a tradeoff and you should consider the up and downsides when you talk about it, always. So on your point:

> They aren't an easy safety feature you can use within a second and suddenly X% of bugs are prevented

Actually thats exactly what they are, because they will stop you from compiling a program that would have bugs in a dynamically typed system. Do they prevent all bugs? No, nobody is saying that. Its also easy to find how, just by googling: https://stackoverflow.com/a/27791387

> No research shows that it prevents the bugs we actually care about

No research shows anything about software, there is no research on software, stop deflecting.

> they don't deal with runtime issues that actually kills people like the one discussed in this thread

This thread is full of people suggesting type-safe fixes that would've prevented this, I'm not sure how you're still arguing that typing wouldn't help here. Again, maybe you don't want to use it because its too much work or some other kind of tradeoff you don't want to make, fine. But if you keep suggesting that types wouldn't work here you simply don't understand types.

> Saying things like "perfectly safe"

I've never said that. It's always about trade-offs, but simply adding a typed system would not have prevented the issue, as it was already built in a typed system.

My whole point is not pro or against typed languages. It's that we need to move beyond that.

> Actually thats exactly what they are, because they will stop you from compiling a program that would have bugs in a dynamically typed system.

It totally depends. It only stops you if you are diligent enough to write programs with a very good type structure and hopefully you don't have any logical mistakes. If you type everything with primitives like uint you can still have a compiling program that's incorrect.

> This thread is full of people suggesting type-safe fixes that would've prevented this

And I could suggest fixes without typed languages that would also have prevented this, like better testing. The point is that a type system does not inherently change anything. It's still up to the developer and the systems around to be good enough to prevent catastrophes from happening.

Using types is most definitely one way of solving the issue, if implemented correctly. But the exact same could be done with a dynamic language.

> But if you keep suggesting that types wouldn't work here you simply don't understand types

Sure... I don't understand types ;)

In any case, I never said types wouldn't work here. Read my comments again. I said types are not the determining factor. The fact that this happened in a typed language simply cannot be overstated. Using a typed language or not affects many variables but it's not what will ultimately decide if a critical piece of software will kill someone or not.

> My whole point is not pro or against typed languages. It's that we need to move beyond that.

Ok, once you know where to move to we can consider that as a good solution. Until then, lets just use types, its the best tool we have.

Restated: car has seatbelts, seatbelts were not used, people got injured, hence "seatbelts were not a deciding factor, we need to move beyond that". OK, sure, I can say the same of whatever you intend to move to, and we will have wasted a lot of air to no benefit.

> 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.

Types are not runtime representations, and any good nominal type system will allow you to avoid this sort of problem easily. For example, this Haskell code

    newtype Inches = Inches Double deriving Num
    newtype Centimeters = Centimeters Double deriving Num
    
    a :: Centimeters
    a = Centimeters 1.0

    b :: Inches
    b = Inches 1.0

    fine = a + a
    alsoFine = b + b
    mistake = a + b

will give this type error

    Couldn't match expected type ‘Centimeters’ with actual type ‘Inches’
      In the second argument of ‘(+)’, namely ‘b’
      In the expression: a + b
      In an equation for ‘mistake’: mistake = a + b

but both `a` and `b` will be doubles at runtime.

That is why I wrote "in any reasonable implementation". Embedding physical quantities in the type system is possible in many language but is not practical. Hence why safety-critical software doesn't contain declarations like yours. For example, what is the type of Inch * Inch? What is the type of Inch / Inch? Sure, perhaps if NASA and their subcontractors had used a common well-developed physical quantities library then the bug could have been caught during compile-time. But I think it is a moot point since most people don't use such libraries.

> For example, what is the type of Inch * Inch?

An area, inch^2.

> What is the type of Inch / Inch?

A unitless ratio?

I don't understand why this is not practical in safety-critical software. nyssos demonstrated what I believe is the right way to do it.

These semantics make the type incompatible with the Num class and attempting to plug your type into, say, a run of the mill ode solver likely won't do what you want. So you have two options. 1) Rewrite all code to become "quantity aware". Multiplying two Matrix[Inch] results in a Matrix[Inch2] and so on. 2) Litter your code with floatToInch and inchToFloat conversions. I think you can see why both options suck? If you really can't, then perhaps try finding some safety-critical software that relies on "physical quantity types" in some form or another?

> I think you can see why both options suck?

Do they suck more than losing spacecraft?

Absolutely. Littering a code base with centimeter-to-inch conversions or rewriting every numeric computation to become unit aware would for sure have caused more bugs than it would have prevented.

It is possible and practical. For example the <chrono> in the C++ standard library.

Very true, it is possible and practical, and chrono is a good example. But you can take a similar approach in dynamically typed languages as well. It wouldn't be hard to design a library that did something like this:

  some_duration = minutes(3) + seconds(2)

Of course that doesn't change the fact that any function receiving a duration would only raise type errors at runtime. For instance, someone could try to pass the number of seconds as an integer rather than as a duration:

  remind_me_after(182)

But any semantic testing would automatically catch type errors as well. remind_me_after would fail every single time assuming the implementation would be something like this:

  def remind_me_after(duration):
    reminder_api.set_reminder(now().as_seconds() + duration.as_seconds())

I think this is the reason why studies don't show huge differences in defects between dynamically and statically typed languages. You have to do semantic tests anyway, and they would cover most* type errors as well.

What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct because some semantic edge cases are not covered by the tests.

* Not all of them because semantic tests could theoretically succeed by accident for some specific values that have incorrect types.

> What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct because some semantic edge cases are not covered by the tests.

It can also mean that the code has incorrect subprograms, but that the program as a whole is protected from them by some hard to analyze condition. As an extreme example, one of these two programs "works":

    if goldbachConjectureCounterexampleExists() then print("Hello world!") else launchMissiles()

    if goldbachConjectureCounterexampleDoesNotExist() then print("Hello world!") else launchMissiles()

but I don't know which and neither does the compiler. Rejecting them is a feature, not a bug.

> 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.

They would not always be stored as flat floats. You could have type aliases for both values (type alias inch = float, the same for cm) and have not a flat float but an inch or cm as a type. Or, even better, F# has type support for such values: https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref...

> 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.

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.

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%.

>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 NonEmpty a = a :| [a]

I think you're underestimating what static types can do. it's funny you mention "blub" in that post ...

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.

> 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.

Option types serve other purposes, like composability; tracing program flow can determine the points where a nullable type either (a) will always be null, or (b) will never be null, and many type checkers for type systems with nullable types (or, more generally, non-discriminated unions, nullable types are just one example.)

> 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

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".

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.

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.

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.

> 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_o...

> 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.

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