Effect encapsulation + parametricity

[pchiusano]

Some old notes from talking with Jonathan Brachthäuser at ICFP 2018.

He pointed out that if you have a HOF that takes an effectful fn, f, as arg which is parametric in its effect, and then you have a handle block which handles some concrete effect (say Abort) and also calls f, then if f happens to use that concrete effect, it gets handled by nearest lexically scoped handler with a matching head. Which I would say is unsound.

Jonathan was doing work on a solution where abilities are represented with regular fn parameters, and a handle block introduces those parameters. As the abilities are now ordinary values, they can be used to uniquely identify the handler when unwinding the stack. My initial reaction was this seems ugly for the programmer but I wonder if it could just be a runtime technique.

Some references that he was kind enough to send:

• This paper by Sam Lindley, one of the Frank authors. See page 114.
• And this one by Biernacki et al: https://dl.acm.org/citation.cfm?doid=3177123.3158096
• Koka's solution is described here, see section 6 - https://www.microsoft.com/en-us/research/uploads/prod/2018/04/resource-v1.pdf

My other half-baked thought was you could avoid the problem via the following restriction: when typechecking handle body, remove all ambient abilities from environment that don’t have a concrete head. This is probably too restrictive but it avoids the unsoundness.