Is Idris really "strictly evaluated?"

Question

Coming from Haskell, I was reading about Idris' story regarding laziness (non-strictness). I trolled the recent release notes, and found code akin to the following

myIf : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
myIf True t e = t
myIf False t e = e

I wrote a simple factorial function to test it

myFact : Int -> Int
myFact n = myIf (n == 1) 1 (n * myFact (n-1))

I ran it and it worked!

> myFact 5
120 : Int

I decided to break it by changing the type signature of myIf to

myIf : (b : Bool) -> a -> a -> a

I reloaded the idris repl, and ran myFact 5 again expecting an infinite recursion. To my surprise, it still worked the same way!

Can idris figure out when it should avoid strictness? Why didn't this recurse forever?

I'm using Idris 0.9.15 and none of the release notes between now and the linked notes, mention any changes.

Answer 1

The explanation is here: http://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on

Compile time and run time evaluation semantics are different (necessarily so, since at compile time the type checker needs to evaluate expressions in the presence of unknown values), and the REPL is using the compile time notion, both for convenience and because it's useful to see how expressions reduce in the type checker.

However, there's a bit more going on here. Idris has spotted that myIf is a very small function and has decided to inline it. So when compiled myFact actually has a definition that looks a bit like:

myFact x = case x == 1 of
                True => 1
                False => x * myFact (x - 1)

So generally you can write control structures like myIf without worrying about making things Lazy, because Idris will compile them into the control structure you wanted anyway. Same goes for, e.g. && and || and short circuiting.