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");

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


Jonathan Brachthäuser