4 ms·
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 y
by 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 agoI 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 agoIt'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.