Umsetzung von Lazy Evaluation in einer immutablen Sprache
Parsing, Cross-Compiler, funktionale Programmiersprachen, Lazy Evaluation/Call-by-Need, Idris, Cairo
Als Grundlage für ein späteres Projekt im Master-Studium, den Cross-Compiler mit Haskell als Ausgangssprache erweitern zu können, werden verschiedene Ansätze, Haskells Lazy Evaluation-Modell in Cairos read-only Speichermodell abzubilden, herausgebildet und anhand verschiedener Metriken verglichen.
Gleichzeitig wird für die dem Compiler interne Repräsentation eines Programms eine textliche Schnittstelle entwickelt, die sowohl beim Debugging des Compilers hilft als auch später als Zielsprache von Haskell aus verwendet werden kann, um von den bereits existierenden Optimisierungen auf dieser IR profitieren zu können.
Am IMVS wird ein Compiler entwickelt der es ermöglicht, die funktionale Programmiersprache Idris in die prozedurale, low-level Sprache Cairo zu übersetzen. Cairo brilliert damit, bei Ausführung einen Beweis erzeugen zu können, welcher mit wesentlich geringerem Rechenaufwand überprüft werden kann, und ermöglicht somit eine vertrauenslose verteilte Anwendung.
Dafür opfert Cairo allerdings einige Features die das Programmieren in anderen Sprachen angenehmer machen, allen voran ist der Speicher in Cairo "non-deterministic & read-only". In der Praxis bedeutet das in den meisten Fällen, man kann ihn als einen Write-Once-Speicher betrachten — der Wert einer Speicheradresse ist zur gesamten Ausführung des Programms derselbe, man legt nur "Einschränkungen" darüber fest.
Idris dient als higher-level Ausgangssprache, um das Schreiben von Programmen angenehmer zu machen. Gleichermassen hat Idris gegenüber der sehr vergleichbaren Sprache Haskell zwei Unterschiede: In Idris werden Ausdrücke sofort evaluiert, in Haskell nur, wenn der Wert benötigt wird — das ist die sogenannte "Lazy Evaluation" —, und gravierender: Haskell ist wesentlich populärer.
Als Vorbereitung, den Compiler um ein Haskell-Frontend zu erweitern, ist es notwendig, diese "Lazy Evaluation" in einer effizienten Weise in Cairo abbilden zu können. Gleichzeitig, um von den bereits entwickelten Optimisierungen im Compile-Vorgang profitieren zu können, ist eine textliche Repräsentation der intern im Compiler verwendeten Datenstrukturen vonnöten, um diese als Zielsprache von Haskell aus verwenden zu können.
Für die Zwischensprache wurde eine formale Grammatik entwickelt, aufgrund derer sowohl die Serialisierung als auch das Parsing als Bestandteil
des Compilers geschrieben wurden.
Die Zwischensprache besitzt eine C-ähnliche Syntax und kann während dem Compile-Vorgang nach jeder Phase produziert werden.
Als alternative Executable bietet es sich auch an, ein Programm direkt von der Zwischensprache nach Cairo zu kompilieren.
Für die Implementation der Lazy Evaluation wurden 2 Ansätze gebildet, von denen sich einer leider als unvereinbar mit Cairos Garantien herausstellte.
Bei dem anderen Ansatz gab es drei alternative Implementations-Möglichkeiten, welche dann die Grundlage für den Vergleich gebildet haben.
Die untere Tabelle zeigt die Menge an Instruktionen, die jeweils für die spätere Ausführung einer durch "Lazy Evaluation" verzögerten Berechnung
benötigt werden, verglichen zur Baseline der Funktion selbst — eine simple Identitätsfunktion, welche ihr Argument unverändert zurückgibt.
Bachelorprojekt Informatik
Projektdauer: Februar - August 2022
Aufwand: 360h
Teamgrösse: 1 Person
Daniel Kröni & Markus Knecht, IMVS FHNW
Cyrill Brunner
Daniel Kröni, daniel.kroeni@fhnw.ch
Markus Knecht, markus.knecht@fhnw.ch
