Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
plajjan opened this issue Sep 9, 2024 · 3 comments
Labels
Compiler Related to the Acton compiler enhancement New feature or request

Comments

@plajjan
Copy link
Contributor

plajjan commented Sep 9, 2024

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
Copy link
Contributor Author

plajjan commented Sep 9, 2024

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

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

@nordlander
Copy link
Contributor

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
Copy link
Contributor Author

plajjan commented Sep 19, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Compiler Related to the Acton compiler enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants