4 ms·

It really matters which static type system is in question. SML or Haskell? Yep, like those ones. The languages would not be so useful without their compile tim

It really matters which static type system is in question. SML or Haskell? Yep, like those ones. The languages would not be so useful without their compile time type checking. C? Not worth the trouble. C++? Not worth the tarpit or the trouble. Python? Definitely not keen, that language was much better without the annotations. Typescript people really like but I haven't played with. I'm pleasantly surprised that unsound static + sound dynamic works well. Type annotations are not inherently good. Some type systems add a lot of value, some really don't.

oldpersonintx 3y ago
type ":t" in ghci for many common Haskell types (functions are also types fyi) and tell me if you have the faintest idea what you are reading lots of comments here praising Haskell and Rust frankly seem to be coming from people with a superficial understanding or limited exposure I've had rustc complain about type deductions that were over a line long...that's just one inferred type...you can easily paint yourself into a corner with a type system with no exit other than trying to cajole the right definition out of the compiler and then you copy-paste it and pray
xigoi 3y ago
> C? Not worth the trouble. C++? Not worth the tarpit or the trouble. The OP said strong static type system, so C and C++ are out of the question.
chongli 3y ago
This is not about type annotations, it’s about type systems. You can write Haskell programs without any type annotations. Your program will type check and compile just fine. The value comes from the checks (as well as the inference, documentation, optimization, and everything else a modern type system gives you), which you don’t have to write yourself, you get them for free. People who say they prefer dynamic languages are really just saying ‘no’ to all these free benefits.
- JonChesterfield 3y ago
  If your language is wholly type inferred, and the type system is expressive enough to deal with whatever one wishes to write, it is indeed "free". If you ignore compile time performance, run time performance, and that you're writing in something between Idris and vapourware. Otherwise the cost is merely being unable to write anything that the type checker does not understand, and however long your compiler takes to do the checks on what it does understand. Also a fair chance the whole program must type check before you can see the results of changing a subset. In the worst case you get to hunt down all the unused variables before it'll run the test suite. I prefer dynamic languages. That makes me a heathen on these boards, to be ignored or chastised for my stupidity. Regardless, those benefits do not come for free.
- WJW 3y ago
  Even though I usually fall more on the "types good" side of the discussion, the advantages you listed are not free at all. They come at the cost of at least: - having a compile step in between writing and running your code. This drastically slows down the feedback loop of development. The more your compiler has to check for you, the slower it gets. - being able to run your program in a half-broken state. This may not seem like much of an advantage, but sometimes it is good to just be able to run a broken piece of code to see how it crashes. This is especially important when learning to program, but is still very beneficial when learning a new language or framework, or sometimes for debugging. - As someone who has contributed to the main Haskell compiler, I can definitely confirm that a more complicated type system can slow down development of the language itself too. It takes significantly more effort to grok all the possible interactions as the codebase of the compiler grows. Don't get me wrong, I think encoding and enforcing program properties with types is a great idea that will grow further in the future. But the dynamic languages gained popularity for good reasons, and some of those reasons are still valid today.
ActorNightly 3y ago
>SML or Haskell? Yep, like those ones Not strong enough. If you are proponent of strong typing, you need something that is effectively a theorem prover. I.e when you define a type, you define the scope of the data it can hold, operations on that data, and the resultant types of those operations. That way, when you code compiles, it is by definition "correct". When you accept anything less then that, you are basically making a statement that you are willing to forgo some of that correctness for convenience, which is fine, but that means that no language out there is really good or bad.
- DonaldPShimoda 3y ago
  Theorem provers' type systems are not necessarily stronger than SML's or Haskell's; they are more expressive, which is a separate thing entirely. That said, your position is also just weird to me. Yes, theorem provers have nice type systems that are wonderfully expressive. The trade-off is that some common programming patterns become difficult to use or are even impossible. When it comes to everyday programming, I don't think theorem provers are at a point where they are particularly useful. Not everything needs to be proved formally, and I don't think this position is at odds with the belief that static type systems are generally "better" than dynamic ones.
  - ActorNightly 3y ago
    > The trade-off is that some common programming patterns become difficult to use or are even impossible. Not really. Strong and expressive typing at its core is simply creating data packaging containers that have defined operations on them. It says nothing about logic. You may be referring to the functional programming aspect that comes with strong typed languages, which is related but not the same as strong typing. The point is that typing is just a tool that a programer can use, whether its built into the language or ran statically like MyPy. You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes. However, in the case of strict+explicit typing, the idea is that you wouldn't need tests in the first place, because your code would be correct by nature of compilation.
yxhuvud 3y ago
100% this. Developer experience in a language is a so much bigger question than if it has static types or not.

oldpersonintx 3y ago

type ":t" in ghci for many common Haskell types (functions are also types fyi) and tell me if you have the faintest idea what you are reading lots of comments here praising Haskell and Rust frankly seem to be coming from people with a superficial understanding or limited exposure I've had rustc complain about type deductions that were over a line long...that's just one inferred type...you can easily paint yourself into a corner with a type system with no exit other than trying to cajole the right definition out of the compiler and then you copy-paste it and pray

xigoi 3y ago

> C? Not worth the trouble. C++? Not worth the tarpit or the trouble. The OP said strong static type system, so C and C++ are out of the question.

chongli 3y ago

This is not about type annotations, it’s about type systems. You can write Haskell programs without any type annotations. Your program will type check and compile just fine. The value comes from the checks (as well as the inference, documentation, optimization, and everything else a modern type system gives you), which you don’t have to write yourself, you get them for free. People who say they prefer dynamic languages are really just saying ‘no’ to all these free benefits.

JonChesterfield 3y ago
If your language is wholly type inferred, and the type system is expressive enough to deal with whatever one wishes to write, it is indeed "free". If you ignore compile time performance, run time performance, and that you're writing in something between Idris and vapourware. Otherwise the cost is merely being unable to write anything that the type checker does not understand, and however long your compiler takes to do the checks on what it does understand. Also a fair chance the whole program must type check before you can see the results of changing a subset. In the worst case you get to hunt down all the unused variables before it'll run the test suite. I prefer dynamic languages. That makes me a heathen on these boards, to be ignored or chastised for my stupidity. Regardless, those benefits do not come for free.
WJW 3y ago
Even though I usually fall more on the "types good" side of the discussion, the advantages you listed are not free at all. They come at the cost of at least: - having a compile step in between writing and running your code. This drastically slows down the feedback loop of development. The more your compiler has to check for you, the slower it gets. - being able to run your program in a half-broken state. This may not seem like much of an advantage, but sometimes it is good to just be able to run a broken piece of code to see how it crashes. This is especially important when learning to program, but is still very beneficial when learning a new language or framework, or sometimes for debugging. - As someone who has contributed to the main Haskell compiler, I can definitely confirm that a more complicated type system can slow down development of the language itself too. It takes significantly more effort to grok all the possible interactions as the codebase of the compiler grows. Don't get me wrong, I think encoding and enforcing program properties with types is a great idea that will grow further in the future. But the dynamic languages gained popularity for good reasons, and some of those reasons are still valid today.

ActorNightly 3y ago

>SML or Haskell? Yep, like those ones Not strong enough. If you are proponent of strong typing, you need something that is effectively a theorem prover. I.e when you define a type, you define the scope of the data it can hold, operations on that data, and the resultant types of those operations. That way, when you code compiles, it is by definition "correct". When you accept anything less then that, you are basically making a statement that you are willing to forgo some of that correctness for convenience, which is fine, but that means that no language out there is really good or bad.

DonaldPShimoda 3y ago
Theorem provers' type systems are not necessarily stronger than SML's or Haskell's; they are more expressive, which is a separate thing entirely. That said, your position is also just weird to me. Yes, theorem provers have nice type systems that are wonderfully expressive. The trade-off is that some common programming patterns become difficult to use or are even impossible. When it comes to everyday programming, I don't think theorem provers are at a point where they are particularly useful. Not everything needs to be proved formally, and I don't think this position is at odds with the belief that static type systems are generally "better" than dynamic ones.
- ActorNightly 3y ago
  > The trade-off is that some common programming patterns become difficult to use or are even impossible. Not really. Strong and expressive typing at its core is simply creating data packaging containers that have defined operations on them. It says nothing about logic. You may be referring to the functional programming aspect that comes with strong typed languages, which is related but not the same as strong typing. The point is that typing is just a tool that a programer can use, whether its built into the language or ran statically like MyPy. You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes. However, in the case of strict+explicit typing, the idea is that you wouldn't need tests in the first place, because your code would be correct by nature of compilation.

yxhuvud 3y ago

100% this. Developer experience in a language is a so much bigger question than if it has static types or not.