categorifier icon indicating copy to clipboard operation
categorifier copied to clipboard

improve support for weaker categories

Open zliu41 opened this issue 3 years ago • 1 comments

Currently, something like uncurry (+) requires a CCC, but, it actually expands to uncurry . curry . plusC, which should be simplifiable to plusC, which only requires a Cartesian category (and appropriate NumCat instance).

The existing implementation converts to the new category too eagerly, which means we need to resolve the CCC instance before we get around to simplifying. Instead, we should categorize in Hask, allowing simplifications like uncurry . curry = id to be performed, then convert to the target category.

This would also reduce the reliance on inlining/rules in the target category in order to get efficient representations.


Greg Pfeil September 16, 2020, 9:19 AM

The reason the current implementation converts to the target early is because it means we get errors earlier. If we went from \x -> foo (bar x) → foo . bar (staying in (->) as our category), we wouldn’t get a failure about skipping some component of categorization until after everything had been categorized, because both the first and second forms have the same type. By switching categories, we switch the type of the arrows, and so GHC complains to us immediately when they don’t line up.

We could potentially get the best of both worlds if we converted to Hask (as used for the plugin tests) in the first phase, then substitute Hask → cat in the second phase. This should work since Hask is isomorphic to (->), but still a distinct type.

Then, as long as the Hask instances have good rules (like curry . uncurry == id), we should get the simplified representation out the other end.


Greg Pfeil May 19, 2020, 12:37 PM

This would probably also require enabling sm_rules in the simplifier in Categorize.hs (so that things like uncurry . curry get rewritten away … but maybe inlining will take care of that).

(Extricated from https://kitty-hawk.atlassian.net/browse/SW-1940)

zliu41 avatar Feb 23 '22 06:02 zliu41

We could potentially get the best of both worlds if we converted to Hask (as used for the plugin tests) in the first phase, then substitute Hask → cat in the second phase. This should work since Hask is isomorphic to (->), but still a distinct type.

This two-step approach is similar to what concat does, except it uses "regular" RULES to do the first conversion, then the plugin to replace -> with the target category. The problems there are that it means the class hierarchy isn't swappable, and also the second step could inadvertently change a -> that shouldn't change into the target category. So using Hask would also help avoid that problem.

sellout avatar Feb 26 '22 00:02 sellout