Encapsulating Effects in Frank

Plotkin and Pretnar’s effect handlers offer a versatile abstraction for modular programming with user-defined effects. Alas, many implementations are not as modular as they may at first seem. Naive composition of a pair of effect handlers, one a producer, and the other a consumer of an intermediate effect, leads to effect pollution: the intermediate effect leaks and external instances are accidentally captured. We extend the Frank programming language with adaptors, which provide general remapping, and in particular hiding, of effect names in order to support effect encapsulation. Frank is a strict bidirectionally typed effect handler oriented programming language with a parsimonious effect type system in which effect polymorphism is almost always invisible. As a case study, we compose a concurrent actor handler from a collection of more primitive effect handlers using Frank. The naive implementation without adaptors yields an actor handler that suffers from effect pollution. Using adaptors we define an unpolluted actor handler whose type is also five times shorter than that of the naive version. As well as formalising adaptors, we also extend the formalism with other features necessary for the case study including polymorphic commands and a built-in top-level reference effect. We give a type system and an operational semantics and prove type soundness.