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
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 ->
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