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?

Piassava

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.

Ula

Thanks! I had to change spin : Nat -> () to spin : Nat -> Bool (I'm guessing Idris realized () only has one inhabitant and optimized away the call to spin), but after that the executable took a moment to run regardless of which branch of the if' it went down. – Piassava

Yes, it would have erased the (). Actually in current master it does a much deeper erasure analysis so you'd probably have to do something like printing the result of spin n to make sure it was evaluated... – Ula

How come, if it is known that spin 1000 is terminating and have no side effects, that this expression is not evaluated at compile time and replaced by its result in the generated code, so that both versions of the if'-line would return their result immediately at run time? (Snowballs comment above indicates that it doesn't.) – Snowden

It's not necessarily easy to decide whether compile time evaluation is a good idea, even knowing that something is total - the result might end up being bigger than the input, or duplicating some intermediate value, for example. The compiler could probably do a lot more, but in general inlining needs a bit of care. – Ula