Track narrowed expressions in type-checker e.g. to support if a.b is not None

[plajjan]

We should track a set of narrowed expressions in the type checker to allow for more natural use of e.g. if a.b is not None or isinstance(a.b, int)

This is from #1401 but reshaped here to be more focused (other solutions / partial workarounds are mentioned in #1401).

class Apa(object):
    def __init__(self, b: ?int):
        self.b = b

actor main(env):
    a = Foo(1)
    if a.b is not None:
        sum = 1337 + a.b
        call_some_func(a) # call_some_func() will still see a with an optional b attribute
        print(sum)
    env.exit(0)

This means that in this scope, a.b will have a narrower type. However, when a is passed around, it will still have the optional b. It is only a.b when accessed exactly as a.b that has the narrower type.

[plajjan]

@nordlander can we track a dict key as a narrowed expression?

if isinstance(foo["hello"]):
    blargh = foo["hello"]

[nordlander]

I suppose the question is really whether we can dynamically check if expression foo is an instance of dict[str,...]. If so the answer is no, not in the desired amount of detail.

What we can do is to check if foo is an instance of class dict, by writing isinstance(foo, dict). So the second parameter to built-in construct isinstance must always be a class name, it can't be a full-blown type expression including type parameters. While we do carry around the actual class of every object at run-time (it's just an aspect of the object's method table), we don't (and can't) keep track of their possible type arguments for the simple reason that these aren't necessarily accessible as object attributes. For a generic function object, the argument and return types are only intermittently determined while the function is being invoked. And for a dict object, the key and value types could only be dynamically traced provided the dict is not empty. Etc, etc.

Instead we rely on type inference to validate an expression like foo["hello"], which is only correct if foo can be statically inferred to support the protocol Indexed[str,T] for some T. This doesn't automatically force foo to be a dict, though, so the question isinstance(foo, dict) might actually be valid in some contexts.

That said, we also have a loop-hole in the current type-checker when it comes to isinstance, in the sense that if the static type of foo is object --- a type that doesn't mention the type parameters of its potential subtype dict[K,V] --- we actually have no right to assume any concrete type for K and V after we've concluded that isinstance(foo, dict) is true. All we are really entitled to do in this case is to treat the foo dict in a fully generic way (like computing its length), which works equally well whatever K and V happens to be. But for this to be statically verifiable we need to introduce the concept of existential types to the type system, which I think is better to defer until we're ready to implement fully-fledged pattern matching.

[plajjan]

Sorry, I don't know what happened there, I just seem to have left out parts of the example. Here's a fixed and more complete one:

foo = {
    "hello": "world",
    "answer": 42
}

def function_that_takes_a_str(s: str):
    print(s)

def function_that_takes_an_int(s: int):
    print(s)

actor main(env):
    if isinstance(foo["hello"], str):
        function_that_takes_a_str(foo["hello"])

    if isinstance(foo["foo"], int):
        function_that_takes_an_int(foo["foo"])
    env.exit(0)

so what I mean by tracking the dict key is that we isinstance check the value that the key maps to, not the key itself.

[plajjan]

@nordlander and I spoke about this separately and yes, dict key accesses like that should act the same way, we can narrow it. I suppose it's general, so we can narrow any expression?

[nordlander]

Yes, this feature is on the to-do list. But type narrowing will be tied to the syntax of the expressions matched, so the following won't work:

    if isinstance(foo["hello"], str):
        function_that_takes_a_str(foo["hel" + "lo"])

Also, the matched expresssions will have to be pure, otherwise we can't guarantee that a repeated occurrence evaluates to an identical instance.

[plajjan]

@nordlander right, but it is still based on like the AST, so whitespace or like which quoting character is used is irrelevant, right? Like this, (note " vs '):

    if isinstance(foo["hello"], str):
        function_that_takes_a_str(foo['hello'])

[nordlander]

Exactly, expression matching will be done on the abstract syntax.

[plajjan]

I would like to make it possible to use this like a guard statement. Swift has an explicit guard statement, which is basically like an if but with an early exit. It guarantees that in the rest of the scope from the guard and down, something holds true. For example, here to check for a non-optional value:

func checkAge() {
	
  var age: Int? = 22

  guard let myAge = age else {
    print("Age is undefined")
    return
  }

  print("My age is \(myAge)")
}

checkAge()

guards are nice since we can do a bunch of conditions but avoid heavy nesting. However, I don't really understand why the guard needs to be its own statement. Perhaps subject to taste.

Anyway, I would like to be able to do:

def foo(a: ?int) -> int:
     if a == None:
         raise ValueError("a should really not be None")

     # This is the inverse of the if (which does early return) i.e. a must be != None at this point and thus any access below can know that a is non-optional!!

     return a * 3.1415