4 ms·

I agree with you that the benefits of static typing are sometimes greatly exaggerated. But I also think that using type hints and type checkers in Python isn't

I agree with you that the benefits of static typing are sometimes greatly exaggerated. But I also think that using type hints and type checkers in Python isn't quite the same thing as static typing. For starters, type checking can't actually guarantee you won't have type errors at run time. Because, unlike in a statically typed language, in Python, anyone can always choose to just not use type hinting. Whenever that happens, as far as the type checker is concerned, anything goes. But type hints are very useful as hints. They help with editor tooling, which can make it easier to navigate an unfamiliar codebase. They provide extra information that makes the code easier to read. And they give me an opt-in form of type linting that allows me to set up regions of code where I don't have to take quite so much personal responsibility for ensuring that arguments are compatible with parameters. In short, it's not a correctness prover; it's an energy saver.

flowerlad 5y ago
> I agree with you that the benefits of static typing are sometimes greatly exaggerated. For large, multi-developer projects, it is impossible to exaggerate the benefits of static typing.
- deleted 5y ago
  [deleted]
nickm12 5y ago
I don't like the term "type hints" because typecheckers like mypy are genuinely proving type correctness. Yes, if you don't annotate part of your program then you can get a type error in that part of the program, likewise, if you pass a value of the wrong type, you can get a type error. But if you are using a typechecker, you are guaranteed that if your inputs are well-typed, then you won't have a type error, which is a stronger guarantee than "hints" implies.
- mumblemumble 5y ago
  I like the term "type hint" because that really is exactly what they are. Typecheckers like mypy are (1) optional, and (2) are only as good as the type hints themselves. Unlike with a language that's actually statically typed, the relation of the type annotations to the actual types of the data operates largely on the honor system, so the type checking is more a validation of internal consistency than full-on static type safety. Which is fine, and well within Python's "We're all adults here" ethos. It's just that it's still not anywhere near the level of rigor you get out of the type checker in a language like OCaml.
  - nickm12 5y ago
    It's really not the honor system. If you verify with a type checker, you are proving that various type errors are impossible, provided that the caller respects the type system. The rigor is exactly the same, it's just that the type system allows for "gradual typing" so that it doesn't need to be strict as in a fully-typed language.

flowerlad 5y ago

> I agree with you that the benefits of static typing are sometimes greatly exaggerated. For large, multi-developer projects, it is impossible to exaggerate the benefits of static typing.

deleted 5y ago
[deleted]

nickm12 5y ago

I don't like the term "type hints" because typecheckers like mypy are genuinely proving type correctness. Yes, if you don't annotate part of your program then you can get a type error in that part of the program, likewise, if you pass a value of the wrong type, you can get a type error. But if you are using a typechecker, you are guaranteed that if your inputs are well-typed, then you won't have a type error, which is a stronger guarantee than "hints" implies.

mumblemumble 5y ago
I like the term "type hint" because that really is exactly what they are. Typecheckers like mypy are (1) optional, and (2) are only as good as the type hints themselves. Unlike with a language that's actually statically typed, the relation of the type annotations to the actual types of the data operates largely on the honor system, so the type checking is more a validation of internal consistency than full-on static type safety. Which is fine, and well within Python's "We're all adults here" ethos. It's just that it's still not anywhere near the level of rigor you get out of the type checker in a language like OCaml.
- nickm12 5y ago
  It's really not the honor system. If you verify with a type checker, you are proving that various type errors are impossible, provided that the caller respects the type system. The rigor is exactly the same, it's just that the type system allows for "gradual typing" so that it doesn't need to be strict as in a fully-typed language.