Hi Joachim. Thanks very much for the suggestions and the `-ddump-rules`
view. I wouldn't want to make people write `morph` rules for all
combinations of operations (like `(.)`) and categories, but perhaps as you
suggest those rules can be generated automatically.
Regards, - Conal
On Tue, Oct 3, 2017 at 7:52 AM, Joachim Breitner <m...@joachim-breitner.de>
wrote:
> Hi,
>
>
> Am Montag, den 02.10.2017, 17:03 -0700 schrieb Conal Elliott:
> > My questions:
> >
> > * Is it feasible for GHC to combine the constraints needed LHS and RHS
> to form an applicability condition?
> > * Is there any way I can make the needed constraints explicit in my
> rewrite rules?
> > * Are there any other work-arounds that would enable writing such
> RHS-constrained rules?
>
> if you are fine writing one RULE per _instance_ of C, the following
> works:
>
>
> {-# LANGUAGE ExplicitForAll, TypeApplications #-}
> {-# OPTIONS_GHC -Wall #-}
> module RuleFail where
> class C k where comp' :: k b c -> k a b -> k a c
>
> instance C (->) where comp' = (.)
> instance C (,) where comp' (_,a) (c,_) = (c,a)
>
> -- Late-inlining version to enable rewriting.
> comp :: C k => k b c -> k a b -> k a c
> comp = comp'
> {-# INLINE [0] comp #-}
>
> morph :: forall k a b. (a -> b) -> k a b
> morph _ = error "morph: undefined"
> {-# NOINLINE morph #-}
>
> {-# RULES "morph/(.)/->" forall f g. morph @(->) (g `comp` f) = morph
> g `comp` morph f #-}
> {-# RULES "morph/(.)/(,)" forall f g. morph @(,) (g `comp` f) =
> morph g `comp` morph f #-}
>
>
> Let’s look at the rules:
>
> $ ghc -O -c -ddump-rules RuleFail.hs
>
> ==================== Tidy Core rules ====================
> "morph/(.)/(,)" [ALWAYS]
> forall (@ b)
> (@ b1)
> (@ a)
> ($dC :: C (->))
> (f :: a -> b)
> (g :: b -> b1).
> morph @ (,) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
> = comp
> @ (,)
> @ b
> @ b1
> @ a
> $fC(,)
> (morph @ (,) @ b @ b1 g)
> (morph @ (,) @ a @ b f)
> "morph/(.)/->" [ALWAYS]
> forall (@ b)
> (@ b1)
> (@ a)
> ($dC :: C (->))
> (f :: a -> b)
> (g :: b -> b1).
> morph @ (->) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
> = comp
> @ (->)
> @ b
> @ b1
> @ a
> $dC
> (morph @ (->) @ b @ b1 g)
> (morph @ (->) @ a @ b f)
>
> As you can see, by specializing the rule to a specific k, GHC can
> include the concrete instance dictionary (here, $fC(,)) _in the rule_
> so it does not have to appear on the LHS. This is pretty much how
> specialization works.
>
> Is that a viable work-around for you? It involves boilerplate code, but
> nothing that cannot be explained in the documentation. (Or maybe TH can
> create such rules?)
>
>
> If this idiom turns out to be useful, I wonder if there is a case for
> -rules specified in type classes that get instantiated upon every
> instance, e.g.
>
> class C k where
> comp' :: k b c -> k a b -> k a c
> {-# RULES "morph/(.)/(,)" forall f g. morph @k (g `comp` f) =
> morph g `comp` morph f #-}
>
>
> Greetings,
> Joachim
> --
> Joachim Breitner
> m...@joachim-breitner.de
> http://www.joachim-breitner.de/
>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
