[Agda] summing rationals

[mechvel at scico.botik.ru]

Nils Anders Danielsson писал 26.06.2017 16:52:
> On 2017-06-25 16:26, Sergei Meshveliani wrote:
>> 1. It appears that final  fn - fn  in my test costs as much as all the
>>     rest.
> 
> As far as I know Agda transforms "let fn = f n in fn - fn" into
> "f n - f n".


I am sorry, I was in a hurry and missed the point.

What may be a reason for writing

  g1 u + g2 u + g3 u     -- (I)
  where
  u = f x (y * z)

instead of

  g1 (f x (y * z)) + g2 (f x (y * z)) + g3 (f x (y * z))    -- (II)

?

Can there be any reason other than readability of the source program?

When `making' (II):
after applying MAlonzo, it starts  GHC -O.
And I expect that it will convert (II) into (I) or into "let - in".
Will it?

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.

Right?

Now, what needs to be the approach with Agda?
Agda converts (I) into (II) (does it?).

How to write the program so that to be sure that run-time computing the 
values like  u  is not repeated?

Thanks,

------
Sergei