Algebraic Effect Handlers with Resources and Deep Finalization

Algebraic effect handlers are a powerful abstraction mechanism that can express many complex control-flow mechanisms. In this article we first define a basic operational semantics and type system for algebraic effect handlers, and then build on that to formalize various optimizations and extensions. In particular, we show how to optimize tail-resumptive operations using skip frames, formalize a semantics and type rules for first-class resource handlers that can express polymorphic references, and formalize a design for finalizers and initializers to handle external resources with linearity constraints. We introduce the concept of deep finalization which ensures finalization is robust across operation handlers even if operations themselves do not resume.