<div dir="ltr"><div><div>Thanks for the suggestion, Joachim.</div><div><br></div><div>Since I'm writing a core-to-core plugin anyway, it wasn't so hard for me to implement all of these n*m rules (for n operations and m instances) at once via a "built-in" rewrite rule that explicitly manipulates Core expressions. Doing so is probably also considerably more efficient than matching against many rewrite rules (whether generated manually or automatically), at least the way rewrite rule matching is currently implemented. As you & I discussed at ICFP, I'm looking for ways to reduce the complexity of the plugin to make it easier to maintain and extend, and I thought that dictionary synthesis from rewrite rules might be one.</div></div><div><br></div><div>Regards,</div><div>-- Conal</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 3, 2017 at 8:49 AM, Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<span class=""><br>
Now that I think about it: You can probably even generate these rules<br>
in a core2core pass that looks for instances of C, and then adds the<br>
</span>rules to the mod_guts. That would solve the problem neatly, I’d say.<br>
<br>
Greetings,<br>
Joachim<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
Am Dienstag, den 03.10.2017, 08:45 -0700 schrieb Conal Elliott:<br>
> Hi Joachim. Thanks very much for the suggestions and the `-ddump-<br>
> rules` view. I wouldn't want to make people write `morph` rules for<br>
> all combinations of operations (like `(.)`) and categories, but<br>
> perhaps as you suggest those rules can be generated automatically.<br>
><br>
> Regards, - Conal<br>
><br>
> On Tue, Oct 3, 2017 at 7:52 AM, Joachim Breitner <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>> wrote:<br>
> > Hi,<br>
> ><br>
> ><br>
> > Am Montag, den 02.10.2017, 17:03 -0700 schrieb Conal Elliott:<br>
> > > My questions:<br>
> > ><br>
> > > * Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?<br>
> > > * Is there any way I can make the needed constraints explicit in my rewrite rules?<br>
> > > * Are there any other work-arounds that would enable writing such RHS-constrained rules?<br>
> ><br>
> > if you are fine writing one RULE per _instance_ of C, the following<br>
> > works:<br>
> ><br>
> ><br>
> > {-# LANGUAGE ExplicitForAll, TypeApplications #-}<br>
> > {-# OPTIONS_GHC -Wall #-}<br>
> > module RuleFail where<br>
> > class C k where comp' :: k b c -> k a b -> k a c<br>
> ><br>
> > instance C (->) where comp' = (.)<br>
> > instance C (,) where comp' (_,a) (c,_) = (c,a)<br>
> ><br>
> > -- Late-inlining version to enable rewriting.<br>
> > comp :: C k => k b c -> k a b -> k a c<br>
> > comp = comp'<br>
> > {-# INLINE [0] comp #-}<br>
> ><br>
> > morph :: forall k a b. (a -> b) -> k a b<br>
> > morph _ = error "morph: undefined"<br>
> > {-# NOINLINE morph #-}<br>
> ><br>
> > {-# RULES "morph/(.)/->" forall f g. morph @(->) (g `comp` f) = morph g `comp` morph f #-}<br>
> > {-# RULES "morph/(.)/(,)" forall f g. morph @(,) (g `comp` f) =<br>
> > morph g `comp` morph f #-}<br>
> ><br>
> ><br>
> > Let’s look at the rules:<br>
> ><br>
> > $ ghc -O -c -ddump-rules RuleFail.hs<br>
> ><br>
> > ==================== Tidy Core rules ====================<br>
> > "morph/(.)/(,)" [ALWAYS]<br>
> > forall (@ b)<br>
> > (@ b1)<br>
> > (@ a)<br>
> > ($dC :: C (->))<br>
> > (f :: a -> b)<br>
> > (g :: b -> b1).<br>
> > morph @ (,) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)<br>
> > = comp<br>
> > @ (,)<br>
> > @ b<br>
> > @ b1<br>
> > @ a<br>
> > $fC(,)<br>
> > (morph @ (,) @ b @ b1 g)<br>
> > (morph @ (,) @ a @ b f)<br>
> > "morph/(.)/->" [ALWAYS]<br>
> > forall (@ b)<br>
> > (@ b1)<br>
> > (@ a)<br>
> > ($dC :: C (->))<br>
> > (f :: a -> b)<br>
> > (g :: b -> b1).<br>
> > morph @ (->) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)<br>
> > = comp<br>
> > @ (->)<br>
> > @ b<br>
> > @ b1<br>
> > @ a<br>
> > $dC<br>
> > (morph @ (->) @ b @ b1 g)<br>
> > (morph @ (->) @ a @ b f)<br>
> ><br>
> > As you can see, by specializing the rule to a specific k, GHC can<br>
> > include the concrete instance dictionary (here, $fC(,)) _in the rule_<br>
> > so it does not have to appear on the LHS. This is pretty much how<br>
> > specialization works.<br>
> ><br>
> > Is that a viable work-around for you? It involves boilerplate code, but<br>
> > nothing that cannot be explained in the documentation. (Or maybe TH can<br>
> > create such rules?)<br>
> ><br>
> ><br>
> > If this idiom turns out to be useful, I wonder if there is a case for<br>
> > -rules specified in type classes that get instantiated upon every<br>
> > instance, e.g.<br>
> ><br>
> > class C k where<br>
> > comp' :: k b c -> k a b -> k a c<br>
> > {-# RULES "morph/(.)/(,)" forall f g. morph @k (g `comp` f) = morph g `comp` morph f #-}<br>
> ><br>
> ><br>
> > Greetings,<br>
> > Joachim<br>
> > --<br>
> > Joachim Breitner<br>
> > <a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a><br>
> > <a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.<wbr>de/</a><br>
><br>
><br>
--<br>
Joachim Breitner<br>
<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a><br>
<a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.<wbr>de/</a><br>
</div></div></blockquote></div><br></div>