mila-iqia / myia

Myia prototyping
MIT License
455 stars 46 forks source link

Check that node annotations are rexpected (when available). #374

Closed notoraptor closed 4 years ago

notoraptor commented 4 years ago

@breuleux @abergeron This is a PR to check node annotations in graph. What do you think ?

notoraptor commented 4 years ago

@breuleux Updated ! I successfully moved annotation checking into step_infer. However, I still us a specific annotation checking function, instead of amerge, to avoid many problems. In particular, amerge either returns an unspecific type (if forced is false), or will complain about type mismatch (if forced is true), while I need to, either return the more specific type (e.g. tuple vs tuple[int, int]), or check if types match perfectly (e.g tuple[int, int] vs tuple[int, float]).

notoraptor commented 4 years ago

@breuleux Hi ! I updated the code with your suggestions (using amerge(annotation, abstract, forced=True, bind_pending=True)). It fixed many issues, but I still had to add an overload to amerge to manage a specific case, when an annotation list (without arguments) is compared to a list (AbstractADT).

In such cases, type_to_abstract(list) returns an AbstractUnion, so AbstractUnion vs AbstractADT will fail, so I added a amerge(self, x1: AbstractUnion, x2: AbstractADT) to handle that.

What do you think?

breuleux commented 4 years ago

@notoraptor Good observation, I hadn't thought about that. This is a more general issue, I think. For instance, if the user annotates a variable x: Union[int, ndarray], should it be compatible with an inferred type of int or ndarray? I suppose that might correspond to user expectation in many cases, but at the same time, are we supposed to allow x.dot(y) if we can prove that x is an ndarray, even though the user explicitly declared that they think x could possibly be an int?

It's debatable.

Regarding amerge: it's not clear to me whether merging U[Empty, Cons] with Cons should yield U[Empty, Cons] or raise a type error (currently it does the latter, as you've experienced). However, what it should not do is yield Cons, because remember that we're also using this to merge branches of conditionals, so the result has to be the union of all possibilities. This is a case where merging the annotation might differ from the normal merging behavior.

Here's something we could try, which is a lot easier now that ovld supports multiple dispatch:

def amerge(self, x: AbstractUnion, y: AbstractValue):
    return self(x, AbstractUnion([y]))

def amerge(self, x: AbstractValue, y: AbstractUnion):
    # Note: should fail if forced=True
    return self(AbstractUnion([x]), y)

Basically, we'd always get a Union out. I'm curious how that plays out and if all the tests would still pass. I'm a bit hesitant about it, though.

An alternative, if we want to go the other way, would be to do this:

@amerge.variant
def annotation_merge(self, x: AbstractUnion, y: AbstractValue):
    # Reproduce the code you wrote for AbstractUnion and AbstractADT

annotation_merge would behave just like amerge except in this case, and it would not interfere with the existing merge behavior that's used for branches of if statements.

I would argue for the second solution, for the time being.

notoraptor commented 4 years ago

@breuleux hi ! New commit, I used the annotation_merge suggestion.

notoraptor commented 4 years ago

@breuleux Updated!

notoraptor commented 4 years ago

@breuleux Done ! PR updated.

notoraptor commented 4 years ago

Coverage seems OK, I don't know why Travis is failing.

breuleux commented 4 years ago

The Travis error looks like it's just a matter of retrying:

CondaHTTPError: HTTP 504 GATEWAY_TIMEOUT for url <https://conda.anaconda.org/mila-iqia/linux-64/tvm-0.7dev1 5.f11abf26-py37ha8d69ae_0.tar.bz2>
Elapsed: 01:00.013945
CF-RAY: 5d64a4b7cd47cf5c-IAD
An HTTP error occurred when trying to retrieve this URL.
HTTP errors are often intermittent, and a simple retry will get you on your way.