Eine besondere Stärke von funktionaler Programmierung ist die Möglichkeit, mittels „Equational Reasoning“ Programme zu analysieren und zu transformieren. So gilt beispielsweise in Haskell die Gleichung „map id = id“ und der Programmierer, aber auch der Compiler, kann nun überall im Programm ein map id durch id ersetzen.

Der Haskell-Compiler GHC erlaubt es dem Programmierer mittels Rewrite-Rules solche Gleichungen anzugeben, die der Compiler dann während der Optimierungsphase entsprechend ersetzt. Damit ist beispielsweise die List-Fusion implementiert, mit der unnötige Zwischenlisten wegoptimiert werden. Allerdings müssen hier die Regeln erst vom Programmierer von Hand geschrieben werden.

In dieser Master- oder Diplomarbeit soll eine Programmanalyse entworfen und implementiert werden, die solche Gleichungen automatisch findet. Konkret sollen für Funktion vom Typ f :: ... -> T a -> T b, wobei T ein Typkonstruktor wie Maybe ist, Gleichungen der Form f ... = id hergeleitet werden. Zwar ist es unwahrscheinlich, dass der Programmierer selbst ein map id in den Programmcode geschrieben hat, aber vorhergehende Optimiserungsschritte können solchen Code entstehen lassen.

Aufgabe:

Sie entwerfen einen Algorithmus der, gegeben eine Funktionsdefinition in einer Modellsprache, also einem einfach typisierten Lambda-Kalkül mit rekursiven Datentypen, hinreichende Bedingungen an die Argumente der Funktion findet, so dass sie zur Identität wird, also das letzte Argument unverändert zurückgibt. Gleichungen, die dabei gefunden werden sollten, sind beispielsweise map id = id, maybe Nothing Just = id und (.) id = id.

Sie beweisen bezüglich einer geeigneten Semantik die Korrektheit ihrer Analyse: Wenn eine Gleichung gefunden wird, dann stimmt sie auch.

Letzendlich implementieren Sie ihre Analyse als GHC-Plugin, das alle Funktionsdefinitionen eines Moduls analysiert und die gefundenen Regeln dem Modul hinzufügt. Dazu lernen Sie, mit der GHC-Zwischensprache Core umzugehen. Sie veröffentlichen den fertigen Code unter einer freien Softwarelizenz auf http://hackage.haskell.org/.

Voraussetzungen

Ein Grundverständnis von funktionaler Programmierung, wie es in der Vorlesung „Programmierparadigmen“ vermittelt wird oder duch interessiertes Selbstudium angeeignet wurde, ist zwingend nötig. Kenntnisse aus den Vorlesungen „Formale Systeme“ oder „Semantik“ sind hilfreich.



Veröffentlichungen

Veröffentlichung

Finding Equations in Functional Programs

Betreuer

Ehemalige Mitarbeiter
Dr. rer. nat. Joachim Breitner

Studenten

Ehemalige Studenten
Johannes Bader