Functional DSL Compilers with Leightweight Proofs

An essential component of programming language design, is to walk the trade-off between re-using as much as possible from already existing languages while carefully questioning core design choices to overcome fundamental problems. To investigate compilation techniques for high-level programming languages, we present a series of compilers covering a wide range of language features. This thesis is structured into two parts: (i) compiling and enforcing protocols, and (ii) intermediate representations and optimizations.

We begin the first part, by comparing two emerging trends in programming languages for distributed protocols – choreographic and multitier programming. Choreographic and multitier programming are both global programming models, in the sense that a single program specifies the behavior of all participants in the distributed protocol. To investigate similarities and differences, we present an algorithm to translate a restricted version of choreographic programming to multitier programming, and vice versa. Then, we present our own global language called Prisma, for writing programs that run partially on a smart contract. Besides splitting the source program into a program for the smart contract and a program for its clients, Prisma also enforces the control flow of the contract even in the presence of clients who deviate from the protocol.

In the second part, we investigate intermediate representations and optimizations. In functional compilers, A-normal form is a common intermediate representation, whose design can be derived from the concept of laws of monads. However, monads are usually associated with sequentiality and bringing evaluation into a total order. We present a notation par-seq that compiles to monadic operations to express dependencies between terms, and applicative functor operations to express independent terms. Then, we present the indexed A-normal form (AiNF), an extension of A-normal form for array operations, based on the idea that arrays are dual to functions, and show how it can create optimization opportunities in combination with partial evaluation and common subexpression elimination. Finally, we present the density compiler repot. It takes a probabilistic program as input and then searches for a program to compute the corresponding probability density function to output. A key part of this search is the use of conditional A-normal form (canf) to perform program inversion.

Ein wesentlicher Bestandteil des Entwurfs von Programmiersprachen besteht darin, eine Balance zwischen der Wiederverwendung möglichst vieler Teile auf der einen Seite und der sorgfältigen Hinterfragung zentraler Konzepte auf der anderen Seite zu finden. Um Kompilierungstechnik zu untersuchen, stellen wir eine Reihe von Compilern vor, die ein breites Spektrum von Sprachmerkmalen abdecken. Diese Arbeit ist in zwei Teile gegliedert: (i) Kompilierung und Durchsetzung von Protokollen, und (ii) Zwischendarstellungen und Optimierungen.

Wir beginnen den ersten Teil mit einem Vergleich von zwei Trends bei Programmiersprachen für verteilte Protokolle -- choreographische und multitier Programmierung. Sowohl die choreografische als auch die multitier Programmierung sind globale Modelle -- in dem Sinne, dass ein einziges Programm das Verhalten aller Teilnehmer eines verteilten Protokolls beschreibt. Um die Gemeinsamkeiten und Unterschiede zu untersuchen, stellen wir einen Algorithmus vor, der eine eingeschränkte Version der choreografischen in die multitier Programmierung übersetzt und umgekehrt. Dann stellen wir eine neue globale Sprache namens Prisma vor, deren Programme teilweise auf einem Smart Contract laufen. Der Prisma Compiler teilt ein Programm nicht nur in eines für den Smart Contract und eines für seine Clients auf, sondern stellt auch den Kontrollfluss des Contracts sicher, selbst in Gegenwart von Clients, die vom Protokoll abweichen.

Im zweiten Teil untersuchen wir Zwischendarstellungen und Optimierungen. In funktionalen Compilern ist die A-Normalform eine gängige Zwischendarstellung, deren Design sich aus dem Konzept der Monadengesetze ableiten lässt. Monaden sind jedoch in der Regel mit Sequentialität verbunden und bringen die Auswertung in eine Gesamtordnung. Wir stellen eine Notation par-seq vor, die zu monadischen Operationen kompiliert wird, um Abhängigkeiten zwischen Termen auszudrücken, und zu applikativen Funktoroperationen, um die Unabhängigkeit von Termen auszudrücken. Anschließend stellen wir die indizierte A-Normalform (AiNF) vor, eine Erweiterung der A-Normalform für Array-Operationen, die auf der Idee beruht, dass Arrays dual zu Funktionen sind, und zeigen, wie sie in Kombination mit Partial-Evaluation und Common-Subexpression-Elimination Potenzial für Optimierungen schafft. Schließlich stellen wir repot vor, einen Compiler für Wahrscheinlichkeitsdichten. Er nimmt ein probabilistisches Programm als Eingabe und sucht dann nach einem Programm, das die entsprechende Wahrscheinlichkeitsdichtefunktion für die Ausgabe berechnet. Ein wichtiger Bestandteil dieser Suche ist die Verwendung der bedingten A-Normalform (CANF) zur Durchführung von Programminversion.