Programming with Symmetric Data and Codata Types

Abstract

Statisch getypte funktionale Programmiersprachen sind auf zwei grundlegenden Theorien aufgebaut: Auf dem Lambdakalkül und auf der Theorie algebraischer Datentypen. Wir erkennen diese beiden Theorien in der Kerngrammatik von Lambdaabstraktionen, Funktionsanwendungen, Konstruktoren und Pattern-Matching die allen funktionalen Programmiersprachen gemeinsam ist. Funktionale Programmierer begegnen dem Versuch diese Kerngrammatik mit anderen Konstrukten wie Schnittstellen aus der objektorientierten oder Ausnahmen aus der imperativen Programmierung zu erweitern häufig mit Skepsis. Dies ist der Fall da diesen Konzepten die enge Verbindung zur Logik und Mathematik zu fehlen scheint welche dem Lambdakalkül und algebraischen Datentypen vermittels des Curry-Howard Isomorphismus zueigen ist. Fortschritte in der Logik und Beweistheorie fordern jedoch dazu heraus diese Skepsis zu überdenken. Die Analyse von logischen Konnektiven in Begriffen der Polarität erlaubt es objektorientierten Schnittstellen eine logische Interpretation als Kodatentypen zu geben, und das verbesserte Verständnis der klassischen Logik zeigt dass Kontrolloperatoren welche zur Implementierung von Ausnahmebehandlung verwendet werden Prinzipien der klassischen Logik entsprechen.

Diese Dissertation zeigt dass funktionale Programmiersprachen symmetrischer und funktionaler gemacht werden können wenn diesen Fortschritten Rechnung getragen wird. Anstatt auf dem Lambdakalkül und algebraischen Datentypen aufzubauen beginnen wir mit der Theorie von algebraischen Daten- und Kodatentypen, welche den Lambdakalkül als Spezialfall einschließen. Anstatt diese zwei komplementären Sprachfragmente unabhängig voneinander zu entwerfen verwenden wir auf systematische Weise die Programmtransformationen Defunktionalisierung und Refunktionalisierung als Methodologie um die Eigenschaften beider Fragmente herzuleiten. In vollständig symmetrischen Sprachen kann Defunktionalisierung jeden Kodatentyp in einen Datentypen transformieren, und Refunktionalisierung jeden Datentyp in einen Kodatentypen. Da wir auch von der Ausdrucksstärke von Kontrolloperatoren Gebrauch machen wollen wechseln wir im zweiten Teil dieser Dissertation zu einem Termzuweisungssystem für den Sequenzenkalkül, nachdem wir im ersten Teil ein Termzuweisungssystem für das System des natürlichen Schließens verwendet haben. Wir zeigen warum der Sequenzenkalkül ein besseres System als das natürliche Schließen ist um symmetrische Programmiersprachen zu entwickeln, welche eine Behandlung von Kontrolleffekten und Ausnahmen als Konstrukte erster Klasse erfordern. Im Laufe der Zeit entwickeln sich die meisten Programmiersprachen zu einer Anhäufung unzusammenhängender Funktionalitäten; indem wir das Prinzip der Dualität anwenden können wir die Uhr ein Stück weit zurückdrehen und zumindest einige dieser angehäuften Features in ein von Symmetrie geprägtes kohärentes System bringen.