5 ms·

PEP 695 is great. I've been using mypy every day at work in last couple years or so with very strict parameters (no any type etc) and I have experience writing

PEP 695 is great. I've been using mypy every day at work in last couple years or so with very strict parameters (no any type etc) and I have experience writing real life programs with Rust, Agda, and some Haskell before, so I'm familiar with strict type systems. I'm sure many will disagree with me but these are my very honest opinions as a professional who uses Python types every day: * Some types are better than no types. I love Python types, and I consider them required. Even if they're not type-checked they're better than no types. If they're type-checked it's even better. If things are typed properly (no any etc) and type-checked that's even better. And so on... * Having said this, Python's type system as checked by mypy feels like a toy type system. It's very easy to fool it, and you need to be careful so that type-checking actually fails badly formed programs. * The biggest issue I face are exceptions. Community discussed this many times [1] [2] and the overall consensus is to not check exceptions. I personally disagree as if you have a Python program that's meticulously typed and type-checked exceptions still cause bad states and since Python code uses exceptions liberally, it's pretty easy to accidentally go to a bad state. E.g. in the linked github issue JukkaL (developer) claims checking things like "KeyError" will create too many false positives, I strongly disagree. If a function can realistically raise a "KeyError" the program should be properly written to accept this at some level otherwise something that returns type T but 0.01% of the time raises "KeyError" should actually be typed "Raises[T, KeyError]". * PEP 695 will help because typing things particularly is very helpful. Often you want to pass bunch of Ts around but since this is impractical some devs resort to passing "dict[str, Any]"s around and thus things type-check but you still get "KeyError" left and right. It's better to have "SomeStructure[T]" types with "T" as your custom data type (whether dataclass, or pydantic, or traditional class) so that type system has more opportunities to reject bad programs. * Overall, I'm personally very optimistic about the future of types in Python! [1] https://github.com/python/mypy/issues/1773 https://github.com/python/mypy/issues/1773 [2] https://discuss.python.org/t/extend-type-hints-to-cover-exceptions/23788/4 https://discuss.python.org/t/extend-type-hints-to-cover-exce...

dragonwriter 3y ago
> If a function can realistically raise a "KeyError" the program should be properly written to accept this at some level By definition, it is, because there is defined behavior for unhandled exceptions. If you want to—and this is a valid preference—wrap all exceptions thrown at a lower level and present an API where they are part of the return type that must be addressed by code to pass typechecking, then you do that and return actual values of an appropriate type (you can still use exception types, if you wish) instead of raising exceptions. Exceptions which you force client code to handle to typecheck are not exceptions, they are return values and should be converted to explicitly that, rather than adding checked exceptions.
- gnulinux 3y ago
  I think that this is a hard problem and you're right that spamming KeyError everywhere is against the exceptionality of exceptions. But the current completely unchecked model is also misleading. I don't have such a great solution in mind but I think mypy should be able to verify each exception type is handled at some point in the stack. I know that it sounds vague, but these are my current unorganized thoughts.
  - zmgsabst 3y ago
    Exceptions are always handled: Python exits while telling you about the exceptional situation. If you’re saying that I must handle an exception in my code rather than crash because my “fail early, fail often” design choices offend your religious preferences… then keep it to yourself and out of PEPs.
    - gnulinux 3y ago
      No I'm not saying that at all, I'm just saying that if you need a function to handle all exceptions, the type system should be powerful enough to express that. E.g. in a webserver if you have a handler that needs a wrapper like: def wrapper(): try: return handler() except Exception: logger.exception("unknown exception") webserver.status = 500 the type system needs to be able to determine that "f doesn't raise an exception". For example, one way to do this can be that all functions by default raise exception and we type: def handler() -> T: ... def wrapper() -> NeverRaises[T]: ... then we have webserver_add('GET', '/handler', wrapper) so that def webserver_add(method: str, path: str, handle_func: Callable[[], NeverRaises[T]]) -> None: ... which is type safer. Of course, here we need to specially handle `KeyboardInterrupt`, signals and exceptions returned by `logger` etc. I would personally recommend ignoring `KeyboardInterrupt`, and signals and type annotating `logger.exception` as `NeverRaises`. 95% is still better than 0%.
      - dragonwriter 3y ago
        > I'm just saying that if you need a function to handle all exceptions, the type system should be powerful enough to express that. I disagree, in part because “handles all exceptions” is a lie; exceptions can occur at any point, including in exception-hnadling code. It is not possible to have a Python function which provides the guarantee you want, so it makes no sense to have a Python type system which expressed it: it will either be never used or a lie. If you think you need this guarantee, you need to step back and ask what the functional requirement actually is and find a different way of meeting it.
NoboruWataya 3y ago
Are there any other languages where typing is purely optional and yet so much effort is going into developing the typing system? I started experimenting with Kotlin just when Python was starting to get type hints and after my experience with Kotlin I am totally sold on the benefits of typing. So to me it's great to see these recent developments. It just feels weird to me to have a language that is fundamentally dynamically typed (and committed to that paradigm) invest so much effort in developing this elaborate but optional typing system.
- jredwards 3y ago
  Uh. JavaScript?
- deleted 3y ago
  [deleted]
- satvikpendem 3y ago
  Javascript, with TypeScript, and Ruby come to mind.
- fwungy 3y ago
  Typing is nice just for the documentation it provides. Refactoring old python scripts was a pain because you had no idea what the arguments and return values were. Is date a string or an object? It gets tiresome.
spinningslate 3y ago
I've been steadily finding the love for F# for sort-of-similar-but-not-quite-the-same reasons. I like Python. It's still my go-to language for most things. But I definitely feel a tail off in utility as code base size increases, and I find myself asking mentally "but what type is that thing?". F# is sort of the opposite of Python. It's strongly, statically and soundly typed, based on Hindley-Milner. It has very good type inference, meaning that explicit type annotations are usually not required. But it's still type checked, and compilation will fail if there are type errors. So F# gives you type soundness without requiring type annotations (in most cases); Python now supports type annotations but doesn't (yet) give type soundness guarantees. Of course, F# doesn't have the Python ecosystem, and that's a major issue. Whilst it sits on the .Net platform, it's very much Sunday League to C#'s premier division. Whilst most all .Net libs can be used in F# thanks the .Net CLR, very little is idiomatic: F# is a functional language, C# is object-oriented at heart. I think my fantasy platform would be some child of F#-the-language and Python-the-ecosystem. Maybe Python's incremental support for typing will get me there someday.
- dgunay 3y ago
  Similar sentiment with Rust (love the ecosystem, and love the language, except for the many, many parts of it that I don't need). F# comes up a lot in discussions like this. From a thread a few days ago: https://news.ycombinator.com/item?id=37892666 https://news.ycombinator.com/item?id=37892666
Spivak 3y ago
> the time raises "KeyError" should actually be typed "Raises[T, KeyError]" You can't do this in Python your bucket will always have hole you can't plug. Arbitrary exceptions can appear anywhere in your code thanks to signal handlers. KeyboardInterrupt is the one you probably know without knowing. Exceptions can even come from higher in the stack down to you with the .throw method on generators.
- gnulinux 3y ago
  Yep, I'm aware of these, I wrote about my thoughts about them here: https://news.ycombinator.com/item?id=37934604 https://news.ycombinator.com/item?id=37934604

dragonwriter 3y ago

> If a function can realistically raise a "KeyError" the program should be properly written to accept this at some level By definition, it is, because there is defined behavior for unhandled exceptions. If you want to—and this is a valid preference—wrap all exceptions thrown at a lower level and present an API where they are part of the return type that must be addressed by code to pass typechecking, then you do that and return actual values of an appropriate type (you can still use exception types, if you wish) instead of raising exceptions. Exceptions which you force client code to handle to typecheck are not exceptions, they are return values and should be converted to explicitly that, rather than adding checked exceptions.

gnulinux 3y ago
I think that this is a hard problem and you're right that spamming KeyError everywhere is against the exceptionality of exceptions. But the current completely unchecked model is also misleading. I don't have such a great solution in mind but I think mypy should be able to verify each exception type is handled at some point in the stack. I know that it sounds vague, but these are my current unorganized thoughts.
- zmgsabst 3y ago
  Exceptions are always handled: Python exits while telling you about the exceptional situation. If you’re saying that I must handle an exception in my code rather than crash because my “fail early, fail often” design choices offend your religious preferences… then keep it to yourself and out of PEPs.
  - gnulinux 3y ago
    No I'm not saying that at all, I'm just saying that if you need a function to handle all exceptions, the type system should be powerful enough to express that. E.g. in a webserver if you have a handler that needs a wrapper like: def wrapper(): try: return handler() except Exception: logger.exception("unknown exception") webserver.status = 500 the type system needs to be able to determine that "f doesn't raise an exception". For example, one way to do this can be that all functions by default raise exception and we type: def handler() -> T: ... def wrapper() -> NeverRaises[T]: ... then we have webserver_add('GET', '/handler', wrapper) so that def webserver_add(method: str, path: str, handle_func: Callable[[], NeverRaises[T]]) -> None: ... which is type safer. Of course, here we need to specially handle `KeyboardInterrupt`, signals and exceptions returned by `logger` etc. I would personally recommend ignoring `KeyboardInterrupt`, and signals and type annotating `logger.exception` as `NeverRaises`. 95% is still better than 0%.
    - dragonwriter 3y ago
      > I'm just saying that if you need a function to handle all exceptions, the type system should be powerful enough to express that. I disagree, in part because “handles all exceptions” is a lie; exceptions can occur at any point, including in exception-hnadling code. It is not possible to have a Python function which provides the guarantee you want, so it makes no sense to have a Python type system which expressed it: it will either be never used or a lie. If you think you need this guarantee, you need to step back and ask what the functional requirement actually is and find a different way of meeting it.

NoboruWataya 3y ago

Are there any other languages where typing is purely optional and yet so much effort is going into developing the typing system? I started experimenting with Kotlin just when Python was starting to get type hints and after my experience with Kotlin I am totally sold on the benefits of typing. So to me it's great to see these recent developments. It just feels weird to me to have a language that is fundamentally dynamically typed (and committed to that paradigm) invest so much effort in developing this elaborate but optional typing system.

jredwards 3y ago
Uh. JavaScript?
deleted 3y ago
[deleted]
satvikpendem 3y ago
Javascript, with TypeScript, and Ruby come to mind.
fwungy 3y ago
Typing is nice just for the documentation it provides. Refactoring old python scripts was a pain because you had no idea what the arguments and return values were. Is date a string or an object? It gets tiresome.

spinningslate 3y ago

I've been steadily finding the love for F# for sort-of-similar-but-not-quite-the-same reasons. I like Python. It's still my go-to language for most things. But I definitely feel a tail off in utility as code base size increases, and I find myself asking mentally "but what type is that thing?". F# is sort of the opposite of Python. It's strongly, statically and soundly typed, based on Hindley-Milner. It has very good type inference, meaning that explicit type annotations are usually not required. But it's still type checked, and compilation will fail if there are type errors. So F# gives you type soundness without requiring type annotations (in most cases); Python now supports type annotations but doesn't (yet) give type soundness guarantees. Of course, F# doesn't have the Python ecosystem, and that's a major issue. Whilst it sits on the .Net platform, it's very much Sunday League to C#'s premier division. Whilst most all .Net libs can be used in F# thanks the .Net CLR, very little is idiomatic: F# is a functional language, C# is object-oriented at heart. I think my fantasy platform would be some child of F#-the-language and Python-the-ecosystem. Maybe Python's incremental support for typing will get me there someday.

dgunay 3y ago
Similar sentiment with Rust (love the ecosystem, and love the language, except for the many, many parts of it that I don't need). F# comes up a lot in discussions like this. From a thread a few days ago: https://news.ycombinator.com/item?id=37892666 https://news.ycombinator.com/item?id=37892666

Spivak 3y ago

> the time raises "KeyError" should actually be typed "Raises[T, KeyError]" You can't do this in Python your bucket will always have hole you can't plug. Arbitrary exceptions can appear anywhere in your code thanks to signal handlers. KeyboardInterrupt is the one you probably know without knowing. Exceptions can even come from higher in the stack down to you with the .throw method on generators.

gnulinux 3y ago
Yep, I'm aware of these, I wrote about my thoughts about them here: https://news.ycombinator.com/item?id=37934604 https://news.ycombinator.com/item?id=37934604