Invoking non-resuming effect in effect handler skips finalizers

[JanBeh]

In the given program

effect ctl myeffect() : ()

fun main() : <console> ()
    with ctl myeffect()
        ()
    with ctl myeffect()
        myeffect()
    with finally
        println("cleanup")
    myeffect()

the line println("cleanup") apparently isn't executed. I assume this is a bug, but I'm not entirely sure.

Tested with koka version 2.4.2.

If this is intended, is there some documentation on this?

[TimWhiting]

This is the relevant code from hnd.kk

pub fun finally( fin : () -> e (), action : () -> e a ) : e a 
  finally-prompt(fin, action());

fun finally-prompt(fin : () -> e (), res : a ) : e a 
  if !yielding() then 
    fin()
    res
  elif yielding-non-final() then 
    yield-cont(fn(cont,x){ finally-prompt(unsafe-decreasing(fin),cont(x)) })
  else 
    val yld = yield-capture()
    fin()
    if yielding() return yield-extend( fn(_x) unsafe-reyield(yld) )
    unsafe-reyield(yld)

It looks like in the else branch where it deals with the non-resumptive handler clauses, it invokes the finalize function fin() after it captures where it actually needs to yield to. However, in your case there is no handler above that actually resumes, so yield-capture never resumes.

So it looks like there might need to be some handler/prompt to delimit the main function, so that when capturing the yield, it actually captures something.

Rather than creating a separate effect to do so, you can just use finally which will install a delimiting prompt. This works for me:

effect ctl myeffect() : ()

fun main() : <console> ()
  with finally
    ()
  with ctl myeffect()
    resume(())
  with override ctl myeffect()
    myeffect()
  with finally
    println("cleanup")
  myeffect()

[JanBeh]

I still don't understand if the exhibited behavior is intentional or not.

[daanx]

I still don't understand if the exhibited behavior is intentional or not.

The behavior was not, and it is fixed now. The idea is that a finally block should always run (at least once for multiple resumptions) -- even when a handler does not resume. This is of course super important to ensure external resources are always released. The previous implementation was wrong and I think it is right now. I wrote about the semantics in this 2018 tech report, section 8: https://www.microsoft.com/en-us/research/uploads/prod/2018/04/resource-v1.pdf but it is a bit old now; we should do this properly again sometime :-)