4 ms·

Started reading this and was disappointed to find the same disingenuous claims about strong static type systems. I say disingenuous because the people that esp

Started reading this and was disappointed to find the same disingenuous claims about strong static type systems. I say disingenuous because the people that espouse these beliefs seem to have a minimum modicum of intelligence and do or would certainly (after a moment of reflection) certainly realize their fallacy: > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary. This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems. It is a certainty that type systems ask for far more than is needed to produce correctness. Anyone who tries to dodge this obvious and fundamental truth is operating off of a religious not rational commitment to defending their type system. Note that I am not saying the type system doesn't give you something back but it certainly comes with a inherent cost over alternatives. > Another argument I hear a lot is that dealing with types imposes too much burden on the programmer. I could sympathize with this sen- timent after having to write a few declarations of iterators in C++ my- self, except that there is a technology called type inference that lets the compiler deduce most of the types This is the most heinous and sad lie. Type inference changes nothing. The types are there even if you don't have to type them in and they are significantly constraining your set of accepted programs. I've heard this response before from seemingly smart static typers. I just can't believe a smart person would not see the obvious emptiness of this claim. There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away. I want to buy into the strong static typist's promise of utopia but I have yet to meet a static typist enthusiast that doesn't parlay in these lies, wittingly or unwittingly. Because of this I have a serious suspicion that there is nothing else to stand on and that strong static typing is simply a case of the Emperor's New Clothes. Prove me wrong.

tome 7y ago
> > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary. > This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems. It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please! > There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away. OP is not claiming that the benefit of type inference is that it automatically "types characters". > I have yet to meet a static typist enthusiast that doesn't parlay in these lies I don't think it's necessary to bring a moral dimension into this discussion. Let's keep it technical please.
- wellpast 7y ago
  > It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please! Great, let's stay in a weakly typed language -- and give the smallest of examples. This is so easy to come by it should be obvious that extrapolating this up to real business systems greatly magnifies cost. Here's weakly typed Java: Function<String, Integer> countChars = str -> str.length(); That's a function that counts characters in a string. It compiles. Now let's drop the types: Function countChars = str -> str.length(); That is a correct definition of the same function but it doesn't compile. The compiler needs information to carry out its proof. This extrapolates to infinite more examples and the cost in building actual business systems is profound. Now carry this to a strongly typed system. The general claim is that type inference will allow the second form to somehow magically pass the compiler. Not true. The type inference requires `length` to be formally declared before the compiler can pass the program. I.e., the compiler must be told about the types somewhere. In a dynamically typed language I can late bind `length`; ie the compiler doesn't need to be "told" something that I, the programmer, have got fully covered by my own measures. But the compiler doesn't know this. I've already done my proof of correctness (as I should). But because the compiler does not have context, I have to tell it something that has no innate value to me and what I'm delivering -- it only has value to the closed-room of the compiler. This is hostile to productivity and serves only my early commitment to having a type prover guard my every move.
Hercuros 7y ago
I think your point about disingenuous arguments made by static typing proponents is mostly reasonable, but I don’t think those are the only arguments to be made for strong static typing. Other benefits of strong static type systems are compiler-enforced documentation (through types) and ease of refactoring. Of course, working in a typed system does constrain you, but I would argue that the cost/benefit ratio is usually quite good. I don’t typically feel very constrained when writing a program in Haskell, compared to Python. I do generally stick to “boring” Python code that would have passed a type checker if Python had one. It does depend a little on the type of application. For writing a compiler, I prefer Haskell, but for doing data-munging and one-off scripts, I prefer Python. However, arguing about the cost/benefit ratio of programming language features is often difficult, since the benefits and costs are hard to quantify. I do think that it isn’t reasonable to measure the cost of a type system by porting a program from a dynamic language to it, since doing large scale rewrites from a different language is not a typical task. It’s also hard to tell which parts of the porting process are “extraneous” and which parts aren’t. If I port a program from Python to Lisp, I will also have to do some significant extra thinking to make it work, but it isn’t because of static typing of the target language. Porting between different languages is just inherently difficult, and will always involve non-trivial “extraneous” effort. Maybe it’s more work when going to statically typed languages, but it’s not a reasonable measure in any case.
- wellpast 7y ago
  > Other benefits of strong static type systems are compiler-enforced documentation (through types) and ease of refactoring. I do agree if "compiler-enforced" is your target then by definition you'll choose compiler enforcement. For me the cost is too high. I'd rather solve my documentation needs through other far less costly means. > ...ease of refactoring. This is one of the lies espoused by the strong static typer. The claim here usually is that the compiler will tell you where you're broken through each step of the refactor. The irony is that the effect is the opposite of what is claimed: requiring a refactor to be formally/machine-verified correct through each iteration is a huge drag on refactoring. In a non-strongly typed language I can iteratively refactor and execute parts of my program even if a formal verified/strong-type prover would reject the program. This equates to way better throughput/speed over the formal static verifier/typer. Formal static verification may give you a host of benefits but in what most of us are doing Time is the most important resource by far. And formal verification/strong-type systems are downright hostile to Time. Which is especially offensive because the claims of stability can be readily achieved through much more efficient and agile techniques than formal verification.

tome 7y ago

> > The only serious argument I hear against strong static type check- ing is that it might eliminate some programs that are semantically cor- rect. In practice, this happens extremely rarely and, in any case, every language provides some kind of a backdoor to bypass the type sys- tem when that’s really necessary. > This is patently false. Port a correct dynamically typed program to Haskell and it will certainly fail until you satisfy the type checker through no small extraneous effort. And this is not a theoretical matter; it is an enormous cost to the programmer that is not there in weaker or non- typed systems. It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please! > There is no way anyone would think that having to type characters is the exclusive cost of static typing that inference suddenly whisks away. OP is not claiming that the benefit of type inference is that it automatically "types characters". > I have yet to meet a static typist enthusiast that doesn't parlay in these lies I don't think it's necessary to bring a moral dimension into this discussion. Let's keep it technical please.

wellpast 7y ago
> It seems like this disagreement should be easy to resolve. You are saying that it's hard to satisfy the type checker when porting a dynamically-typed program; OP says this happens very rarely. Therefore you can easily disprove OP's claim by providing some examples that happen commonly in practice. Provide them, please! Great, let's stay in a weakly typed language -- and give the smallest of examples. This is so easy to come by it should be obvious that extrapolating this up to real business systems greatly magnifies cost. Here's weakly typed Java: Function<String, Integer> countChars = str -> str.length(); That's a function that counts characters in a string. It compiles. Now let's drop the types: Function countChars = str -> str.length(); That is a correct definition of the same function but it doesn't compile. The compiler needs information to carry out its proof. This extrapolates to infinite more examples and the cost in building actual business systems is profound. Now carry this to a strongly typed system. The general claim is that type inference will allow the second form to somehow magically pass the compiler. Not true. The type inference requires `length` to be formally declared before the compiler can pass the program. I.e., the compiler must be told about the types somewhere. In a dynamically typed language I can late bind `length`; ie the compiler doesn't need to be "told" something that I, the programmer, have got fully covered by my own measures. But the compiler doesn't know this. I've already done my proof of correctness (as I should). But because the compiler does not have context, I have to tell it something that has no innate value to me and what I'm delivering -- it only has value to the closed-room of the compiler. This is hostile to productivity and serves only my early commitment to having a type prover guard my every move.

Hercuros 7y ago

I think your point about disingenuous arguments made by static typing proponents is mostly reasonable, but I don’t think those are the only arguments to be made for strong static typing. Other benefits of strong static type systems are compiler-enforced documentation (through types) and ease of refactoring. Of course, working in a typed system does constrain you, but I would argue that the cost/benefit ratio is usually quite good. I don’t typically feel very constrained when writing a program in Haskell, compared to Python. I do generally stick to “boring” Python code that would have passed a type checker if Python had one. It does depend a little on the type of application. For writing a compiler, I prefer Haskell, but for doing data-munging and one-off scripts, I prefer Python. However, arguing about the cost/benefit ratio of programming language features is often difficult, since the benefits and costs are hard to quantify. I do think that it isn’t reasonable to measure the cost of a type system by porting a program from a dynamic language to it, since doing large scale rewrites from a different language is not a typical task. It’s also hard to tell which parts of the porting process are “extraneous” and which parts aren’t. If I port a program from Python to Lisp, I will also have to do some significant extra thinking to make it work, but it isn’t because of static typing of the target language. Porting between different languages is just inherently difficult, and will always involve non-trivial “extraneous” effort. Maybe it’s more work when going to statically typed languages, but it’s not a reasonable measure in any case.

wellpast 7y ago
> Other benefits of strong static type systems are compiler-enforced documentation (through types) and ease of refactoring. I do agree if "compiler-enforced" is your target then by definition you'll choose compiler enforcement. For me the cost is too high. I'd rather solve my documentation needs through other far less costly means. > ...ease of refactoring. This is one of the lies espoused by the strong static typer. The claim here usually is that the compiler will tell you where you're broken through each step of the refactor. The irony is that the effect is the opposite of what is claimed: requiring a refactor to be formally/machine-verified correct through each iteration is a huge drag on refactoring. In a non-strongly typed language I can iteratively refactor and execute parts of my program even if a formal verified/strong-type prover would reject the program. This equates to way better throughput/speed over the formal static verifier/typer. Formal static verification may give you a host of benefits but in what most of us are doing Time is the most important resource by far. And formal verification/strong-type systems are downright hostile to Time. Which is especially offensive because the claims of stability can be readily achieved through much more efficient and agile techniques than formal verification.