Honestly, this is probably not too bad if we’re talking about Haskell or Purescript. They say, “if it compiles, ship it” because these languages are rigorous about types at compilation time.
That’s pure nonsense. Types don’t tell you that your code is correct, they just tell you that your types align. Here’s a perfect example of where the mentality that if it compiles, ship it leads you in practice.
Haskell bro wrote a benchmark comparing Haskell with C implementation of websockets. The initial results looked extremely favorable for Haskell. However, it turned out that the Haskell implementation failed to deliver messages reliably, dropping 98% of the messages it received.
Furthermore, static typing is that it’s inherently more limiting in terms of expressiveness because you’re limited to a set of statements that can be verified by the type checker effectively. This is a subset of all valid statements that you’re allowed to make in a dynamic language.
So, a static language will often force you to write code for the benefit of the type checker as opposed to the human reader because you have to write code in a way that the type checker can understand. This can lead to code that’s more difficult to reason about, and you end up with logic errors that are much harder to debug than simple type mismatches. People can also get a false sense of confidence from their type system as seen here where the author assumed the code was correct because it compiled, but in fact it wasn’t doing anything useful.
At the same time, there is no automated way to check the type definitions themselves and as you encode more constraints via types you end up with a meta program describing your program, and there is nothing to help you know whether that program itself is correct. Consider a fully typed insertion sort in Idris. It’s nearly 300 lines long! I could understand a 10 line Python version in its entirety and be able to guarantee that it works as intended much easier than the Idris one.
Honestly, this is probably not too bad if we’re talking about Haskell or Purescript. They say, “if it compiles, ship it” because these languages are rigorous about types at compilation time.
Because if the types are correct, it’s mostly bug free already, right?
Yeah. and since it is so strict, it’s pretty satisfying when it actually does compile.
That’s pure nonsense. Types don’t tell you that your code is correct, they just tell you that your types align. Here’s a perfect example of where the mentality that if it compiles, ship it leads you in practice.
Haskell bro wrote a benchmark comparing Haskell with C implementation of websockets. The initial results looked extremely favorable for Haskell. However, it turned out that the Haskell implementation failed to deliver messages reliably, dropping 98% of the messages it received.
Furthermore, static typing is that it’s inherently more limiting in terms of expressiveness because you’re limited to a set of statements that can be verified by the type checker effectively. This is a subset of all valid statements that you’re allowed to make in a dynamic language.
So, a static language will often force you to write code for the benefit of the type checker as opposed to the human reader because you have to write code in a way that the type checker can understand. This can lead to code that’s more difficult to reason about, and you end up with logic errors that are much harder to debug than simple type mismatches. People can also get a false sense of confidence from their type system as seen here where the author assumed the code was correct because it compiled, but in fact it wasn’t doing anything useful.
At the same time, there is no automated way to check the type definitions themselves and as you encode more constraints via types you end up with a meta program describing your program, and there is nothing to help you know whether that program itself is correct. Consider a fully typed insertion sort in Idris. It’s nearly 300 lines long! I could understand a 10 line Python version in its entirety and be able to guarantee that it works as intended much easier than the Idris one.