5 ms·

The author is right with every. Single. Point. But I think their criticism comes from an ivory tower where people in general agree that efficient programming n

The author is right with every. Single. Point. But I think their criticism comes from an ivory tower where people in general agree that efficient programming needs strong and sound tools. Unfortunately, in practice it seems to be all about "velocity". When you see a huge codebase in python grown over several years and try to refactor it, reason about it, or just enhance it, you will inevitably come to the conclusion that the omission of static type checking is a grave error from a system-design perspective. And when you work with the developers of such a code base you will understand that static type checking is first and foremost a means of communication between the language implementation and the developers. Without this tool it is like taking away a common spoken language between the developers and having to translate everything into some form of pidgin.

jmull 7y ago
If you have a system where the developers often aren’t sure what it does, how to organize the code, aren’t designing for maintainability, etc., static type checking really isn’t going to help you pick up the pieces afterward. I like static type checking for what it does, but it solves some little problems, not big ones. (And can cause their own little problems.)
- cobbzilla 7y ago
  Disagree. Off the top of my head: Inability to do automatic, reliable refactoring is a big problem. Inability to detect a wide range of errors before hitting them at runtime, big problem. There are many more.
  - naasking 7y ago
    In other words, it will help you not break things. Tests are existential proofs of something broken, but types establish a universal proof that something is not broken in specific ways. Tests simply can't replace the properties guaranteed by types.
    - jnwatson 7y ago
      And types can’t represent the properties shown by tests. Type checking as typically applied only catches the simple problems of feeding the wrong argument into a function. Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance.
      - cobbzilla 7y ago
        It’s not an either/or. Both types and tests help, for different reasons. For programming in the large, both should be used. In the long run it’s about saving time that is otherwise wasted on wolf-fencing and hair-pulling; and in getting new developers up to speed faster.
      - jcora 7y ago
        Actually with dependent types you totally can encode proofs that your logic is correct. But I don't really see that trickling down into mainstream programming anytime soon.
      - naasking 7y ago
        > And types can’t represent the properties shown by tests. That's not true generally. Dependent types can be used to represent any property that a test might check, and lightweight alternatives can prove a subset [1]. And this makes sense from the type of logical property being established: you can easily turn a universally quantified proposition into an existentially quantification, but going the other way around means checking all possible permutations of values. However, proving a universally quantification is sometimes (often?) far more difficult than proving an existential quantification, which is why programs have to be structured in a certain way to make them amenable to such proofs. > Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance. Type systems always improve performance, so I don't know what you mean by that exactly. [1] http://lambda-the-ultimate.org/node/1635 http://lambda-the-ultimate.org/node/1635
  - jmull 7y ago
    Those are the big problems in the systems you've worked on? Consider yourself lucky.
    - cobbzilla 7y ago
      I normally don't respond to snark but what the heck I'm feeling festive. Your stated "big problems": * developers often aren’t sure what it does It's easier to understand what code is doing in a strongly typed system. Just trying to find where a method is defined in a dynamic language is often difficult and time-consuming. * how to organize the code Strongly typed languages generally encourage better code modularity. Not a panacea, but a help. * aren’t designing for maintainability Automatic, safe refactoring is a crucial tool in the maintainability toolkit. Again, not a panacea, but a huge help. I understand there are always bigger problems, and adopting a strongly typed approach after a mountain of technical debt has already accumulated may not be worth it. And if your developers can't write good, maintainable code regardless of static/dynamic types, that is certainly a bigger problem. But none of this means that static types don't solve big problems, which was the assertion I disagreed with.
pytester 7y ago
>When you see a huge codebase in python grown over several years and try to refactor it, reason about it, or just enhance it, you will inevitably come to the conclusion that the omission of static type checking is a grave error from a system-design perspective. I inevitably came the exact opposite conclusion. Perhaps because at the start of my career I was trying to do the same thing with Java, and it added overhead and expense without a commensurate payoff in safety. Frankly, I think velocity is ridiculously underrated: * Because of the age old "customer doesn't know what they want" issue - hence you throw away a lot of the code that was not fit for purpose. * Also because the right kind of architecture is only obvious in retrospect - hence you throw away a lot of the code that was not fit for purpose. * And finally, because the only times in my career where I've had significant success in refactoring a large mission critical codebase it was python and it was because I'd managed to quickly build custom tooling infrastructure (e.g. testing) to support that refactoring. I do take some issue with python's type system (e.g. the whole truthiness thing), but on the whole it balances safety and velocity in a highly pragmatic manner.
- youerbt 7y ago
  I can't help the feeling that your post is about Python vs Java rather than static vs dynamic. And I don't see how your 3 points about the velocity thing are affected by static types.. Like, come on, many points can be argued over compiler usefulness, but help with throwing away code is rather not one of them.
  - pytester 7y ago
    >I can't help the feeling that your post is about Python vs Java rather than static vs dynamic. Because the OP was about python and because python and java are the two languages where I have worked on refactorings of large scale code bases. I can't help but feel that if you make a hypothesis (e.g. "static typing is naturally better"), you need to be open to examples that disprove this hypothesis. >And I don't see how your 3 points about the velocity thing are affected by static types.. Static typing usually means a lot of time spent satisfying the compiler. I don't disagree that this can be useful because it catches bugs (although a lot of stuff caught by compilers are not bugs). I disagree that this isn't a cost/benefit trade off that naturally works out.
z3t4 7y ago
When learning about math vectors the code often looked like x Pos + y Vec. But when rewriting it in a language withot annotations it became hard to understand the code. So I argued about adding annotations to the language. But the other side of the argument urged to use better variable names. So I rewrote it as position+speed and it became even easier to understand. And I have never missed annotations since then.
- mike_hock 7y ago
  A variable name tells me what the person who wrote it thought it was at the time they wrote it. A type tells me what it is in any version of the program that the compiler accepts.
  - sooheon 7y ago
    If the type is something generic like Tuple, it doesn't tell you what it means. If it's a type with domain semantics like Speed or Velocity, then goto your issue with naming variables.
    - mike_hock 7y ago
      No, but it tells me what types the tuple elements are, and thus indirectly (I know where to look to find out), how I can use them, and what calling functions on them will do. It doesn't tell me their significance for the business logic, that's what variable names are for.
- thaumasiotes 7y ago
  Adding a speed to a position is a cardinal sin against dimensional analysis, the type model for physics. ;p
  - foldr 7y ago
    The speed is most likely implicitly multiplied by a unit time.
ken 7y ago
Everybody evaluates new programming languages relative to the previous programming languages they've used. In fact, you can usually tell what language(s) a person comes from by their complaints about the new one they have to use. > When you see a huge codebase in python grown over several years and try to refactor it, reason about it, or just enhance it, you will inevitably come to the conclusion that the omission of static type checking is a grave error from a system-design perspective. I never did. When you give a C++ or Java programmer a large Python codebase, they'll find it hard to work with, and conclude that the problem with Python is the "omission of static type checking", i.e., the defining feature that their previous language had. Coming from Lisp, when I found large Python codebases hard to work with, I concluded that the features of Lisp (macros, symbols, conditions, multimethods, dynamic vars, feature-complete lambdas, etc.) were the problem. Static type checking is one tool to help deal with the massive quantity of dirt [1], but better abstraction capabilities mean there's an order of magnitude less dirt to deal with in the first place. Yes, static types are a means of communication. But they really only communicate what's already there. Conditions and multimethods are also means of communications, and they enable me to say what I mean in higher level terms instead of spelling it out in lower-level constructs each time. I don't worry about "refactoring tools" in Lisp because I don't have to repeat my intent all over the codebase. Most people come from programming languages with static type systems. The most popular dynamic languages in 2019 (Python, Javascript), unfortunately, lack the great abstraction-building features that Lisp has. It's not surprising most people extrapolate from their Py/JS experience into believing the problem with dynamic languages in general is that they don't have a static type system. [1]: http://steve-yegge.blogspot.com/2007/12/codes-worst-enemy.html http://steve-yegge.blogspot.com/2007/12/codes-worst-enemy.ht...

jmull 7y ago

If you have a system where the developers often aren’t sure what it does, how to organize the code, aren’t designing for maintainability, etc., static type checking really isn’t going to help you pick up the pieces afterward. I like static type checking for what it does, but it solves some little problems, not big ones. (And can cause their own little problems.)

cobbzilla 7y ago
Disagree. Off the top of my head: Inability to do automatic, reliable refactoring is a big problem. Inability to detect a wide range of errors before hitting them at runtime, big problem. There are many more.
- naasking 7y ago
  In other words, it will help you not break things. Tests are existential proofs of something broken, but types establish a universal proof that something is not broken in specific ways. Tests simply can't replace the properties guaranteed by types.
  - jnwatson 7y ago
    And types can’t represent the properties shown by tests. Type checking as typically applied only catches the simple problems of feeding the wrong argument into a function. Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance.
    - cobbzilla 7y ago
      It’s not an either/or. Both types and tests help, for different reasons. For programming in the large, both should be used. In the long run it’s about saving time that is otherwise wasted on wolf-fencing and hair-pulling; and in getting new developers up to speed faster.
    - jcora 7y ago
      Actually with dependent types you totally can encode proofs that your logic is correct. But I don't really see that trickling down into mainstream programming anytime soon.
    - naasking 7y ago
      > And types can’t represent the properties shown by tests. That's not true generally. Dependent types can be used to represent any property that a test might check, and lightweight alternatives can prove a subset [1]. And this makes sense from the type of logical property being established: you can easily turn a universally quantified proposition into an existentially quantification, but going the other way around means checking all possible permutations of values. However, proving a universally quantification is sometimes (often?) far more difficult than proving an existential quantification, which is why programs have to be structured in a certain way to make them amenable to such proofs. > Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance. Type systems always improve performance, so I don't know what you mean by that exactly. [1] http://lambda-the-ultimate.org/node/1635 http://lambda-the-ultimate.org/node/1635
- jmull 7y ago
  Those are the big problems in the systems you've worked on? Consider yourself lucky.
  - cobbzilla 7y ago
    I normally don't respond to snark but what the heck I'm feeling festive. Your stated "big problems": * developers often aren’t sure what it does It's easier to understand what code is doing in a strongly typed system. Just trying to find where a method is defined in a dynamic language is often difficult and time-consuming. * how to organize the code Strongly typed languages generally encourage better code modularity. Not a panacea, but a help. * aren’t designing for maintainability Automatic, safe refactoring is a crucial tool in the maintainability toolkit. Again, not a panacea, but a huge help. I understand there are always bigger problems, and adopting a strongly typed approach after a mountain of technical debt has already accumulated may not be worth it. And if your developers can't write good, maintainable code regardless of static/dynamic types, that is certainly a bigger problem. But none of this means that static types don't solve big problems, which was the assertion I disagreed with.

pytester 7y ago

>When you see a huge codebase in python grown over several years and try to refactor it, reason about it, or just enhance it, you will inevitably come to the conclusion that the omission of static type checking is a grave error from a system-design perspective. I inevitably came the exact opposite conclusion. Perhaps because at the start of my career I was trying to do the same thing with Java, and it added overhead and expense without a commensurate payoff in safety. Frankly, I think velocity is ridiculously underrated: * Because of the age old "customer doesn't know what they want" issue - hence you throw away a lot of the code that was not fit for purpose. * Also because the right kind of architecture is only obvious in retrospect - hence you throw away a lot of the code that was not fit for purpose. * And finally, because the only times in my career where I've had significant success in refactoring a large mission critical codebase it was python and it was because I'd managed to quickly build custom tooling infrastructure (e.g. testing) to support that refactoring. I do take some issue with python's type system (e.g. the whole truthiness thing), but on the whole it balances safety and velocity in a highly pragmatic manner.

youerbt 7y ago
I can't help the feeling that your post is about Python vs Java rather than static vs dynamic. And I don't see how your 3 points about the velocity thing are affected by static types.. Like, come on, many points can be argued over compiler usefulness, but help with throwing away code is rather not one of them.
- pytester 7y ago
  >I can't help the feeling that your post is about Python vs Java rather than static vs dynamic. Because the OP was about python and because python and java are the two languages where I have worked on refactorings of large scale code bases. I can't help but feel that if you make a hypothesis (e.g. "static typing is naturally better"), you need to be open to examples that disprove this hypothesis. >And I don't see how your 3 points about the velocity thing are affected by static types.. Static typing usually means a lot of time spent satisfying the compiler. I don't disagree that this can be useful because it catches bugs (although a lot of stuff caught by compilers are not bugs). I disagree that this isn't a cost/benefit trade off that naturally works out.

z3t4 7y ago

When learning about math vectors the code often looked like x Pos + y Vec. But when rewriting it in a language withot annotations it became hard to understand the code. So I argued about adding annotations to the language. But the other side of the argument urged to use better variable names. So I rewrote it as position+speed and it became even easier to understand. And I have never missed annotations since then.

mike_hock 7y ago
A variable name tells me what the person who wrote it thought it was at the time they wrote it. A type tells me what it is in any version of the program that the compiler accepts.
- sooheon 7y ago
  If the type is something generic like Tuple, it doesn't tell you what it means. If it's a type with domain semantics like Speed or Velocity, then goto your issue with naming variables.
  - mike_hock 7y ago
    No, but it tells me what types the tuple elements are, and thus indirectly (I know where to look to find out), how I can use them, and what calling functions on them will do. It doesn't tell me their significance for the business logic, that's what variable names are for.
thaumasiotes 7y ago
Adding a speed to a position is a cardinal sin against dimensional analysis, the type model for physics. ;p
- foldr 7y ago
  The speed is most likely implicitly multiplied by a unit time.

ken 7y ago

Everybody evaluates new programming languages relative to the previous programming languages they've used. In fact, you can usually tell what language(s) a person comes from by their complaints about the new one they have to use. > When you see a huge codebase in python grown over several years and try to refactor it, reason about it, or just enhance it, you will inevitably come to the conclusion that the omission of static type checking is a grave error from a system-design perspective. I never did. When you give a C++ or Java programmer a large Python codebase, they'll find it hard to work with, and conclude that the problem with Python is the "omission of static type checking", i.e., the defining feature that their previous language had. Coming from Lisp, when I found large Python codebases hard to work with, I concluded that the features of Lisp (macros, symbols, conditions, multimethods, dynamic vars, feature-complete lambdas, etc.) were the problem. Static type checking is one tool to help deal with the massive quantity of dirt [1], but better abstraction capabilities mean there's an order of magnitude less dirt to deal with in the first place. Yes, static types are a means of communication. But they really only communicate what's already there. Conditions and multimethods are also means of communications, and they enable me to say what I mean in higher level terms instead of spelling it out in lower-level constructs each time. I don't worry about "refactoring tools" in Lisp because I don't have to repeat my intent all over the codebase. Most people come from programming languages with static type systems. The most popular dynamic languages in 2019 (Python, Javascript), unfortunately, lack the great abstraction-building features that Lisp has. It's not surprising most people extrapolate from their Py/JS experience into believing the problem with dynamic languages in general is that they don't have a static type system. [1]: http://steve-yegge.blogspot.com/2007/12/codes-worst-enemy.html http://steve-yegge.blogspot.com/2007/12/codes-worst-enemy.ht...