confused about lazy evaluation in Idris

Question

Reading and playing around with some examples from the official Idris tutorial has left me a bit confused regarding lazy evaluation.

As stated in the tutorial Idris uses eager evaluation, and they go on to give an example where this would not be appropriate

ifThenElse : Bool -> a -> a -> a
ifThenElse True  t e = t
ifThenElse False t e = e

And they then proceed to show an example using lazy evaluation

ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True  t e = t
ifThenElse False t e = e

I like to try things out while reading, so I created an inefficient Fibonacci function to test out the non-lazy and lazy ifThenElse.

fibo : Nat -> Nat
fibo Z = Z
fibo (S Z) = S Z
fibo (S(S Z)) = S(S Z)
fibo (S(S(S n))) = fibo (S(S n)) + fibo (S n)

-- the non lazy
ifThenElse1 : Bool -> (t: a) -> (f: a) -> a
ifThenElse1 False t f = f
ifThenElse1 True t f = t

-- should be slow when applied to True
iftest1 : Bool -> Nat
iftest1 b = ifThenElse1 b (fibo 5) (fibo 25)

-- the lazy
ifThenElse2 : Bool -> (t: Lazy a) -> (f: Lazy a) -> a
ifThenElse2 False t f = f
ifThenElse2 True t f = t

-- should be fast when applied to True
iftest2 : Bool -> Nat
iftest2 b = ifThenElse2 b (fibo 5) (fibo 25)

Given that Idris should be performing eager evaluation, I would expect the execution of iftest1 to be slowed down by (fibo 25) even when applied to True. However, both iftest1 and iftest2 execute very fast when applied to True. So maybe my understanding of lazyness/eagerness is fundamentally flawed?

What is a good example to observe the difference between lazyness and eagerness in Idris?

Answer 1

You probably tried iftest1 and iftest2 from the Idris REPL. The REPL uses different evaluation order than compiled code:

Being a fully dependently typed language, Idris has two phases where it evaluates things, compile-time and run-time. At compile-time it will only evaluate things which it knows to be total (i.e. terminating and covering all possible inputs) in order to keep type checking decidable. The compile-time evaluator is part of the Idris kernel, and is implemented in Haskell using a HOAS (higher order abstract syntax) style representation of values. Since everything is known to have a normal form here, the evaluation strategy doesn’t actually matter because either way it will get the same answer, and in practice it will do whatever the Haskell run-time system chooses to do.

The REPL, for convenience, uses the compile-time notion of evaluation.