Resource Finalization for Effect Handlers
Handling resources, such as files or network sockets, in a language with control (such as exceptions) safely can become difficult. We need to make sure that all memory is eventually freed and all file handles and sockets are closed; even in the case of an exception.
Finally Clauses
In the following example,
val fh = open("my-file.txt");
prog(fh);
fh.close();
how can we make sure that the file will always be closed, even if prog throws an exception?
To address this issue, many languages (like Java, JavaScript, Ruby, etc.) have added a finally-clause to their exception handling mechanism.
val fh = open("my-file.txt");
try { prog(fh) }
finally { fh.close() }
Complex Control-Flow Mechanisms
The Effekt language not only supports exceptions, but also the more general form of “effect handlers”. In particular, a handler might resume the computation at the point where an exception / effect has been raised. In presence of such a feature it is necessary to make sure that the file is reopened, when resuming the computation. To this end, Leijen (2018) has introduced initializers to Koka. In a similar spirit, scheme supports performing operations on unwinding/rewinding (called dynamic-wind).
Goal of the Thesis
The goal of this thesis is to design, implement, and evaluate a language feature for resource initialization/finalization that integrates well into the Effekt language.
Additional Material
- Research project: Effekt
- Documentation: Dynamic Wind in Scheme
- Documentation: Control Operators in Scheme
- Paper: “Algebraic Effect Handlers with Resources and Deep Finalization” (Leijen 2018)
- Paper: “All about that Stack” (Schuster et al., 2021)
- Paper: “Region-based Resource Management in CPS” (Schuster et al., 2022)