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 <[email protected]
<mailto:[email protected]>> 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
<[email protected] <mailto:[email protected]>> 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:[email protected]
<mailto:[email protected]>] *On Behalf Of *Conal
Elliott
*Sent:* 07 May 2014 04:50
*To:* [email protected] <mailto:[email protected]>
*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
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
