On 15 Jul 2012, at 19:30, mechvel wrote:

This doesn't give you full laziness though, just means the argument isn't evaluated immediately.

-------------------------------------------------------------------
genDivRem :: Integer -> Integer -> (Integer, Integer)
                                    -- quot  rem
genDivRem n m =  cDRem 0 n
                 where
                 cDRem q r = if r < m then (q, r)
                             else          cDRem (q + (count q)) (r-m)

count :: Integer -> Integer
count n =  cn (n^6)           -- to make the first component expensive
           where
           cn n = if n < 0 then 1  else  cn (n-1)

genRem :: Integer -> Integer -> Integer
genRem n m =  snd (genDivRem n m)

genQuot :: Integer -> Integer -> Integer
genQuot n m =  fst (genDivRem n m)

main = putStr (shows (genRem 40 2) "\n")
                      -- genQuot
-------------------------------------------------------------------

I program _only_  genDivRem,  and further, use

    genDivRem n m,  snd (genDivRem n m),  fst (genDivRem m n),

depending on what it is needed.
And, for example,              genRem 40 2 =  snd (genDivRem 40 2)
works fast due to laziness.

In a _strict_ language, this approach would not do, because
snd (genDivRem m n)  will cause a great volume of unneeded computation
in the first component.
In a _strict_ language, one needs to program a separate loop for
computing the remainder only.
This approach complicates program systems.

Now, in  Idris,  how may it look a similar program and a similar usage
for   genDivRem m n  with using the laziness annotation?

Thank you for explanation,