<div dir="ltr">Here are a few variants<div><br></div><div><div>open import Agda.Builtin.Strict</div><div><br></div><div>case_of_ : {A B : Set} → A → (A → B) → B</div><div>case x of f = f x</div><div>{-# INLINE case_of_ #-}</div><div><br></div><div>test1 test2 test3 test4 : {A B : Set} → (B → A) → (A → A → B) → B → B</div><div>test1 f g x = let u = f x in g u u</div><div>test2 f g x = case f x of λ u → g u u</div><div>test3 f g x = g u u where u = f x</div><div>test4 f g x = primForce (f x) λ u → g u u</div></div><div><br></div><div>These compile to the following code (in our intermediate language, which maps more or less directly to Haskell):</div><div><br><div>test1 = λ a b c d e → d (c e) (c e)</div><div>test2 = λ a b c d e → let f = c e in d f f</div><div>u     = λ a b c d e → u' c e</div><div>u'    = λ a b → a b</div><div>test3 = λ a b c d e → d (u' c e) (u' c e)</div><div>test4 = λ a b c d e → let f = c e in seq f (d f f)</div></div><div><br></div><div>test1 and test3 are pretty much equally bad (ghc will most likely inline u').</div><div>test2 is good for run-time performance, but bad for compile-time (due to call-by-name).</div><div>test4 is good for both run-time and compile-time provided you're ok with being strict in f x</div><div><br></div><div>If you want to see the intermediate code produced by the compiler you can give the flag -v treeless:20 when compiling.</div><div><br></div><div>/ Ulf</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 27, 2017 at 10:59 AM,  <span dir="ltr"><<a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Nils Anders Danielsson писал <a href="tel:26.06.2017%2016" value="+12606201716" target="_blank">26.06.2017 16</a>:52:<span class=""><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 2017-06-25 16:26, Sergei Meshveliani wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
1. It appears that final  fn - fn  in my test costs as much as all the<br>
    rest.<br>
</blockquote>
<br>
As far as I know Agda transforms "let fn = f n in fn - fn" into<br>
"f n - f n".<br>
</blockquote>
<br>
<br></span>
I am sorry, I was in a hurry and missed the point.<br>
<br>
What may be a reason for writing<br>
<br>
 g1 u + g2 u + g3 u     -- (I)<br>
 where<br>
 u = f x (y * z)<br>
<br>
instead of<br>
<br>
 g1 (f x (y * z)) + g2 (f x (y * z)) + g3 (f x (y * z))    -- (II)<br>
<br>
?<br>
<br>
Can there be any reason other than readability of the source program?<br>
<br>
When `making' (II):<br>
after applying MAlonzo, it starts  GHC -O.<br>
And I expect that it will convert (II) into (I) or into "let - in".<br>
Will it?<br>
<br>
Anyway, this optimization is not reliable. So that in a Haskell program (for GHC) it is bettter to write (I) both for readability and for an reliable optimization, to be sure that computing by new the values like  u  is not repeated.<br>
<br>
Right?<br>
<br>
Now, what needs to be the approach with Agda?<br>
Agda converts (I) into (II) (does it?).<br>
<br>
How to write the program so that to be sure that run-time computing the values like  u  is not repeated?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>