Thanks, Jacques! That paper looks tremendously relevant to what I'm doing. -- Conal
On Thu, May 8, 2014 at 5:01 AM, Jacques Carette <[email protected]> wrote: > Sorry to jump in mid-conversation, but since I read about people doing > exactly this a few days ago, I thought this might be useful. See the paper > Michael D. > Adams<http://www.informatik.uni-trier.de/%7Eley/pers/hd/a/Adams:Michael_D=.html>, > Andrew > Farmer<http://www.informatik.uni-trier.de/%7Eley/pers/hd/f/Farmer:Andrew.html>, > José Pedro Magalhães: Optimizing SYB is easy! PEPM > 2014<http://www.informatik.uni-trier.de/%7Eley/db/conf/pepm/pepm2014.html#AdamsFM14>: > 71-82 > http://www.ittc.ku.edu/csdl/fpg/files/Adams-13-OSIE.pdf > > where they use Hermit > http://www.ittc.ku.edu/csdl/fpg/software/hermit.html > http://hackage.haskell.org/package/hermit > to do exactly this transformation [and a fair bit more]. > > Jacques > > > On 2014-05-07 11:18 PM, Conal Elliott wrote: > > 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 > [email protected]http://www.haskell.org/mailman/listinfo/ghc-devs > > >
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
