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

[Relay] Check match expressions for completeness #3203

Merged
merged 8 commits into from
Jun 13, 2019

Conversation

slyubomirsky
Copy link
Contributor

@slyubomirsky slyubomirsky commented May 16, 2019

We never defined the semantics of an incomplete match in Relay, so I've written a fairly simple function to check whether a match is complete (there's probably a better algorithm, but this one also concretely finds all cases that are not handled) and added into the type checker.

This did require me to change several functions that relied on having incomplete matches, such as hd and tl. I do not think we should permit partial functions, as that would require us to define semantics for incomplete matches and potentially, down the line, to complicate the language with other kinds of error handling that could be placed higher in the stack (e.g., it would be a problem if some execution settings for Relay had one kind of error for incomplete matches and others reported the error a different way).

I suppose, though, that it would be easy to change the match incompleteness to a warning rather than an error if we really do want to keep hd, tl, etc.

Incomplete matches only generate a warning for now, though we may want to add flags to make this an error later, see @MarisaKirisame's comment below

@MarisaKirisame
Copy link
Contributor

@slyubomirsky can you make it LOG(WARNING) if a pattern is not exhausted right now? I think we should touch the hd/nth/tl function later.
So I think there is 3 pr:
0: the exhaustiveness checker that warn stuff
1: a flag 'strict' in the match node that check for exhaustiveness, and possibly redundancy later
2: discuss what to do with the partial functions, as @icemelon9 is using them.
I think we can take a similar approach as http://hackage.haskell.org/package/safe: provide version that is easiest to use, provide one that return default, provide one that return Maybe, etc.

@slyubomirsky
Copy link
Contributor Author

I agree, I'll make it a warning

@MarisaKirisame
Copy link
Contributor

@slyubomirsky http://moscova.inria.fr/~maranget/papers/warn/index.html
this paper conver redundancy as well. It's exhaustiveness algorithm is different. I think we can keep ours as it is, unless it get too slow.

@tqchen
Copy link
Member

tqchen commented May 24, 2019

for (size_t i = 0; i < op->patterns.size(); i++) {
MatchResult submatch = this->Check(op->patterns[i], ctor_cand->patterns[i]);
if (submatch != MatchResult::kMatch) {
return submatch;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you can be more aggressive here: if any of the child is clash, return clash

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point, I'll do that.

@MarisaKirisame
Copy link
Contributor

one small nitpick, otherwise is good.

@slyubomirsky
Copy link
Contributor Author

Pinging @MarisaKirisame and @icemelon9 for final review

@tqchen tqchen merged commit a698ad7 into apache:master Jun 13, 2019
wweic pushed a commit to wweic/tvm that referenced this pull request Jun 26, 2019
wweic pushed a commit to neo-ai/tvm that referenced this pull request Jun 27, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants