Is Idris "strictly evaluated"?

Question

Based on Haskell, I read the story of Idris regarding laziness (laxity). I looked through the latest release notes and found code similar to the following

myIf : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a myIf True te = t myIf False te = 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 and it worked!

 > myFact 5 120 : Int 

I decided to break it by changing the signature like myIf to

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

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

Can idris find out when strictness should be avoided? Why is this not repeated forever?

I use Idris 0.9.15 and not one of the release notes between them and the related notes mentions any changes.

Answer 1

Explanation 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

The semantics of estimating compilation time and runtime are different (this is necessary, since the compiler must evaluate expressions in the presence of unknown values ​​during compilation), and REPL uses the concept of compilation time both for convenience and because it is useful to see how expressions decrease during validation types.

However, there is a bit more. Idris noticed that myIf is a very small function and decided to embed it. Therefore, when the compiled myFact really has a definition that looks something like this:

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

That way, you can write control structures like myIf without worrying about creating Lazy things, because Idris will compile them into the control structure you want anyway. The same goes for example. && and || and short circuit.