What are scoped handlers?

[JanBeh]

I would like to understand better understand the concept of scoped handlers. The manual/book states that combining handlers creates different results based on which handler is written first. Is this related to scoped handlers? The manual section on scoped handlers is still a TODO (with a broken link).

I have found several papers on this topic, but they were quite abstract/mathematical and usually didn't refer to Koka but Eff.

There are examples in scoped.kk but they don't seem to use a particular language feature regarding scoped handlers but just demonstrate the type and runtime differences regarding ordering handlers. Where can I find more information (ideally Koka-related) on scoped handlers? How do they relate to named handlers?

When implementing effect handling in Lua, I ran into problems when creating an effect that waits for I/O in a multi-fiber environment, because the sleeping (link to code) must be performed in the most inner context and not in the context where the effect handler is installed. To solve this, I made it possibe to not pass a value to the continuation but a function that gets evaluated in the context where an effect has been performed (link to code, link to docs). This seemed to be helpful for my implementation. Does something similar exist in Koka, i.e. where you can write something like rcontext.resume_and_evaluate(func) such that func is evaluated in the context where the effect was performed? If not, would it make sense to add such a feature or is it not needed due to other language constructs that exist in Koka?

[TimWhiting]

I believe this would be the recommended paper to read for both scoped effects and named handlers. First-class Names for Effect Handlers.
You obviously don't have to understand the formalism to use them, but section 2 has several examples, section 3 is still pretty understandable, and you can skip to section 7 for more examples.

If you don't have access to the paper via that website you can get the technical report which is very similar here: https://www.microsoft.com/en-us/research/publication/first-class-named-effect-handlers/

Additionally, your mention of passing a function to be called in the context where the effect is being performed I'm pretty sure is a problem addressed by this paper for a different language: Handling Bidirectional Effects - including appropriate typing rules I think. I'm not sure if it is something Daan has thought about or would want to add to Koka, but you could open an issue and link to the paper and propose how it would work in Koka.

[JanBeh]

I believe this would be the recommended paper to read for both scoped effects and named handlers. First-class Names for Effect Handlers.

Thanks for that link, this helped!

Some things are still confusing me and I feel like I'm missing some documentation. For example, I don't see where abstract type is explained in Koka's documentation. I find it in the grammar specification of the book, but no explanation is given there.

Also, do I understand it right that if a named handler escapes its scope (and I don't use scoped effects), weird things will happen at runtime? I tried the following example:

named effect read
  ctl ask() : int

fun read(x, action)
  with h <- named handler
    ctl ask()
      resume(x)
  action(h)

fun main()
  read(17, fn(x) fn() x.ask.println)()
  println("unreachable")

This program terminates with no output at all. Is this intended or a bug? Shouldn't there be a runtime (or compile-time?) error?

I have used Koka 3.1.1, 23:47:21 Apr 9 2024 (ghc release version).

Update: Seems to be a bug, I just found #356.

[JanBeh]

First-class Names for Effect Handlers.

[…], section 3 is still pretty understandable, […]

In section 3, I looked at Figure 4 (scoped read effect). I tried to compile the code, but apparently it needed a few adjustments for today's Koka:

-named scoped effect read<s>
+named scoped effect read<s::S>
-  ask() : int
+  ctl ask() : int
 
-fun read(x : int, action : forall<s> read<s> -> <read<s>|e> a) : e a
+fun read(x : int, action : forall<s> ev<read<s>> -> <read<s>|e> a) : e a
   with h <- named handler
-    ask(){ resume(x) }
+    ctl ask(){ resume(x) }
   action(h)

Adding ctl is clear to me. The ::S seems to be a type annotation indicating that the type parameter s is a "scope" type. I found ev<a> in std/core/hnd. Documentation says: "Effect handler evidence of a handler h in the context." I can't really follow here. Is there an easy explanation of what the ev type is about?

[TimWhiting]

The ev<> is a recent change made by Daan to better type first class named effects. Before the effect type was directly used as a parameter type, which was kind of weird due to the type being used as an effect type and a value type. Now we have ev which represents the first class evidence value for the handler:
More documentation here:

koka/lib/std/core/hnd.kk

Line 54 in 0bb2a23

- Evidence `ev<h :: (E,V)->V >` for a handler `:h` is an existential tuple