No runtime exception for the escape of named but unscoped handlers

[thwfhk]

The Section 5 of the paper First-class names for effect handlers mentions that when a named but unscoped handler is not found at runtime, an exception will be raised. However, this seems to be not reflected in the implementation. Consider the following example:

module reader

named effect read
  ctl read() : string

fun h0(action)
  with h <- named handler
    fun read() "Hi"
  action(h)

fun h1(action)
  with h <- named handler
    ctl read() resume("Hi")
  action(h)

pub fun test0()
  with h <- h0()
  h.read.println

pub fun test0'()
  val h = h0(id)
  h.read.println

pub fun test1()
  with h <- h1()
  h.read.println

pub fun test1'()
  val h = h1(id)
  h.read.println

Both test0' and test1' let the named handler h escape. I get the following output for them using Koka 2.4.2:

> test0'()
check  : interactive
check  : interactive
add default effect for std/core/exn
linking: interactive
created: /var/folders/t1/zb004c5101z0gk4g61njxhdh0000gn/T/.koka/v2.4.2/clang-debug/interactive

Hi

> test1'()
check  : interactive
check  : interactive
add default effect for std/core/exn
linking: interactive
created: /var/folders/t1/zb004c5101z0gk4g61njxhdh0000gn/T/.koka/v2.4.2/clang-debug/interactive

> test0()
check  : interactive
check  : interactive
add default effect for std/core/exn
linking: interactive
created: /var/folders/t1/zb004c5101z0gk4g61njxhdh0000gn/T/.koka/v2.4.2/clang-debug/interactive

Hi

> test1()
check  : interactive
check  : interactive
add default effect for std/core/exn
linking: interactive
created: /var/folders/t1/zb004c5101z0gk4g61njxhdh0000gn/T/.koka/v2.4.2/clang-debug/interactive

Hi

It is also interesting that the two handlers h0 and h1 have different behaviours after escape; h0 still correctly handles the read operation even though there is no surrounding handler (test0'), while h1 outputs nothing (test1').

[TimWhiting]

Yes, I've seen this behavior too. You'll notice that test1' does cause the program to terminate which is technically a sort of exception just without an exceptional status or an exception message. Additionally, since h0 does not require building a resumption due to the fact that it is not a ctl opration and due to the fact that Koka's implementation only builds a resumption / delimited continuation on demand, it works perfectly fine. In fact you can sort of model an object oriented program with just named handlers that have some local state and provides an interface to working with that state with fun clauses.

[thwfhk]

Ah I see! It makes sense that test1' raises an exception without any message, though a little misleading. Yes I understand that it is fine for tail-resumptive handlers like h0 to escape. Thank you!

[TimWhiting]

To be clear, I think it should raise a message, I was just saying that it was technically exceptional behavior.