Stricter Type Guard

19 Sept 2023

Eric Traut & Rich Chiodo

Developing an intuition about type guards

# For the purposes of illustration,

# assume the following class hierarchy.

​

class Animal: ...

class Dog(Animal): ...

​

class Plant: ...

class Tree(Plant): ...

Developing an intuition about type guards

def func1(val: Animal | Plant):

if isinstance(val, Animal):

reveal_type(val) # ?

else:

reveal_type(val) # ?

Animal is same type as Animal

def func1(val: Animal | Plant):

if isinstance(val, Animal):

reveal_type(val) # Animal

else:

reveal_type(val) # Plant

def func2(val: Animal | Plant):

if isinstance(val, Dog):

reveal_type(val) # ?

else:

reveal_type(val) # ?

Dog is a subtype of Animal but not of Plant

def func2(val: Animal | Plant):

if isinstance(val, Dog):

reveal_type(val) # Dog

else:

reveal_type(val) # Animal | Plant

def func3(val: Dog | Tree):

if isinstance(val, Animal):

reveal_type(val) # ?

else:

reveal_type(val) # ?

Animal is a supertype of Dog but not of Tree

def func3(val: Dog | Tree):

if isinstance(val, Animal):

reveal_type(val) # Dog

else:

reveal_type(val) # Tree

def func4(val: Animal):

if isinstance(val, Tree):

reveal_type(val) # ?

Tree is not subtype or supertype of Animal

def func4(val: Animal):

if isinstance(val, Tree):

reveal_type(val) # <subclass Animal & Tree> (pyright & mypy)

# Never (pyre)

Developing an intuition about type guards

def func5(val: list[Plant]):

if isinstance(val, Iterable):

reveal_type(val) # ?

def func6(val: Iterable[Plant]):

if isinstance(val, list):

reveal_type(val) # ?

def func7(val: Plant | Iterable[Plant] | Mapping[str, Plant]):

if isinstance(val, Mapping):

reveal_type(val) # ?

def func5(val: list[Plant]):

if isinstance(val, Iterable):

reveal_type(val) # list[Plant]

def func6(val: Iterable[Plant]):

if isinstance(val, list):

reveal_type(val) # list[Plant] (pyright)

# list[Any] (mypy & pyre)

def func7(val: Plant | Iterable[Plant] | Mapping[str, Plant]):

if isinstance(val, Mapping):

reveal_type(val) # Mapping[Plant, Any] | Mapping[str, Plant] (pyright)

# Mapping[Any, Any] | Mapping[str, Plant] (mypy)

# Mapping[str, Plant] (pyre)

def func8(val: T):

if isinstance(val, Animal):

reveal_type(val) # ?

def func8(val: T):

if isinstance(val, Animal):

reveal_type(val) # Animal & T (pyright)

# Animal (mypy)

# Never (pyre)

What does type theory say?

• R = isinstance filter type
• A = isinstance argument type (pre-narrowed)
• NP = Narrowed type (positive)
• NN = Narrowed type (negative)

def func1(val: A):

if isinstance(val, R):

reveal_type(val) # NP

else:

reveal_type(val) # NN

Type theoretic narrowing equations:

NP = A & R

NN = A & ~R

Set intersection

Set negation

A

R

A & R

A & ~R

def func1(val: Animal | Plant):

if isinstance(val, Animal):

reveal_type(val) # (Animal | Plant) & Animal → Animal

else:

reveal_type(val) # (Animal | Plant) & ~Animal → Plant & ~Animal

def func2(val: Animal | Plant):

if isinstance(val, Dog):

reveal_type(val) # (Animal | Plant) & Dog → Dog

else:

reveal_type(val) # (Animal | Plant) & ~Dog → (Animal & ~Dog) | Plant

def func3(val: Dog | Tree):

if isinstance(val, Animal):

reveal_type(val) # (Dog | Tree) & Animal → Dog | (Tree & Animal)

else:

reveal_type(val) # (Dog | Tree) & ~Animal → Tree & ~Animal

def func4(val: Animal):

if isinstance(val, Tree):

reveal_type(val) # Animal & Tree

Type theoretic narrowing

Narrower than “Animal | Plant”

Wider than “Dog”

Animal

Plant

Dog

Tree

Narrower than “Plant”

Narrower than “Tree”

Type theoretic narrowing

def func5(val: list[Plant]):

if isinstance(val, Iterable):

reveal_type(val) # list[Plant] & Iterable[Any] → list[Plant]

def func6(val: Iterable[Plant]):

if isinstance(val, list):

reveal_type(val) # Iterable[Plant] & list[Any] → list[Plant]

def func7(val: Plant | Iterable[Plant] | Mapping[str, Plant]):

if isinstance(val, Mapping):

reveal_type(val) # (Plant | Iterable[Plant] | Mapping[str, Plant]) & Mapping[Any]

→ (Plant & Mapping[Any]) | Mapping[Plant, Any] |

Mapping[str, Plant]

def func8(val: T):

if isinstance(val, Animal):

reveal_type(val) # Animal & T

PEP 647 introduced user-defined type guards

​

TypeGuard does not work like isinstance, which violates many users’ expectations

​

1. In the positive case, narrowing is a simple replacement

2. In the negative case, types are not narrowed

Problems with current formulation of TypeGuard

def is_animal(val: object) -> TypeGuard[Animal]:

return isinstance(val, Animal)

​

def func1(val: Dog | Tree):

if is_animal(val):

reveal_type(val) # Animal

else:

reveal_type(val) # Dog | Tree

Expected “Dog”

Expected “Tree”

Allows for broader set of use cases that don’t strictly conform to type rules

​

​

​

​

Why was TypeGuard formulated the way it was?

def has_no_nones[T](val: list[None | T]) -> TypeGuard[list[T]]:

return all(x is not None for x in val)

​

class Person(TypedDict):

name: str

age: int

​

def is_person(val: dict) -> TypeGuard[Person]:

try:

return isinstance(val["name"], str) and isinstance(val["age"], int)

except KeyError:

return False

​

Option 1: Create a new form called StrictTypeGuard that applies isinstance type guard semantics

• Requires users to understand a new form and the subtle difference between TypeGuard and StrictTypeGuard
• Previously prototyped in pyright, but feedback was mixed

​

Option 2: Modify TypeGuard to apply isinstance type guard semantics when it can be shown to be safe

• Users automatically get the expected behavior when it’s safe
• Theoretically could break existing code that uses TypeGuard; in practice, we don’t think it will
• Proposed in draft PEP
• Recently prototyped in pyright (enabled via enableExperimentalFeatures=true)

​

Accommodating both non-strict and strict semantics

Each use of a type guard involves five types:

• P = Type guard parameter type
• R = Type guard return type
• A = Argument type (pre-narrowed)
• NP = Narrowed type (positive)
• NN = Narrowed type (negative)

def guard(x: P) -> TypeGuard[R]: ...

​

def func1(val: A):

if guard(val):

reveal_type(val) # NP

else:

reveal_type(val) # NN

These cannot be represented in the Python type system today, so they need to be approximated. We recommend leaving it up to each type checker to decide how to do this, just as we allow each type checker to decide how to implement the “isinstance” type guard today.

This symbol means “R” is consistent with “P”; i.e. you can assign a value of type “R” to “P” without a type violation.

Proposed new definition of TypeGuard

PEP started

PEP 724: Stricter TypeGuard by rchiodo · Pull Request #3266 · python/peps (github.com)