Simplifying casts and beta-reduction

[Jacques Carette]

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 <conal at conal.net 
> <mailto:conal at conal.net>> 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
>     <simonpj at microsoft.com <mailto:simonpj at microsoft.com>> 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//
>
>         //
>
>         I hope that's useful.
>
>         Simon
>
>         *From:*ghc-devs [mailto:ghc-devs-bounces at haskell.org
>         <mailto:ghc-devs-bounces at haskell.org>] *On Behalf Of *Conal
>         Elliott
>         *Sent:* 07 May 2014 04:50
>         *To:* ghc-devs at haskell.org <mailto:ghc-devs at haskell.org>
>         *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
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140508/3445496a/attachment.html>