Safely using effect handler resources?

[osa1]

Suppose I have a simple file system effect:

effect file-system
  ctl open-file(path: string) : handle
  ctl read-file(handle: handle) : string

To be able to use this safely (i.e. without bugs) I need to make sure a handle obtained from a file-system handler needs to be used with the same handler.

(To keep things simple let's assume that all file system handler use the same handle type, maybe an integer.)

For example, if I have an in-memory file system implementation of this effect, and do open-file with a handler and use read-file with another handler, I'll get an error or read a wrong file.

This problem is not specific to Koka, and I'm not seeing anyone trying to tackle this problem (or maybe they don't publish about it?). I'm wondering if you considered this issue at all?

The higher ranked types trick (used in Haskell's ST and managed) is one way but it's also quite limiting: the entire effectful code needs to be lexically enclosed with the effect handler, so e.g. you can't store the handle in a map and use it elsewhere.

This could be solved at the user level by adding a unique handler id to handle and check that the handle's id matches the handler's id in read-file. Maybe a combination of this (when the values escape) and the higher-ranked types trick (when the values don't escape) is good enough? I'm wondering if you've experimented with this kind of thing at all and what your experience was.

[TimWhiting]

Two things to look at: named effects + scoped effects

https://github.com/koka-lang/koka/blob/dev/samples/handlers/named/file-scoped.kk
This shows you how to use named effects + scope types via rank-2 polymorphism. This solves both safety issues you mention, but likely runs into issues with storing them in lists, because they will unify with fresh scope types.

https://github.com/koka-lang/koka/blob/dev/samples/handlers/named/heap.kk
This shows you how to create a resource (mutable state in this case), using first-class named effects + scoped effects. In this case the scoped effect's operation returns a new named effect such that all of the named effects are born under the same scope type, and cannot escape the shared scope where they were born. This solves both the safety issues and the usability issues you mention.

A paper discussing this is: https://www.microsoft.com/en-us/research/publication/first-class-named-effect-handlers/