Simplifying casts and beta-reduction

newer
GHC not parsing TH pretty printed...

Conal Elliott

6 May 2014 6 May '14

11:50 p.m.

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

Attachments:

attachment.html (text/html — 2.9 KB)

Show replies by date

Conal Elliott

6 May 6 May

11:51 p.m.

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 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 -> b>_R -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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 _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

Simon Peyton Jones

7 May 7 May

4:28 a.m.

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:ghc-devs-bounces@haskell.org] On Behalf Of Conal Elliott Sent: 07 May 2014 04:50 To: ghc-devs@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 -> b>_R -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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))))

...

(\ (@ 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 _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

Conal Elliott

4:02 p.m.

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 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@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 07 May 2014 04:50 *To:* ghc-devs@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 -> b>_R -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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 _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

Conal Elliott

11:18 p.m.

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 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 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@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 07 May 2014 04:50 *To:* ghc-devs@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 -> b>_R -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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 _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

Simon Peyton Jones

8 May 8 May

3:54 a.m.

Yes, that’s right: simplCast is the guy. I can’t explain why it’s not working for you, though Simon From: conal.elliott@gmail.com [mailto:conal.elliott@gmail.com] On Behalf Of Conal Elliott Sent: 08 May 2014 04:19 To: Simon Peyton Jones Cc: ghc-devs@haskell.org Subject: Re: Simplifying casts and beta-reduction 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 mailto:conal@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 mailto:simonpj@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/ I hope that’s useful. Simon From: ghc-devs [mailto:ghc-devs-bounces@haskell.orgmailto:ghc-devs-bounces@haskell.org] On Behalf Of Conal Elliott Sent: 07 May 2014 04:50 To: ghc-devs@haskell.orgmailto:ghc-devs@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 -> b>_R -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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))))

...

(\ (@ 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 _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

Conal Elliott

3:32 p.m.

Thanks, Simon. I'll keep poking around. On Thu, May 8, 2014 at 12:54 AM, Simon Peyton Jones wrote:

...

Yes, that’s right: simplCast is the guy. I can’t explain why it’s not working for you, though

Simon

*From:* conal.elliott@gmail.com [mailto:conal.elliott@gmail.com] *On Behalf Of *Conal Elliott *Sent:* 08 May 2014 04:19 *To:* Simon Peyton Jones *Cc:* ghc-devs@haskell.org *Subject:* Re: Simplifying casts and beta-reduction

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 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 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@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 07 May 2014 04:50 *To:* ghc-devs@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 -> b>_R -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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 _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

Jacques Carette

8:01 a.m.

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#AdamsFM...: 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 mailto:conal@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 mailto:simonpj@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//

//

I hope that's useful.

Simon

*From:*ghc-devs [mailto:ghc-devs-bounces@haskell.org mailto:ghc-devs-bounces@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 07 May 2014 04:50 *To:* ghc-devs@haskell.org mailto:ghc-devs@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 > -> b>_R > -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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 _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 ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Conal Elliott

2:04 p.m.

Thanks, Jacques! That paper looks tremendously relevant to what I'm doing. -- Conal On Thu, May 8, 2014 at 5:01 AM, Jacques Carette 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. Adamshttp://www.informatik.uni-trier.de/%7Eley/pers/hd/a/Adams:Michael_D=.html, Andrew Farmerhttp://www.informatik.uni-trier.de/%7Eley/pers/hd/f/Farmer:Andrew.html, José Pedro Magalhães: Optimizing SYB is easy! PEPM 2014http://www.informatik.uni-trier.de/%7Eley/db/conf/pepm/pepm2014.html#AdamsFM...: 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 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
...
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@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 07 May 2014 04:50 *To:* ghc-devs@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 -> b>_R -> Sub (Sym (TFCo:R:Encode(->)[0] <a8>_N _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 _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@haskell.orghttp://www.haskell.org/mailman/listinfo/ghc-devs

4030

Age (days ago)

4031

Last active (days ago)

List overview

Download

8 comments

3 participants

participants (3)

Conal Elliott
Jacques Carette
Simon Peyton Jones

Simplifying casts and beta-reduction

tags

participants (3)