I'm still sorting through how to optimize these almost-beta-redexes in the form `((\ x -> u) |> co) v`, shifting coercions to enable beta-reduction (as described in section 3.1 of "Evidence normalization"). Is it done by `simplCast` (with help from `simplCoercion`), as called indirectly from `simplifyExpr` in `SimplCore`? I think I'm now calling `simplifyExpr` from HERMIT but I'm not getting the cast-shifting I'm looking for.
-- Conal On Wed, May 7, 2014 at 1:02 PM, Conal Elliott <[email protected]> wrote: > Very useful, indeed! Exactly what I was looking for. Thanks, Simon. Now > I've read the evidence normalization and the deferred types paper, and I > have a much better understanding of what's going on. > > -- Conal > > > > On Wed, May 7, 2014 at 1:28 AM, Simon Peyton Jones > <[email protected]>wrote: > >> Absolutely. There’s a whole module that does this: OptCoercion. If you >> want to see what programs look like without coercion optimisation, try >> –fno-opt-coercion. >> >> >> >> The rules are described in our paper *Evidence normalization in System >> FC: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ >> <http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/>* >> >> >> >> I hope that’s useful. >> >> >> >> Simon >> >> >> >> *From:* ghc-devs [mailto:[email protected]] *On Behalf Of *Conal >> Elliott >> *Sent:* 07 May 2014 04:50 >> *To:* [email protected] >> *Subject:* Simplifying casts and beta-reduction >> >> >> >> I'm looking for tools to help simplify Core terms that involve casts. In >> particular, I want to beta-reduce when the function is wrapped with a cast. >> Do the GHC sources have such utility functions? >> >> Here is an example of a lambda expression with a cast. In context, it's >> applied to two type arguments and two dictionary arguments and returns a >> function of one more argument. (The function `(-->)` is defined as `(f --> >> h) g = h . g . f`.) >> >> > ((\ (@ a8) (@ b) >> > ($dEncodable :: Encodable a8) >> > ($dEncodable1 :: Encodable b) -> >> > case $dEncodable of _ >> > D:Encodable _ tpl_B3 -> >> > case $dEncodable1 of _ >> > D:Encodable tpl_B2 _ -> >> > \ (g :: a8 -> b) (eta :: Encode a8) -> tpl_B2 (g (tpl_B3 >> eta)) >> > ) >> > `cast` (forall a8 b. >> > <Encodable a8>_R >> > -> <Encodable b>_R >> > -> <a8 -> b>_R >> > -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N <b>_N)) >> > :: (forall a8 b. (Encodable a8, Encodable b) => >> > (a8 -> b) -> Encode a8 -> Encode b) >> > ~# >> > (forall a8 b. (Encodable a8, Encodable b) => >> > (a8 -> b) -> Encode (a8 -> b)))) >> >> I can imagine pushing the `cast` down through the type lambdas while >> stripping off `forall` coercions, then pushing the remaining `cast` through >> the dictionary arguments, while stripping off the outer `<Encodable t>_R >> ->` coercion wrappers, and then pushing the cast into the `case` >> alternatives and the lambda body, leaving something like >> >> > (\ (@ a8) (@ b) >> > ($dEncodable :: Encodable a8) >> > ($dEncodable1 :: Encodable b) -> >> > case $dEncodable of _ >> > D:Encodable _ tpl_B3 -> >> > case $dEncodable1 of _ >> > D:Encodable tpl_B2 _ -> >> > \ (g :: a8 -> b) -> >> > (\ (eta :: Encode a8) -> tpl_B2 (g (tpl_B3 eta))) >> > `cast` (Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N <b>_N)) >> > :: (Encode a8 -> Encode b) >> > ~# >> > (Encode (a8 -> b)))) >> >> Now, given type, dictionary, and function arguments, I think we could >> beta-reduce. >> >> Before I try implementing these transformations, does something like them >> already exist in GHC? >> >> Thanks, -- Conal >> > >
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
