Brittle short-circuiting of OR `||`. AND `&&` always works.

[DanGooding]

Hello, I'm enjoying using Koka, but have come across a slightly bizarre bug.

In the following example, the expression ( resume(True) || resume(False) ) : bool does not short-circuit, whereas the similar expressions (resume(True) : bool) || resume(False) and resume(True) || False || resume(False) do short-circuit.

When using AND instead (and swapping True/False) as in resume(False) && resume(True) the expression does short-circuit! (only evaluating the first resume). Could this somehow be to do with the overloading of ||? (whereas && is not overloaded)?

Here's a full example:

effect choose {
  ctl flip() : bool
}

fun mystery() : <choose, console> bool {
  val b = flip()
  println("b = " ++ b.show)
  b
}

// is `mystery` ever true?
fun satisfiable-no-short-circuit() : <console> bool {
  with ctl flip()
    // for each input flip(), try both values
    ( ( resume(True) || resume(False) ) : bool )
  mystery()
}

fun satisfiable-short-circuit() : <console> bool {
  with ctl flip()
    ( resume(True) : bool ) || resume(False)
  mystery()
}

fun main() {
  satisfiable-no-short-circuit().println
  satisfiable-short-circuit().println
}

This example has the following output:

b = True
b = False
True
b = True
True

both satisfiable-no-short-circuit() and satisfiable-short-circuit() return True, but the former evaluates both calls to resume, whist the latter only evaluates the first (resume(True)).

This issue occurs for me in Koka version 2.4.0 (I haven't tried it in other versions).

---

For completeness, here are a few more working and non-working cases I found:

No short-circuit:

• False || resume(True) || resume(False)
• fun k(b) { resume(b) }; ( (k(True) || k(False)) : bool )

Short-circuit:

• (resume(True) : bool) || resume(False)
• resume(True) || (resume(False) : bool)
• resume(True) || False || resume(False)
• resume(True) || resume(False) || False
• (False || resume(True)) || resume(False)
• resume(True) || (False || resume(False))
• fun k(b) : <console> bool { resume(b) }; ( k(True) || k(False) )

[daanx]

Ha, very strange -- I am looking into it soon.

[daanx]

Thanks for the report! I found the bug and it is fixed in the latest dev branch. The example program was very helpful.

[DanGooding]

Thats great, thanks for the quick response!