4 ms·

Why do you say that static type systems are a "premature optimization"? On its face, that seems like a (very spicy) opinion that's been stated as fact.

auggierose 3y ago
It is a fact, that is why I state it as one. You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of times myself, and it is a good way to waste time and tell yourself you are productive. Yes, I am also looking at all the "let's rewrite stuff in Rust" projects. Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about. You are spending your time trying to shoehorn your solution into somebody else's idea of correctness, who doesn't really know anything about your program at hand. That's why I like TypeScript, its type system is expressive enough for many simple correctness checks I actually care about, while at the same time not getting (too much, and with the above caveats) in the way of how I think about what I build. It is especially clear to me that static type systems are dinosaurs of the past. The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset.
- naasking 3y ago
  > Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about. You're neglecting that these guardrails guide you towards solutions that can be naturally expressed and checked by the language. That's a feature, not a bug. > The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset. Yeah, except for logical consistency or soundness, but who cares about that?
  - auggierose 3y ago
    No, I don't neglect that. These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. There is a lot of religion and faith involved here. I care a lot for logical consistency and soundness, probably more than anyone else you know. But it is wrong to think that static type systems are the best way towards this. Logic is the best way towards this, and static type systems are just one way of implementing logic, and not the best one. Especially in programming, what static type systems were really good at, was automating some correctness checks. I believe in a future where automation gets so good that static type systems become a hindrance, and where their benefit vanishes when weighed up against your freedom to express things as they really are.
    - naasking 3y ago
      > These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. "Best solution" is a fantasy. Any solution must be expressed in a language with concrete semantics, but there is no best language for all possible problems. This was the lesson of Kolmogorov complexity. Therefore, we will always necessarily be using a suboptimal language, and we should let go of any wish for ill-defined optimality. We should instead use a language that guides towards engineering good solutions to problems with desirable properties. Sometimes that might mean strict control over resources (as with Rust), sometimes that isn't necessary (so OCaml,F#, etc. would do). An empirical fact of engineering is that most mistakes people make are trivial, eg. typos, one off errors, forgetfulness to change code in all relevant places during refactoring, etc. Good abstractions enforced by static types solve all of these problems, allowing you to focus on the core problem without being bothered that you might have missed some silly details. Yes the compiler bothers you to correct these details, but this is typically simple mechanistic work that nevertheless can't be automated by any other language without sacrificing other desirable properties. I'm not going to argue that any static type system is better than no static types, because it's easy to invent a bad type system. We've had pretty damn good type systems since the 70s though, they just didn't see much use until recently.
      - 3y ago
- lolinder 3y ago
  > You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of times myself This is where I think the commenter towards the top of this thread has it right: > If your style is to hack hack hack until it’s right, yeah, types are challenging. If your style is to think first about types, you can also create guardrails in your code that naturally create the correct thing. Your experience with static typing is that of someone whose personal style is to write code as an exploratory process while you're trying to figure out what to build, and from the sound of it you were trying to do that in something like Java before you switched to TypeScript. And I completely agree—that style is a terrible match for a Java-like type system. But there are type systems besides TypeScript that are much more flexible than the kind that you're thinking of, and there are styles of software engineering that don't involve extensive prototyping as part of the development process. Those styles—typically slower and data-centric—combine really well with strong and flexible type systems (even something like modern Java with sealed interface goes a long way), and you're doing yourself a disservice by assuming that everyone who uses those styles is just wasting a lot of time.
  - auggierose 3y ago
    I've been programming with Standard ML pretty much since 1995, so I know a thing or two about powerful type systems. Of course there are different kinds of software and different kinds of styles to write this software. Some software needs a correctness proof, other software doesn't, because if it seems to work, that is good enough. If your type system aligns well with the kind of correctness you need for your software, sure, that's good, go for it. A type system is better than nothing at all (that's why I much prefer TypeScript over JavaScript), but it is only an approximation of what you really want (your program fulfils its purpose). If that approximation is good enough for you and your problem domain, fine. Just be aware that the time you spend thinking about how to best fit of what you want to do into your type system, is probably not the best way to work on what to build and how to build it, although it might feel to you that way.
    - IshKebab 3y ago
      > if it seems to work, that is good enough I think that's where many people would disagree with you. Also static types are not only about correctness. They also greatly help with understanding, documentation and navigation. The two biggest third party codebases I've contributed to are VSCode and Gitlab. VSCode was about 10x easier than Gitlab simply because I spent so much time in Gitlab just trying to find the code that a function called, or the code that called a function. (I think Ruby also encourages ungreppable code styles which makes this even worse.) In VSCode it was pretty much just one click. (Occasionally more because of abstract interfaces, but even then way way nicer.) Anyway yeah obviously if you don't really care about your code working or being readable then you are going to feel like static types are a waste of your time. That's kind of like saying that showering is a waste of time because you don't need to be clean.

auggierose 3y ago

It is a fact, that is why I state it as one. You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of times myself, and it is a good way to waste time and tell yourself you are productive. Yes, I am also looking at all the "let's rewrite stuff in Rust" projects. Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about. You are spending your time trying to shoehorn your solution into somebody else's idea of correctness, who doesn't really know anything about your program at hand. That's why I like TypeScript, its type system is expressive enough for many simple correctness checks I actually care about, while at the same time not getting (too much, and with the above caveats) in the way of how I think about what I build. It is especially clear to me that static type systems are dinosaurs of the past. The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset.

naasking 3y ago
> Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about. You're neglecting that these guardrails guide you towards solutions that can be naturally expressed and checked by the language. That's a feature, not a bug. > The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset. Yeah, except for logical consistency or soundness, but who cares about that?
- auggierose 3y ago
  No, I don't neglect that. These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. There is a lot of religion and faith involved here. I care a lot for logical consistency and soundness, probably more than anyone else you know. But it is wrong to think that static type systems are the best way towards this. Logic is the best way towards this, and static type systems are just one way of implementing logic, and not the best one. Especially in programming, what static type systems were really good at, was automating some correctness checks. I believe in a future where automation gets so good that static type systems become a hindrance, and where their benefit vanishes when weighed up against your freedom to express things as they really are.
  - naasking 3y ago
    > These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. "Best solution" is a fantasy. Any solution must be expressed in a language with concrete semantics, but there is no best language for all possible problems. This was the lesson of Kolmogorov complexity. Therefore, we will always necessarily be using a suboptimal language, and we should let go of any wish for ill-defined optimality. We should instead use a language that guides towards engineering good solutions to problems with desirable properties. Sometimes that might mean strict control over resources (as with Rust), sometimes that isn't necessary (so OCaml,F#, etc. would do). An empirical fact of engineering is that most mistakes people make are trivial, eg. typos, one off errors, forgetfulness to change code in all relevant places during refactoring, etc. Good abstractions enforced by static types solve all of these problems, allowing you to focus on the core problem without being bothered that you might have missed some silly details. Yes the compiler bothers you to correct these details, but this is typically simple mechanistic work that nevertheless can't be automated by any other language without sacrificing other desirable properties. I'm not going to argue that any static type system is better than no static types, because it's easy to invent a bad type system. We've had pretty damn good type systems since the 70s though, they just didn't see much use until recently.
    - 3y ago
lolinder 3y ago
> You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of times myself This is where I think the commenter towards the top of this thread has it right: > If your style is to hack hack hack until it’s right, yeah, types are challenging. If your style is to think first about types, you can also create guardrails in your code that naturally create the correct thing. Your experience with static typing is that of someone whose personal style is to write code as an exploratory process while you're trying to figure out what to build, and from the sound of it you were trying to do that in something like Java before you switched to TypeScript. And I completely agree—that style is a terrible match for a Java-like type system. But there are type systems besides TypeScript that are much more flexible than the kind that you're thinking of, and there are styles of software engineering that don't involve extensive prototyping as part of the development process. Those styles—typically slower and data-centric—combine really well with strong and flexible type systems (even something like modern Java with sealed interface goes a long way), and you're doing yourself a disservice by assuming that everyone who uses those styles is just wasting a lot of time.
- auggierose 3y ago
  I've been programming with Standard ML pretty much since 1995, so I know a thing or two about powerful type systems. Of course there are different kinds of software and different kinds of styles to write this software. Some software needs a correctness proof, other software doesn't, because if it seems to work, that is good enough. If your type system aligns well with the kind of correctness you need for your software, sure, that's good, go for it. A type system is better than nothing at all (that's why I much prefer TypeScript over JavaScript), but it is only an approximation of what you really want (your program fulfils its purpose). If that approximation is good enough for you and your problem domain, fine. Just be aware that the time you spend thinking about how to best fit of what you want to do into your type system, is probably not the best way to work on what to build and how to build it, although it might feel to you that way.
  - IshKebab 3y ago
    > if it seems to work, that is good enough I think that's where many people would disagree with you. Also static types are not only about correctness. They also greatly help with understanding, documentation and navigation. The two biggest third party codebases I've contributed to are VSCode and Gitlab. VSCode was about 10x easier than Gitlab simply because I spent so much time in Gitlab just trying to find the code that a function called, or the code that called a function. (I think Ruby also encourages ungreppable code styles which makes this even worse.) In VSCode it was pretty much just one click. (Occasionally more because of abstract interfaces, but even then way way nicer.) Anyway yeah obviously if you don't really care about your code working or being readable then you are going to feel like static types are a waste of your time. That's kind of like saying that showering is a waste of time because you don't need to be clean.