12

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.

mjgpy3
  • 8,597
  • 5
  • 30
  • 51
  • My REPL does the same thing. However, I appear to get an infinite loop if I call `myFact` with `:x` in the REPL, or compile to an executable. – C. Quilley Oct 02 '15 at 15:06
  • Possible duplicate of [Idris eager evaluation](http://stackoverflow.com/questions/23149532/idris-eager-evaluation) – Cactus Oct 06 '15 at 07:49

1 Answers1

19

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.

Edwin Brady
  • 4,546
  • 1
  • 22
  • 14
  • 1
    Is this inline optimization correct when it is changing the semantics? – luochen1990 Apr 24 '17 at 14:13
  • It's not changing the semantics. You get the same answer for all inputs whichever way you do it. – Edwin Brady Apr 24 '17 at 14:36
  • But it changes the totality, which is hard to understand, especially when the user switch to some similar coding style (e.g. some changes which makes the code no longer small enough to be inlined) , expecting not change the programs behavior, but the programs may no longer work again .. – luochen1990 Apr 24 '17 at 14:45
  • It doesn't change the totality... EDIT: Ah, of course you mean that it changes the termination of this specific expression, so I should elaborate a bit: Idris will think, whatever it does to optimise, that "myFact" is not total. And, in any case, since it's not total, it's not going to evaluate it when type checking. There is a reasonable argument that it should only do this inlining when the definition is total. – Edwin Brady Apr 25 '17 at 08:48