laziness, multiparametric classes

[mechvel]

Hello,
 I have the following beginner questions.
1. Is Idris going to have multiparametric classes?
2. May Idris have lazy evaluation?

Regards,
Sergei

[Edwin Brady]

Hi,

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

> Hello,
> I have the following beginner questions.
> 1. Is Idris going to have multiparametric classes?

It already does! Though no

> 2. May Idris have lazy evaluation?

You can use laziness annotations - you annotate function arguments with a vertical bar '|', or use the built in function lazy : a -> a.

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

Edwin.

[Serge D. Mechveliani]

On Sun, Jul 15, 2012 at 07:32:06PM +0100, Edwin Brady wrote:
> [..]

> > 2. May Idris have lazy evaluation?
>
> You can use laziness annotations - you annotate function arguments
> with a vertical bar '|', or use the built in function lazy : a -> a.
>
> This doesn't give you full laziness though, just means the argument
> isn't evaluated immediately.

For example, consider the following Haskell program for a
"complicated division with remainder" for positive integers.

-------------------------------------------------------------------
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,

------
Sergei
mec...@botik.ru