-
Notifications
You must be signed in to change notification settings - Fork 37
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
Figure out how match flattening affects us #113
Comments
It looks like match flattening was the cause of huge memory usage during compilation of |
It also seems that there might have been a bug in the implementation of match flattening, which caused failure of Singletons/Nat test. See #97. |
This fails because takeWhile can't be singletonized, which in turn is because of #113 and friends. Oh well.
This fails because takeWhile can't be singletonized, which in turn is because of #113 and friends. Oh well.
There is lots of good data on this issue in #96. But it's not exactly the data that we need. The big question I have about the performance blowup is where, precisely, it's happening. First, we need to know what the trigger is. The data in #96 suggests that the blowup happens with both Question 2: Where, precisely, is the blowup happening? Here are some possibilities:
Perhaps the blowup is happening at multiple places! But we need to discover which pass is causing problems before we can start addressing them. I don't think it's terribly hard to do this, but it would take some time and attention to details. Once we're sure that And then there's question 3: even when things aren't terrible, how bad is match-flattening in the average case? Does it increase all compilations by 20%? Code size? Is it worth the cost? If you want to explore this, you'll want to enable match-flattening again. Take a look at commit 87aa901. Restore the Do let me know if you're taking this on! :) |
Not in the next weeks - I'm totally swamped with teaching and once this is over (in two weeks) I plan to take on generalized injectivity. |
To be clear: my "you" was addressed to any reader out there in cyberspace. Not you, Janek, specifically. :) |
I admit that this possibility crossed my mind when writing my comment :-) |
In the
master
branch, all pattern-matches are "flattened" before further processing. This is done fromscLetDec
insquashWildcards
, called insingTopLevelDecs
. This is a drastic change, meaning that no patterns are overlapped anymore. How is this change affecting us? Is the code bloat truly terrible? How are compilation times? Pattern-match flattening allows some nice things -- in particular, it allows singletonization of functions with overlapping patterns. But is the cost too high? If the cost is high, is there a way to detect when match flattening is a good idea? Should we ask the user for assistance?The text was updated successfully, but these errors were encountered: