Exhaustiveness Checking with Mypy

https://hakibenita.com/python-mypy-exhaustive-checking

by rbanffy • 6 years ago

85 19 6 years ago

karlicoss2• 6 years ago

I also find type narrowing extremely useful for error handling: you can use Union[Exception, T] as the result type, and ‘pattern match’ with isinstance, which works in runtime and statically checkable by mypy.

In addition, covariant Union type allows using it with generators (i.e. yield Exception("some error"), and consuming without extra boilerplate. I write more about it here: https://beepb00p.xyz/mypy-error-handling.html#coderef-simple...

londt8• 6 years ago

This may seem like a good idea, but it gets problematic since you need to always use isinstance checks. Its actually discouraged to return union types by the mypy team: https://github.com/python/mypy/issues/1693

karlicoss2• 6 years ago

Yeah, but you need to test whether the result is an error or not in some way. In languages with better ADT/pattern matching support (like Haskell or Rust) you'd use case/match operator, or whatever it's called.

I've read the issue, and it seems that it's more about the lack of overloading/dependent types, e.g. their example with pow function. In c++ you'd have two overloads:

    float pow(float, float)
    int pow(int, int)

Whereas in python, even though you can achieve the equivalent behaviour in runtime, mypy (at least until recently) couldn't express this, so you had to define something like

    def pow(base: Union[int, float], power: Union[int, float]) -> Union[int, float]

Which might be annoying on call sites when you do expect the return type to be int (but there is no way for mypy to know that with such signature).

In my case I do want to return a variant type unconditionally, so this warning doesn't really apply. It's more similar to an Optional type (just instead of None I am using a more meaningful Exception): while it's not great if your code is riddled with optional return types, sometimes you don't have other choice but using it.

petters• 6 years ago

This is great! This function belongs in the standard library.

haki• 6 years ago

See relevant section in the article:

https://hakibenita.com/python-mypy-exhaustive-checking#the-f...

frob• 6 years ago

Issues like this are another reason Python should have a native switch...case control flow instead of trying to cram it into a chain of elifs or a dict. In other languages, calling a switch on an enum will cause the type checker to ensure that all cases are handled or that there's a default case. I see there's a PEP out to push this functionality into elifs, but it still seems inelegant to me.

frou_dh• 6 years ago

The `match` statement, slated for the next version of Python (3.10), is rather comprehensive. Don't think we could reasonably expect much more than this to be retrofitted into an old language [0]

https://www.python.org/dev/peps/pep-0622/#exhaustiveness-che...

https://www.python.org/dev/peps/pep-0634/

[0] Trivia: Python is older than Linux!

adenozine• 6 years ago

I'm so excited for match to become a thing. Honestly, exhaustiveness had kept me from using Python for some work that I'd have otherwise loved to use it! I enjoy FP and some of the other benefits of Ocaml, which is what I use for programs where Mypy can't give me what I need. But at the end of the day, I'm just not as nimble with it, and I can just see the python in my head so much easier.

jackric3• 6 years ago

Very exciting for experienced developers missing this from other languages, but I predict the growing spec of Python is leading it away from the "my first language" crowd in future.

mirko224• 6 years ago

Yet python never needed a case statement. It used to be simple to write and read language, unlike so many others.

Cramming in new statements just to check Enums types properly sounds... well wrong... The types don't do anything except make code harder to read. But I know that unpopular opinion here... I guess I just like old simple Python more.

jackric3• 6 years ago

Curious what other languages you're fluent with? I found once I'd grokked a language with `match` (Rust), I missed it when writing Python afterwards.

tpoacher• 6 years ago

On one hand, this "feels" useful ... on the other hand, I can't shake that unnerving feeling that this kind of exhaustiveness check should belong in tests instead.

If the issue is to help you ensure that you check your edge cases properly, and ensure you are acting within specification, then presumably you should be addressing these issues in your tests, not in production code.

Therefore the whole exercise of writing code to catch errors of this kind 'at compile-time vs runtime' is somewhat of a red herring, if not dangerous.

Having said that, I'm also guilty of frequently writing

    else: error("In theory this should never happen")

mirko224• 6 years ago

Heh, I feel you. Test were indeed used to verify that your code runs correctly and with edge cases, and stuff like isinstance were discouraged so you wouldn't need to think about types but rather of interfaces. However I assume that a large influx of people who had experience with typed languages had changed general idea of how Python should look and be used. Oh well, times change and we all allowed it so... types it is :/

brundolf• 6 years ago

presumably you should be addressing these issues in your tests, not in production code

What you may be missing is that this code will be guaranteed by MyPy to never actually run in production. In fact what it's effectively saying is "if this code can run, there's a type error", and therefore MyPy forces you to ensure that the code can never run.

Exhaustiveness Checking with Mypy

Related Stories