New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
GHC backend: Automatically inline all projections? #1895
Comments
I thought that GHC automatically inlines small, simple functions. Perhaps it would be worthwhile investigating why inlining is not happening automatically in this case. |
Some time ago, I did some experiments: After some exploration, I arrived at the following patch:
The result is that the generated Haskell code explodes, with code of the following pattern (simplified for readability): ... = case v3 of
Constr1 v10 v11 v12 v13 v14 v15 -> case vX of
... -> ...
... -> case v3 of
Constr1 v50 v51 v52 v53 v54 v55 -> result (With default cases and I thought about adding a “case folding” pass to I currently think that the proper way would be something along the following lines:
With informal substitution notation, the example above would then become: ... = case v3 of
Constr1 v10 v11 v12 v13 v14 v15 -> case vX of
... -> ...
... -> result[ v50 := v10 , v51 := v11 , v52 := v12 , v53 := v13 , v54 := v14 , v55 := v15 ] @UlfNorell , @phile314: Does this make sense? I think this would introduce valuable sharing that is currently lost. Even if GHC might be able to reconstruct it with extremely aggressive options (I tried quite a few things in the past, with no significant success), it would still be very expensive on the GHC-compilation side. Unfortunately this proposal involves a lot more Agda internals than I am currently able to handle; I am not even confident that I could arrive at a way to set up that |
I thought there was a pass in the treeless compiler that would get rid of repeated cases, but of course that still would have the problem with the huge intermediate terms. This might make a nice code sprint for next week. |
Another option would be to not inline projection functions in ToTreless itself, but to add an additional pass inlining projection functions and making sure that we generate only one case expression per scrutinee (like wolfram outlined above). @UlfNorell I also thought there is such a pass. Maybe it only works on consecutive cases? |
For illustration, here is an example of what came out with that patch (I switched Haskell pretty-printing to PPInLine to avoid megabytes of spaces, and then manually indented):
This contains 15
Notice that
Sharing also the associated
|
To avoid changing the evaluation order, one could generate a pattern
|
Could this have any negative consequences, like for example causing space leaks? I haven't yet looked at this in detail, but it might be worth checking this before implementing. GHC's literature discusses this to some extent:
|
One factor coming in here to make a difference is that Agda has a module system. 😉 Another important difference is that Haskell datatypes are by default coinductive. (All I am arguing about here is about constructors for (at most) inductive datatypes. One might even make a difference between non-recursive records and inductive recursive records. Constructors for coinductive records in Agda will definitely need to be treated differently.) The pattern Without the let-floating, The trimmed-down source for the example above is:
The situation is quite typical:
(The fact that this example is about “proofs” does actually not make a difference: These proofs here are, for me, in general not irrelevant, since I sometimes need them for totality proofs from which I then extract total functions.) In many practical examples, the role of the |
Natalie Perna and I are currently working on this in https://github.com/natalieperna/agda/tree/stable-2.5-inline-projections . |
I only took a quick glance at your branch, but if I understood correctly you inline projections during the |
For instance `case x of c ys -> case x of c zs -> u` => `case x of c ys -> u[ys/zs]`. cc #1895
After learning about
{-# INLINE #-}
from the ChangeLog and seeing at the top of my profile output:, I added
INLINE
pragmas in the standard library forData.Product.Σ.proj₂
andData.Product.Σ.proj₁
, and obtained a 16% speed-up.Close to the top of the list in my profiling output, there are quite a few more record fields ─ shouldn't they all be inlined automatically?
Summary of the attached file ─ the important lines are the
runtime
of the compiled program (without profiling):2016-03-05_profiling_log.txt
The text was updated successfully, but these errors were encountered: