Inhaltszusammenfassung:
Der ständig steigende Bedarf an Software in immer unterschiedlicheren Bereichen führt zu einer immer größeren Komplexität der Programme. Um die Größe und Komplexität von Software zu skalieren, setzen Programmierer die Programme aus einzelnen, wiederverwendbaren Teilen zusammen. Diese Teile werden als allgemein nützlich erkannt und als Software-Bibliotheken geteilt. Um diese gemeinsame Nutzung und Wiederverwendung zu ermöglichen, müssen Programmiersprachen Möglichkeiten bieten, über Code-Muster zu abstrahieren und diese später wieder zu konkretisieren. Außerdem wird es mit zunehmendem Umfang der Software immer wichtiger, dass die Programmierer in der Lage sind, sich von der Korrektheit eines Teils des Programms zu überzeugen, ohne sich alle anderen Teile anzuschauen.
Effekte sind eine Klasse von Sprachkonstrukten, die Programme auf nicht-triviale Weise mit ihrem Kontext interagieren lässt. Beispiele sind der Zugriff auf das Dateisystem, veränderliche Referenzen, Ausnahmen, Generatoren und mehr. Die meisten Sprachen enthalten eine Auswahl dieser Konstrukte in unterschiedlichen Variationen, was für ihre Nützlichkeit spricht. Es besteht jedoch weitgehend Einigkeit darüber, dass undisziplinierte Verwendung von Effekten zu Programmen führt, die schwer korrekt zu erstellen, schwer zu verstehen und schwer zu pflegen sind. Des Weiteren muss jedes einzelne dieser Konstrukte in jede einzelne Programmiersprache eingebaut werden, und dabei muss ihre Kombination sorgfältig bedacht werden. Schließlich können Programmierer nicht über diese Konstrukte selbst abstrahieren und sie daher nicht gemeinsam nutzen oder in einer Weise erweitern, die der Implementierer der Programmiersprache nicht vorhergesehen hat.
Effekt-Handler sind ein relativ neues Sprachkonstrukt, das viele bestehende Konstrukte für Effekte ausdrücken kann und sogar über das hinausgeht, was die meisten Programmiersprachen anbieten. Mit Effekt-Handlern können Effekte wie veränderliche Referenzen, Ausnahmen oder Generatoren von Benutzern der Programmiersprache definiert werden. Dies ermöglicht die Abstraktion über wiederholte Muster, die Effekte verwenden. Natürlich können die Programmierer diese Abstraktionen in verschiedenen Kontexten gemeinsam nutzen und wiederverwenden und sogar ihre eigenen Effekte erfinden, was ganz neue Gestaltungsmöglichkeiten eröffnet. Darüber hinaus grenzen Effekt-Handler den Kontext von Effekten ab, was dem Programmierer gewisse Garantien gibt, ohne dass er das gesamte Programm inspizieren muss. Mit anderen Worten, sie erzwingen einen disziplinierten Gebrauch von Effekten.
In dieser Thesis stellen wir eine Kompilierungstechnik für Effekt-Handler vor, welche dabei hilft, dieses Sprachkonstrukt von der Theorie in die Praxis zu bringen. Kompilierte Programme benötigen keine Laufzeitunterstützung, was sie weithin einsetzbar macht. Sie ermöglicht aggressive Optimierungen zur Kompilierzeit, was sie effizient macht. Sie unterstützt Programme, die exotischere Effekte wie Nicht-Determinismus verwenden, was sie allgemein einsetzbar macht. Sie ist auch von theoretischem Interesse, da sie in bekannte und gut untersuchte Programmiersprachen übersetzt. Zusammenfassend: Unsere Kompilierungstechnik ermöglicht neue Arten von Abstraktion ohne Bedauern in Programmen, die Effekt-Handler verwenden.
Abstract:
The ever increasing demand for software in an ever increasing number of different domains leads to an ever increasing complexity of programs. To scale the size and complexity of software, programmers compose programs out of individual, reusable parts. These parts are discovered to be commonly useful and shared as libraries. To enable this sharing and reuse, programming languages must offer a way to abstract over patterns of code and to concretize the pattern to specific use cases. Moreover, as the scale of software increases, it becomes more and more important that programmers are able to ascertain themselves of the correctness of one part of the program without looking at all the other parts.
Effects are a class of language features that makes programs interact with their context in a non-trivial way. Examples are file system access, mutable state, exceptions, generators, and more. Most languages include some of these features in one form or another, which speaks to their usefulness. However, it is widely agreed upon that undisciplined use of effects leads to programs that are hard to get correct, hard to understand, and hard to maintain. Moreover, each of these individual features must be built into a programming language and while doing so their combination must be carefully considered. Finally, programmers cannot abstract over these features and therefore not share them nor extend them in ways unforeseen by the programming language implementor.
Effect handlers are a relatively recent programming language feature that subsumes many existing language features for effects, and even goes beyond what most programming languages offer. With effect handlers, effects like mutable state, exceptions, or generators are user-defined. This allows for abstraction over repeated patterns involving different kinds of effects. Naturally, programmers can share and reuse these abstractions in different contexts and even invent their own effects which opens up a whole new design space. Moreover, effect handlers delimit the extent of effects, which gives programmers certain guarantees without inspecting the entire program. In other words, they enforce a disciplined use of effects.
In this thesis we present a compilation technique for effect handlers, which will help this programming language feature to move from theory to practice. Compiled programs do not need any runtime support, which makes it widely deployable. It enables aggressive compile-time optimizations, which makes it efficient. It supports programs using more exotic effects like non-determinism, which makes it general. It is also of theoretical interest, because it targets well-known and well-studied languages.
In summary, our compilation technique enables new kinds of abstractions without regret for programs using effect handlers.
