[Agda] summing rationals

[Ulf Norell]

Here are a few variants

open import Agda.Builtin.Strict

case_of_ : {A B : Set} → A → (A → B) → B
case x of f = f x
{-# INLINE case_of_ #-}

test1 test2 test3 test4 : {A B : Set} → (B → A) → (A → A → B) → B → B
test1 f g x = let u = f x in g u u
test2 f g x = case f x of λ u → g u u
test3 f g x = g u u where u = f x
test4 f g x = primForce (f x) λ u → g u u

These compile to the following code (in our intermediate language, which
maps more or less directly to Haskell):

test1 = λ a b c d e → d (c e) (c e)
test2 = λ a b c d e → let f = c e in d f f
u     = λ a b c d e → u' c e
u'    = λ a b → a b
test3 = λ a b c d e → d (u' c e) (u' c e)
test4 = λ a b c d e → let f = c e in seq f (d f f)

test1 and test3 are pretty much equally bad (ghc will most likely inline
u').
test2 is good for run-time performance, but bad for compile-time (due to
call-by-name).
test4 is good for both run-time and compile-time provided you're ok with
being strict in f x

If you want to see the intermediate code produced by the compiler you can
give the flag -v treeless:20 when compiling.

/ Ulf


On Tue, Jun 27, 2017 at 10:59 AM, <mechvel at scico.botik.ru> wrote:

> 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170627/80cbd7c4/attachment.html>