Simplifying casts and beta-reduction

[Conal Elliott]

Thanks, Jacques! That paper looks tremendously relevant to what I'm doing.
-- Conal


On Thu, May 8, 2014 at 5:01 AM, Jacques Carette <carette at mcmaster.ca> 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 <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
>>>
>>
>>
>
>
> _______________________________________________
> ghc-devs mailing listghc-devs at haskell.orghttp://www.haskell.org/mailman/listinfo/ghc-devs
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140508/3953b1f2/attachment.html>