Simplifying casts and beta-reduction

[Conal Elliott]

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> 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>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:ghc-devs-bounces at haskell.org] *On Behalf Of *Conal
>> Elliott
>> *Sent:* 07 May 2014 04:50
>> *To:* 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
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140507/0a471bc0/attachment-0001.html>