Finalizers can be run multiple times even when entering the continuation once

[osa1]

This is probably a documentation issue, but the book section 3.4.11 says this about finally:

The finally function handles these situations, and takes as its first argument a function that is always executed when either returning normally, or when unwinding for a non-resuming operation
...
The current definition is robust for operations that never resume, or operations that resume once – but there is still trouble when resuming more than once. ...

My understanding of this is if I enter a continuation one or zero times, it should work as expected. But actually even with entering it once you can run a finalizer twice:

effect fx1
  ctl op1(): ()

fun test()
  with finally
    println("In finally")
  println("Before op1")
  op1()
  println("After op1")

fun main()
  var cont := Nothing

  val _ =
    with handler
      ctl op1()
        cont := Just(resume)
        ()

    test()

  match cont
    Just(res) ->
      println("Calling continuation")
      res(())
    Nothing -> ()

Output:

Before op1
In finally
Calling continuation
After op1
In finally

Note that "After op1" is printed once (i.e. the continuation is called once), but "In finally" is printed twice.

[TimWhiting]

Since the resumption escapes the handler you should probably use raw ctl instead of ctl. This will fix your issue, though I've added issue #649 to track the fact that we should be more restrictive and require raw ctl for escaping resumptions.

fun main()
  var cont := Nothing

  val _ =
    with handler
      raw ctl op1()
        cont := Just(fn() rcontext.resume(()))
        ()

    test()

  match cont
    Just(res) ->
      println("Calling continuation")
      res()
    Nothing -> ()

Output:

Before op1
Calling continuation
After op1
In finally

The explanation is that when you capture a resumption, there is no guarantee that the finalizers will ever run - if you never call resume. So at a high level the default behavior is to run finalizers after the operation finishes if there is no call to resume. For example, you want to close a file even if there is an exception thrown when working with the file. raw ctl defers the finalization to the point after a call to resume returns.