Understanding raw ctl

[JanBeh]

Hi all!

I would like to learn more about raw ctl in Koka.

When I implemented effects in Lua, I had to solve the problem when to run finalizers of an interrupted (to be resumed) action. Sometimes, my handler function would return, but the resumption would be stored somewhere to be invoked later.

For this, I added a method :persistent() in my Lua implementation, which (I believe) somehow resembles raw ctl in Koka. Such a resumption would have to be manually released with :discontinue() in my implementation, if it wasn't resumed. I had to do this because it is not forseeable when Lua's garbage collection runs, and finalizers should run in a predictable manner (and not in the context of the Lua garbage collector).

The API for my Lua implementation can be found here:

• resume:persistent() disables automatic discontinuation when the effect handler returns. The method returns resume for convenience.
• resume:discontinue() closes all to-be-closed variables of the action, i.e. runs finalizers. This is implemented by throwing a special error object within the action and catching it.

Now what surprises me is that Koka requires an argument to rcontext.finalize. What's the purpose of that argument? I made some test:

pub effect dummy
  ctl dummy() : ()

pub fun handle-dummy(action : () -> <dummy,console|e> int ) : <console|e> int
  with handler
    raw ctl dummy()
      println("A: " ++ rcontext.finalize(1).show())
      println("B: " ++ rcontext.finalize(2).show())
      3
  action() + 10

pub fun main()
  val result : int = handle-dummy
    dummy()
    0
  println("Result: " ++ result.show())

Output:

A: 1
B: 2
Result: 3

Some questions:

• What happens if I don't finalize?
• And why can I finalize multiple times?
• Also, I wonder if Koka shouldn't be able to release the context right in time due to Perceus reference counting? Why would I need to manually finalize in Koka? (Or why would Koka need to finalize the resumption when a non-raw handler exits, and not when the resume handle gets free'd?)
• What purpose has the argument and return value of rcontext.finalize (it needs to fit the action's return type, yet doesn't seem to be used other than being returned by rcontext.finalize)?

Regarding documentation of raw ctl, I have seen samples/handlers/unix.kk, but I find the example a bit difficult to comprehend, and it also doesn't contain rcontext.finalize.

Also possibly related:

• Resumptions can escape without using raw ctl #649

I also just found:

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

[TimWhiting]

What happens if I don't finalize?

Finalizers don't get run unless you resume or finalize. Finalization is for when you never resume a strand of raw-control that has gotten resources. This is different than garbage collection. The reference counting will drop all heap resources, but if you got OS resources or other external interactions that need cleanup, this is where finalization is important.

See this paper for more in-depth information: https://www.microsoft.com/en-us/research/publication/algebraic-effect-handlers-resources-deep-finalization/.

And why can I finalize multiple times?

Because that is hard to restrict from the type system perspective. Essentially you need linear types (which do exist to some degree in Koka via fip, but fip analysis is pretty limited -> no reasoning about mutation / state which often are necessary with raw ctl. Ideally however in my opinion we should replace the finalizer after it has run with a stub that terminates the program with an error to catch logical bugs.

Also, I wonder if Koka shouldn't be able to release the context right in time due to Perceus reference counting? Why would I need to manually finalize in Koka? (Or why would Koka need to finalize the resumption when a non-raw handler exits, and not when the resume handle gets free'd?)

Good question. Not 100% sure on this, but definitely something to look into. I believe the work on raw control predates the work on Perceus though, so maybe it just hasn't been revisited since then.

What purpose has the argument and return value of rcontext.finalize (it needs to fit the action's return type, yet doesn't seem to be used other than being returned by rcontext.finalize)?

The underlying data structure is also used for finalizing final ctl handlers, which don't resume and need to propagate a value (e.g. an exception) to the handler. This value needs to be threaded through the finalizers for other handlers / finalizers that are between the throw and the exception handling. I'm not sure the point of having it in rcontext.finalize or if there is something special needed there. I assume the types make it return the same thing as the handler overall returns, which makes some amount of sense I think. I haven't looked to closely at it though.

Regarding documentation of raw ctl, I have seen samples/handlers/unix.kk, but I find the example a bit difficult to comprehend, and it also doesn't contain rcontext.finalize.

Sorry, I'm not aware of any good examples at this point. Most examples I know of try to keep an invariant that all captured continuations are run via rcontext.resume, and thus are finalized implicitly after the resumption finishes. I don't know of any examples that preemptively finalize. When we reintegrate async we will likely want to take a closer look.

[TimWhiting]

The problem here isn't finalization as indicated by the output. Instead it is likely crashing due to stack overflow, which is a known issue. I'm curious about the memory usage though.

For jump I would just use final ctl instead of raw ctl since you aren't intending to resume ever there. You can still call the stored resumption captured from the other operation.

[JanBeh]

Instead it is likely crashing due to stack overflow, which is a known issue.

I assume a missing tail call optimization?

I'm curious about the memory usage though.

I can see in top how the process quickly accumulates memory. The core dump then has a size of 716 MiB.

For jump I would just use final ctl instead of raw ctl since you aren't intending to resume ever there.

Ah, good reminder. I have read about final ctl somewhere in the examples. Yeah, that solves the issue with the argument to finalize there. (Though I feel like it should also work without final ctl using rcontext.finalize and without a default value.)

Any idea about the compiler error when I uncomment the with finally block?

I think a good (and not too complicated) example that shows how to use rcontext.finalize could be an implementation of coroutines using effects. I didn't succeed with an implementation in Koka, but I have created a demonstration of how to implement of coroutines using effects with my Lua library (that implements effects using coroutines, i.e. the other way around). There you can see also the "finalization" of the resumption, and that it doesn't need any argument. I'm not sure if that example applies to Koka well, as Lua is untyped. But perhaps it would be possible to create a similar example for Koka, which might explain better how raw ctl is used.

[TimWhiting]

I assume a missing tail call optimization?

Note here:

koka/lib/std/core/hnd.kk

Line 410 in 0554632

clause(resume) // TODO: we should exit prompt first, and then execute clause to use constant stack space when resuming

I can see in top how the process quickly accumulates memory. The core dump then has a size of 716 MiB.

I'll have to try it myself and analyze what is in the dump.

Though I feel like it should also work without final ctl using rcontext.finalize and without a default value.

I'd have to think about this some more.

As far as your example, this fixes the type error, but...

  with finally
   match target
     Nothing -> ()
     Just(c) -> 
      c.finalize(default) 
      () // Finally requires unit to be returned in all branches
      // Since finalization returns the value you pass it, 
      // and it needs to be the right type to be returned from the handler
      // you need to add an extra `()`
   ()

For this example you do not need to finalize in the first place. Finalization is only important if you never resume. However, you are resuming mark immediately, which means you don't need to worry about finalization. If you resume once, or more than once, the resume call takes care of running any finalizers when returning. In fact you never should be calling finalize if you have resumed. We should store a flag in the rcontext, and exit the program with an error if that happens.

For example this is what I think the behavior should be and what you want.

pub fun handle-jump(action : () -> <jump,exn,div,console|e> a) : <console,exn,div|e> a
  var target := Nothing
  with handler
    raw ctl mark()
      target := Just(rcontext)
      rcontext.resume(())
    final ctl jump() 
      match target
        Nothing -> throw("no target")
        Just(c) -> c.resume(())
  with finally 
    println("finalizing")
  action()

For fibers, you'd capture a rcontext from a yield and not resume it immediately, which means that if you haven't run the fiber yet, and want to cancel it, you should finalize it since it hasn't been resumed yet.

[JanBeh]

Thank you for your detailed explanations. I think I understand better now. (I don't understand the TODO in hnd.kk yet, but I would like to take a closer look at that module soon.)

Regarding what I wrote here:

I think a good (and not too complicated) example that shows how to use rcontext.finalize could be an implementation of coroutines using effects. […] perhaps it would be possible to create a similar example for Koka, which might explain better how raw ctl is used.

I was able to create such an example that shows where a (second) argument to finalize may be problematic.

Consider the following (hopefully correct) implementation of asymmetric coroutines:

pub effect yield<y>
  ctl yield( yield-val : y ) : ()

pub type coro-state<h,e,y>
  New ( action : () -> <st<h>,exn,div,yield<y>|e> y )
  Running
  Suspended ( rcontext : resume-context<(), <st<h>,exn,div|e>, <st<h>,exn,div,yield<y>|e>, y> )
  Dead

pub alias coroutine<h,e,y> = ref<h,coro-state<h,e,y>>

pub fun coroutine( action : () -> <st<h>,exn,div,yield<y>|e> y ) : <st<h>> coroutine<h,e,y>
  ref(New(action))

pub fun resume( coro : coroutine<h,e,y> ) : <st<h>,exn,div|e> y
  match !coro
    New(action) ->
      with handler
        raw ctl yield( yield-val )
          coro := Suspended(rcontext)
          yield-val
      with finally
        coro := Dead
      coro := Running
      action()
    Running -> throw("attemt to resume running coroutine")
    Suspended(rcontext) ->
      coro := Running
      rcontext.resume(())
    Dead -> throw("attempt to resume dead coroutine")

pub fun close( coro : coroutine<h,e,y>, ?default : y ) : <st<h>,exn,div|e> ()
  match !coro
    New(_) -> coro := Dead
    Running -> throw("attempt to close running coroutine")
    Suspended(rcontext) ->
      coro := Dead
      rcontext.finalize(default)  // having to provide a value here makes no sense
      ()
    Dead -> ()

pub fun main()
  val c = coroutine
    with finally
      println("...and good bye!")
    yield(1)
    println("Hello")
    yield(2)
    3
  with finally
    c.close( ?default = 0 )  // note that 0 is never used!
  println(c.resume().show())
  println(c.resume().show())
  //println(c.resume().show())
  //println(c.resume().show())

The output, using Koka version 3.2.2 (39b4bec), is:

1
Hello
2
...and good bye!

Note that the function close as defined above needs to provide a (seemingly useless?) value of type y to rcontext.finalize. This means we cannot implement a polymorphic implementation of coroutines for any yielded type y unless we provide some sort of default function for that type y.

I believe rcontext.finalize should not have any extra argument, but perhaps I don't fully understand the implications.

After the question is resolved, maybe the example above (or a similar, perhaps more idiomatic one) could be added to the examples.

[TimWhiting]

#783
This PR makes some changes to allow for finalize without a parameter. The type system forces us to make a cast here, but I think it makes sense, and is an acceptable place for a cast. It likely won't be high priority, and will require some discussion with Daan, but you can build the PR yourself if you would like to experiment further with your example.