Inhaltszusammenfassung:
In unserer hochgradig digitalisierten Welt sind Computerprogramme allgegenwärtig.
Es gibt eine Vielzahl von Hochsprachen mit komplexen Sprachmerkmalen, die das strukturierte Schreiben von Code erleichtern.
Letztlich muss dieser Code jedoch auf realer Hardware ausgeführt werden, die weitaus weniger strukturiert ist und komplexe hochsprachliche Merkmale nicht direkt ausdrücken kann.
Ein Programm aus einer Ausgangssprache, in der Programmierer ihre Programme schreiben, in Befehle zu kompilieren, die eine reale Maschine versteht, ist daher eine komplexe Aufgabe.
Ein Compiler sollte nicht nur Maschinencode erzeugen, der das beabsichtigte Verhalten des Programms korrekt umsetzt, sondern der erzeugte Code sollte auch effizient ausgeführt werden.
Diese anspruchsvolle Aufgabe wird durch den Einsatz einer Zwischenrepräsentation im Compiler ermöglicht, die die Lücke zwischen hochsprachlichen Annehmlichkeiten und maschinennahen Anforderungen überbrückt.
Moderne funktionale Programmiersprachen zeichnen sich oft durch ein besonders hohes Abstraktionsniveau aus.
Dies ermöglicht es Programmierern zwar häufig Programme auf eine prägnante und elegante Weise auszudrücken, macht jedoch zugleich die Kompilierung solcher Sprachen besonders herausfordernd.
Erschwerend kommt hinzu, dass moderne Programme oft kontinuierlich mit externen Komponenten interagieren, was asynchron erfolgen muss, um die Ausführung nicht zu blockieren, während auf das Ergebnis der externen Komponente gewartet wird.
Asynchrone Kommunikation erfordert die Fähigkeit, nicht-lokale Kontrollflüsse auszudrücken.
Compiler gehen damit typischerweise auf zwei Arten um: Entweder sie fügen dem Laufzeitsystem Unterstützung für eine Art von Kontrolloperator hinzu, oder sie wenden eine Übersetzung an, die nicht-lokale Kontrolleffekte durch andere Konstrukte ausdrückt, die in der Zwischenrepräsentation des Compilers bereits vorhanden sind.
Eine Möglichkeit, nicht-lokalen Kontrollfluss auszudrücken, ist die Verwendung einer Zwischenrepräsentation mit expliziten Konsumenten (consumers).
Ein gut untersuchtes Beispiel hierfür sind Zwischenrepräsentationen im Continuation-Passing Style (CPS).
Im Continuation-Passing Style ist die Continuation, d.h. der Rest der Berechnung, explizit als Term in der Sprache vorhanden.
Sprachen im Continuation-Passing Style sind seit langem als Option für Zwischenrepräsentationen in Compilern etabliert.
Eine andere, bisher deutlich weniger beachtete Möglichkeit sind Sprachen, die auf dem Sequenzenkalkül basieren.
Der Sequenzenkalkül ist das Gegenstück zum natürlichen Schließen, bekannt aus der Logik.
Während das natürliche Schließen durch seine Entsprechung mit dem Lambda-Kalkül via des Curry-Howard-Isomorphismus seit langem als Grundlage funktionaler Programmiersprachen dient, wurde erst vergleichsweise kürzlich ein zufriedenstellendes Termzuweisungssystem für den klassischen Sequenzenkalkül gefunden.
Im Gegensatz zum natürlichen Schließen und dem Lambda-Kalkül, die auf Beweise, welche zu Produzenten (producers) korrespondieren, ausgerichtet sind, behandeln der klassische Sequenzenkalkül und darauf basierende Sprachen Beweise und Widerlegungen, welche zu Konsumenten korrespondieren, auf symmetrische Weise.
Dies macht solche Sprachen zu einer interessanten Alternative zum Continuation-Passing Style für Zwischenrepräsentationen.
In dieser Dissertation untersuchen wir zwei verschiedene Möglichkeiten, wie explizite Konsumenten bei der Kompilierung funktionaler Programmiersprachen eingesetzt werden können.
Zunächst betrachten wir Zwischenrepräsentationen im Continuation-Passing Style sowie Übersetzungen in diese.
Eine naheliegende Frage in diesem Zusammenhang ist, ob es möglich ist, Programme aus dem Continuation-Passing Style wieder zurück in den Direktstil (direct style) zu übersetzen, in dem Programme üblicherweise geschrieben werden.
Dies ist nicht nur theoretisch von Interesse, sondern hat auch praktische Relevanz.
Zwar bringt der Continuation-Passing Style viele Vorteile für Zwischenrepräsentationen mit sich, jedoch auch einige Nachteile im Vergleich zum Direktstil.
Insbesondere stellen viele Plattformen einen Aufrufstapel (call stack) bereit, der von Programmen im Continuation-Passing Style nicht genutzt wird.
Eine geeignete Rückübersetzung in den Direktstil könnte es einem Compiler ermöglichen, die Vorteile beider Stile zu nutzen.
Im ersten Teil dieser Arbeit stellen wir daher das Design einer Rückübersetzung in den Direktstil vor, die viele Eigenschaften besitzt, die im Compiler-Kontext wichtig sind, und legen damit die Grundlage für eine praktische Anwendbarkeit einer solchen Übersetzung.
Im zweiten Teil dieser Arbeit gehen wir in die andere Richtung: Wir kompilieren bis hinunter zu Maschinencode.
Dabei verwenden wir jedoch nicht den Continuation-Passing Style, sondern untersuchen Zwischenrepräsentationen auf Basis des klassischen Sequenzenkalküls.
Wir präsentieren eine vollständige Kompilationskette, beginnend mit einer funktionalen Ausgangssprache mit interessanten Eigenschaften, bis hin zur Erzeugung von Maschinencode, der auf einem realen Computer ausgeführt werden kann.
Wir identifizieren eine Normalform unserer sequenzenkalkülbasierten Zwischenrepräsentation, die sich für eine überraschend direkte Möglichkeit der Codegenerierung eignet.
Die symmetrische Struktur von Sprachen, die auf dem klassischen Sequenzenkalkül basieren, macht sie, auch im Hinblick auf Optimierungen, zu einem vielversprechenden Ziel, und unsere Kompilationskette bildet die Grundlage für zukünftige Untersuchungen.
Abstract:
In our highly digitalized world, computer programs are ubiquitous. There is a multitude of
high-level programming languages with complex language features that facilitate writing code in a structured way.
Eventually, however, this code must be executed on real hardware, which is much less structured and
cannot express complex high-level features directly. Compiling a program from a surface language,
used by programmers to write their programs, into instructions a real machine understands hence is a complicated task.
A compiler should not only generate machine code that correctly implements the intended behavior of the
program written in the surface language, but the generated code should also execute efficiently. This complicated
task is made possible by employing a compiler intermediate representation that bridges the gap between
high-level conveniences and low-level concerns.
Modern functional programming languages tend to exhibit a particularly high level of abstraction. While
this often enables programmers to express programs in a concise and elegant way, it also makes the compilation
of such languages particularly challenging. This is exacerbated by the fact that modern programs
often continually interact with external components, which must be done in an asynchronous way to avoid
blocking execution while waiting for the result of the external component.
Asynchronous communication requires the ability to express non-local
control flow. Compilers typically deal with this in one of two ways. Either they add support for some
kind of control operator in the runtime system, or they apply a translation to express non-local
control effects in terms of other constructs present in the compiler intermediate language.
One possibility for expressing non-local control flow is to use an intermediate language that exhibits
explicit consumers. A well-studied example are intermediate representations in continuation-passing style (CPS).
In continuation-passing style, the continuation, i.e., the rest of the computation, is explicitly available
as a term in the language. Languages in continuation-passing style have long been established as an option
for compiler intermediate languages. A different option that has received much
less attention so far are languages based on sequent calculus. Sequent calculus is the sibling calculus of
natural deduction, known from logic. While natural deduction has long been used as a
basis for functional programming languages, through its correspondence with the lambda calculus by the
Curry-Howard isomorphism, it took until relatively recently to find a satisfying term-assignment system
for the classical sequent calculus. In contrast to natural deduction and lambda calculus, which
are biased towards proofs corresponding to producers, classical sequent calculus and languages based on
it treat proofs and refutations, which correspond to consumers, in a symmetric way. This makes
such languages an interesting alternative to continuation-passing style for intermediate representations.
In this thesis, we examine two different ways how explicit consumers can be used in the compilation of
functional programming languages. First, we consider intermediate languages in continuation-passing style
and translations into them. A question that naturally arises in this context is whether it is possible to
translate from continuation-passing style back to direct style in which programs are usually written.
This is not only of theoretical interest, but there is also a practical aspect. While continuation-passing style
has many benefits for intermediate representations, it also comes with downsides compared to direct style.
In particular, many platforms provide a call stack, which programs in continuation-passing style do not make
use of. A suitable translation back to direct style could enable a compiler to reap the benefits of both styles.
In the first part of this thesis, we thus present the design of a translation back to direct style
having many properties that are important in the context of a compiler, laying the groundwork for making
such a translation practically applicable.
In the second part of this thesis, we go in the other direction, compiling down to machine code. However,
instead of using continuation-passing style, we examine intermediate languages based on classical sequent calculus.
We present a complete compilation pipeline, starting from a functional surface language with interesting features,
and ending with the generation of machine code that can be executed on a real computer. We identify a normal form
of our sequent-calculus-based intermediate representation that is suitable for a surprisingly direct way of code
generation. The symmetric structure of languages based on classical sequent calculus makes them a promising target,
also with regard to optimizations, and our pipeline forms the basis for future investigations.
continuation-passing style