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.