Simplifying casts and beta-reduction

[Conal Elliott]

P.S. Never mind the remark about `(-->)`. I inlined and simplified it away
in the example code.


On Tue, May 6, 2014 at 8:50 PM, Conal Elliott <conal at conal.net> wrote:

> 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/20140506/ddf46c86/attachment.html>