6 ms·

Hm, growing somewhat experienced, I find myself adapating an old quote more and more: Sufficiently advanced static typing is indistinguishable from dynamic typi

• plmpsu 5y ago
  I don't understand your argument. Could you please explain it?
  • tetha 5y ago
    Type systems simply have matured a lot. It's not too long ago that you either had very clumsy type systems - C, Java. These type systems were more of a chore than anything else. Especially the generic transition in java was just tedious, you had to type cast a lot of stuff, and the compiler would still yell at you, and things would still crash. Or you had very powerful and advanced type systems - Haskell and C++ with templates for example. However, these type systems were just impenetrable. C++ template errors before clang error messages are something. They are certainly an error message. But fixing those without a close delta what happened? Pfsh. Nah. In those days, dynamic typing was great. You could shed the chore of stupid types, and avoid the really arcane work of making really strong types work. However, type systems have matured. Today, you can slap a few type annotations on a python function and a modern type inference engine can give you type prediction, accurate tab-completion and errro detection. In something like rust, you define a couple of types in important locations and everything else is inferred. This in turn gives you the benefit of both: You care about types in a few key locations, but everything else is as simple as a dynamically typed language. And that's when statically typed languages can end up looking almost - or entirely - like a dynamically typed language. Except with less error potential.
    • musicale 5y ago
      > a modern type inference engine can give you type prediction, accurate tab-completion and errro detection (emphasis mine) "errros" are my nemesis in languages which automatically create a new symbol with every typo!
• Jensson 5y ago
  > Sufficiently advanced static typing is indistinguishable from dynamic typing. Static typing type checks are compile time, dynamic typing doesn't. I don't see how these two could be indistinguishable, in one you can't run the program with type errors, in the other you can.
  • wvenable 5y ago
    I believe the author was talking about the act of writing the software. Modern type inference means that you can mostly code without needing to write down the types in many cases. This line of code is the same in JavaScript or C#: var instance = new SomeClass(); In function definitions, where you are definitely going to need to provide parameter types it's extremely common to document those types in a docblock in a dynamically typed language. At least I always did. So making the types part of the definition is not a significant difference while writing the code.
    • merb 5y ago
      c# even has target-typed expressions which might be useful aswell, i.e. instead of var instance = you write SomeClass instance = new(); this might be preferable so that you have all types on the left.
  • acdha 5y ago
    This is true if you're focused on the compiler but if you include the adjacent question of what is reported to you in your editor while working it's a bit blurrier. If I write some Rust code and pass a string into something which expects an integer, I get a hard error preventing compilation. If I do the same thing in Python, however, and there's a prominent error displayed in my editor before I even run the code, how different is that from the perspective of anyone who isn't watching my screen? In either case the bug was caught before the code even ran and I likely have type-aware autocompletion to reduce the odds of making that mistake in the first place. That's not to say that there aren't quite reasonable questions about how effective the different approaches are or how easy it is to fix the error, how complete the checks are, how deep the checks go, etc. A lot of how you feel about that is going to be subjective based on the languages you use and the quality of the code you work with — Rust has an advanced type system and great developer ergonomics providing unusually helpful error messages, Python has weaker typing but also a culture about simplicity which discourages some classes of bugs, Java has a lot of mushy-typed code where people got tired of language / compiler drawbacks and came up with ways to improve ergonomics at the expense of defeating the type checker, etc.
• slaymaker1907 5y ago
  Please write a type for the following function: def compose(start, *args): def helper(x): for func in reversed(args): x = func(x) return start(x) return helper There is no mainstream typed language which can write a fully general type for the vararg compose function. TypeScript is probably the one that comes closest, but last I checked it still was unable to write a sufficiently powerful array type. You can write a type for a version of compose with a fixed number of arguments, but not for one working over an arbitrary number of arguments.
  • tetha 5y ago
    As I said, there are infinite possible programs that cannot be type checked statically. This is derived from the halting theorem trivially - lambda(p) = if p.halts() then A() else B(). However, the intersection of programs I encounter in practice with the number of programs that can be statically checked is rather large.
    • phoneperson 5y ago
      You are probably thinking of Gödel's incompleteness theorems. I do not think that you can trivially derive it from the halting problem.
      • tehnub 5y ago
        He just did derive it from the halting problem. In words: It's impossible to statically check the type of a function that takes a program P as its input, and returns the integer 1 as its output if P halts, and returns the string "1" if it does not halt. It would require solving the halting problem, which is undecidable.
        • native_samples 5y ago
          How does that follow? The input type would be vague, e.g. ByteArray or Program or something.