Idris eager evaluation

Question

In Haskell, I might implement if like this:

if' True  x y = x
if' False x y = y
spin 0 = ()
spin n = spin (n - 1)

This behaves how I expect:

haskell> if' True  (spin 1000000) ()  -- takes a moment
haskell> if' False (spin 1000000) ()  -- immediate

---

In Racket, I could implement a flawed if like this:

(define (if2 cond x y) (if cond x y))
(define (spin n) (if (= n 0) (void) (spin (- n 1))))

This behaves how I expect:

racket> (if2 #t (spin 100000000) (void))  -- takes a moment
racket> (if2 #f (spin 100000000) (void))  -- takes a moment

---

In Idris, I might implement if like this:

if' : Bool -> a -> a -> a
if' True  x y = x
if' False x y = y
spin : Nat -> ()
spin Z = ()
spin (S n) = spin n

This behavior surprises me:

idris> if' True  (spin 1000) ()  -- takes a moment
idris> if' False (spin 1000) ()  -- immediate

I expected Irdis to behave like Racket, where both arguments are evaluated. But that's not the case!

How does Idris decide when to evaluate things?

Answer 1

We say Idris has strict evaluation, but this is for its run-time semantics.

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. So, your 'spin 1000' is never actually getting evaluated. If you make an executable with the same code, I would expect to see very different behaviour.

As well as being easier to implement (because we have the evaluator available) this can be very useful to show how terms evaluate in the type checker. So you can see the difference between:

Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat

Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat

This would be harder (though not impossible) if we used the run-time evaluation at the REPL, which doesn't reduce under lambdas.