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, Andrew Farmer, José Pedro Magalhães: Optimizing SYB is easy! PEPM 2014: 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@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@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@haskell.org] On Behalf Of Conal Elliott
Sent: 07 May 2014 04:50
To: ghc-devs@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@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs