type narrowing predicates¶

basedpython spells PEP 742 TypeIs[T] as name is T in the return annotation, naming the place being narrowed:

def is_str(x) -> x is str:
    return isinstance(x, str)

transpiles to:

from typing_extensions import TypeIs

def is_str(x) -> TypeIs[str]:
    return isinstance(x, str)

semantics¶

the runtime semantics are exactly PEP 742 — the function asserts that its argument has type T when it returns True, and the checker narrows accordingly at call sites. the name is lost in lowering (TypeIs doesn't carry it) but is preserved in the source for readers

a predicate cannot be negated. -> x is not str would narrow to everything but str where the call returns True, which TypeIs has no way to say, so it is an error. write -> x is str and negate the call instead (if not is_str(x):), or assert with asserts x is not str

naming the parameter¶

TypeIs always narrows a function's first parameter. the name says which parameter is meant, so any of them can be the narrowed one:

def is_str(first: object, second: object) -> second is str:
    return isinstance(second, str)

def f(a: object, b: object):
    if is_str(a, b):
        b  # str
        a  # object

the name is matched against the argument the call passes for that parameter, so a keyword argument narrows the same place

callable types¶

a callable type returns a predicate the same way, naming one of its parameters. its return binds tighter than a comparison, as it does than |, so the predicate is parenthesized:

def pick(check: (first: object, second: object) -> (second is int), a: object, b: object):
    if check(a, b):
        b  # int

a def whose predicate names that parameter is such a callable. a name that is not one of the callable's parameters is a place, as it is for a def

a caller narrows the argument the callable type names, so a function that tests a different one is not such a callable, even when the narrowed type is the same:

def is_int(first: object, second: object) -> first is int:
    return isinstance(first, int)

pick(is_int, 1, "b")  # error: narrows `first`, where `second` is expected

a parameter is matched by position, and by name too where a caller can pass it by keyword. a TypeIs that names no parameter narrows the first one — after self for a method — and a Callable narrows the first argument it is passed. an override is held to the same rule: it narrows what the method it overrides narrows

narrowing a member¶

a guard can name a member of what it narrows, which is how a method vouches for its own state:

class Holder:
    data: str | None = None

    def ensure(self) -> asserts self.data is not None:
        if self.data is None:
            raise ValueError

    def loaded(self) -> self.data is str:
        return self.data is not None

def f(h: Holder):
    h.ensure()
    h.data  # str

the member follows the receiver the call was made on — o.holder.ensure() narrows o.holder.data, and nothing else. a guard on a parameter's member (def ensure(h: Holder) -> asserts h.data is not None) narrows the argument's member the same way. python has no spelling for either, so both lower to what the function returns

the member a guard names is resolved where the guard is written, so a call from another module narrows the argument itself but not a member of it

narrowing a place¶

a name that is not a parameter is a place — narrowed where the call is written rather than at an argument:

a: int | None

def f() -> a is int: ...

def m():
    if f():
        a  # int

this has no PEP 742 spelling, so it lowers to bool

the place is resolved by name in the calling scope. a guard declared in another file names a place in that module, which is a different symbol from a same-named place at the call site, so it narrows nothing. for the same reason there is no definition-site check that the narrowed type fits the place: the place's type is whatever the calling scope has, and narrowing intersects with it

a predicate that was never written down¶

the annotation says what a truthy result means about the argument. a def that leaves its return type out says the same thing by returning the test, and callers narrow by that too:

def is_str(x):
    return isinstance(x, str)

def f(a: object):
    if is_str(a):
        a  # str
    else:
        a  # not str

what is recovered is what every return agrees on. a place is narrowed where the call is truthy only if every return that can hand back a truthy value narrows it, and a return that says nothing about the place leaves it unnarrowed. the falsy side is the same for the returns that can be falsy, and falling off the end of the body is one of those

so a test on each of two parameters narrows both where the call is truthy, and neither where it is falsy — a falsy and only says the conjunction failed:

def both(a, b):
    return a is int and b is str

def f(x: object, y: object):
    if both(x, y):
        x  # int
        y  # str
    else:
        x  # object

a guard names the argument a call passed, so a body that puts something else where that argument was has no claim to make about it — a parameter the body rebinds is not recovered from, nor is a member the body writes to:

def rebound(x):
    x = 1
    return x is int   # `True` whatever it was given, so it says nothing about it

a single place narrowed both ways is exactly what TypeIs[T] says, so that is how the recovered return type is written — and a result held in a variable carries it, the same as a written one. a guard set with no such spelling — several places, or one side only — rides on the signature instead, and narrows where the call itself is tested

def is_str(x):
    return isinstance(x, str)   # -> TypeIs[str]

def f(a: object):
    ok = is_str(a)
    if ok:
        a  # str

nothing is recovered where the body is not what a caller tests: an async def or a generator hands back a coroutine or a generator rather than what its returns say, and a predicate that calls itself would be proving itself

this is recovered alongside the return type itself, so it follows sound-types and infer-unannotated-signatures. an annotation is the whole of what a function declares: nothing is recovered beside one, and -> bool is a def saying its result is just a bool. an overridden base is the same — except for a narrowing return type, which is a claim about the body, so an override that tests something else is left to its own body and told where it differs

assertion guards¶

asserts declares a function that narrows once it returns, rather than one whose result is tested:

def check(x: int | None) -> asserts x:
    assert x

def f(a: int | None):
    check(a)
    a  # int

the narrowing is truthiness, the same as if a:, and it holds for the rest of the flow — a later assignment to a ends it. asserts not x narrows the other way:

def check_empty(x: str | None) -> asserts not x:
    if x:
        raise ValueError

an assertion guard returns None — it raises when the assertion doesn't hold — so it lowers to -> None:

def check(x: int | None) -> None:
    assert x

and asserts every place it names:

def check(a: int | None, b: str | None) -> asserts a is int and b:
    assert a is not None and b

every call narrows on the strength of the annotation, so the body has to establish what it asserts wherever it returns — at each return, and at the end of the body. ruling out None is not the same as truthiness, since 0 is still falsy:

def check(x: int | None) -> asserts x:  # error: `x` is `int` where the body ends
    if x is None:
        raise ValueError

a parameter is the argument the caller passed, so a body that assigns to it establishes nothing about the argument. the same goes for a place: a local of that name is a different place from the one a call narrows. a member is read back by the caller, so assigning to one is how a body establishes it:

class Holder:
    data: int | None = None

    def load(self) -> asserts self.data is not None:
        self.data = 1

an assertion an overridden method makes is one its callers rely on whatever the value they hold turns out to be, so an override makes the same assertion — its callers narrow by it too — and has to establish it in its own body. the guard follows the parameter by position, so an override may rename a positional-only parameter

some ways out of a body are left alone rather than checked: a return a finally suite can follow hands control back only once that suite has run, and what the suite leaves behind is not modelled. such a body is neither read as establishing an assertion nor reported for failing to. a ... body declares a function without implementing one — in a stub, an @overload, an @abstractmethod, or a Protocol — so the claim is for whatever implements it

what a body establishes is read the same way narrowing is, and rests on the same thing: a call that mutates what was narrowed, or an alias that writes to it, leaves the claim standing where it no longer holds. an argument a conversion rewrites is another such case — the callee is handed the converted value, while the narrowing lands on the place the call was written with

an assertion narrows when it is called as a statement, which is where an assertion is written. its value is the None it returns, so testing that value (if check(x):) or binding it (ok = check(x)) is an error — it gets no narrowing, and the test is always false. a call whose arguments are unpacked (check(*args)) doesn't say which argument reached the parameter, so it narrows nothing

an assertion that was never written down¶

a def that leaves its return type out and returns nothing asserts what its body establishes, and callers narrow by that too:

def check(x: int | None):
    assert x

def f(a: int | None):
    check(a)
    a  # int, and truthy

what is asserted is what every way out of the body agrees on — each return it can reach, and the end of the body — so an early return before the assertion leaves nothing asserted, and so does a body that catches its own failure. as with a predicate, a parameter the body rebinds asserts nothing, and neither does an async def, whose call does not run the body. a body that hands back a value is not an assertion, since the narrowing only reaches a call written as a statement

an override is handed what the method it overrides asserts, recovered or written, and is checked against it

asserting a type¶

asserts x is T narrows by a type instead of by truthiness, and is not removes one:

def check(x: int | str | None) -> asserts x is int:
    if x is not int:
        raise ValueError

def require(x: int | None) -> asserts x is not None:
    if x is None:
        raise ValueError

def f(a: int | str | None, b: int | None):
    check(a)
    a  # int
    require(b)
    b  # int

the type is an ordinary type expression, so asserts x is None narrows to None. as with a predicate, the asserted type has to fit the parameter it narrows — def check(x: int) -> asserts x is str is an error, since no int is ever a str. removing a type constrains nothing, so is not is unrestricted

naming nothing¶

a guard whose name is neither a parameter nor a place it can see narrows nothing at every call site, which is almost always a typo:

def check(value: int | None) -> asserts values:  # error: `values` is nothing
    assert value

scope¶

the place is T rewrite fires only where the return annotation is a single is comparison whose left side is a name or an attribute chain rooted at one. this disambiguates from identity checks elsewhere in the function:

• in the return annotation: x is str → TypeIs[str]
• anywhere else: x is y follows the identity-swap rules and lowers to isinstance(x, y)

chained comparisons (a is int is str) and other left operands — a subscript, a call — are ignored