- Hazel ist eine webbasierte Live-Umgebung für funktionale Programmierung, die Typed Holes in den Mittelpunkt stellt und es ermöglicht, auch unvollständige Programme typzuprüfen, zu bearbeiten und auszuführen
- Unvollständige Zustände wie Leerstellen, Typfehler oder Merge-Konflikte werden als Holes modelliert; zentral ist dabei, dass der Editor weniger Bereiche verliert, in denen die Semantik erhalten bleibt
- Unvollständige Programme, die sich in Hazel erstellen lassen, sind statisch und dynamisch definiert und können unvollständige Typen sowie unvollständige Ausführungsergebnisse haben
- Ziel der Implementierung ist eine funktionale Sprache der Elm/ML-Familie; genutzt wird sie als Grundlage für Programmierlehre, kollaboratives Editieren, das Lernen von Beweisen und Forschung zu AI-Codevervollständigung
- Das Open-Source-Forschungsprojekt wird vom Future of Programming Lab der University of Michigan geleitet; ein Web-Build zum Ausprobieren und der Quellcode auf GitHub sind öffentlich verfügbar
Hazel: die Kernidee
- Hazel ist eine Live-Umgebung für funktionale Programmierung, aufgebaut rund um Typed Holes
- Auch mit unvollständigen Programmen kann weitergearbeitet werden
- Typprüfung
- Bearbeitung
- Ausführung
- Ziel ist eine Umgebung, die auch dann sinnvolles Feedback liefert, wenn der Code während des Editierens in einem fehlerhaften Zustand ist
Umgang mit unvollständigen Programmen
- Im normalen Programmierprozess treten häufig Zustände auf, in denen der Programmtext formal unvollständig ist
- Leerstellen
- Typfehler
- Merge-Konflikte
- Herkömmliche Sprachdefinitionen geben solchen Strukturen keine formale Semantik, weshalb selbst das Verhalten bereits fertiger Teilstücke nur schwer als Live-Feedback behandelt werden kann
- Editoren und Werkzeuge sind dadurch gezwungen, sich auf komplexe Heuristiken zu stützen, um Codevervollständigung, Typprüfung und Code-Navigation ohne Unterbrechung anzubieten
- Hazel modelliert unvollständige Programme als Programme mit Holes
- Holes stehen für fehlende Programmteile
- Sie wirken wie eine Membran, die fehlerhafte Bereiche oder Konfliktbereiche in kollaborativen Umgebungen umschließt
- Dieser Ansatz basiert auf contextual modal type theory und gradual type theory
Hazel-Umgebung und Ausführungsmodell
- Hazel wird als webbasierte Programmierumgebung für eine funktionale Sprache implementiert, die Elm/ML ähnelt
- Alle unvollständigen Programme, die sich mit Hazels Sprache für Editieraktionen erzeugen lassen, sind statisch und dynamisch definiert
- Sie können unvollständige Typen haben
- Bei der Ausführung können sie unvollständige Ergebnisse erzeugen
- Dank dieser Eigenschaften dient Hazel als Plattform für zukünftige Programmierumgebungen und für Forschung zur Programmierlehre
Forschungsvision und Materialien
- Toward Semantic Foundations for Program Editors: Forschungsvision zu semantischen Grundlagen für Programmeditoren
- Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine: Vision einer Live-, kombinierbaren und kollaborativen Rechenumgebung für wissenschaftliches Rechnen im großen Maßstab
- Präsentationen zu Hazel sind in der YouTube playlist of Hazel-related talks gesammelt
- Eine aktuelle Demo ist in der Topos Institute Präsentation zu sehen
Aktuelle Forschung und Publikationen
- 2025 wurden mehrere Arbeiten aus dem Hazel-Umfeld auf Konferenzen vorgestellt
- Incremental Bidirectional Typing via Order Maintenance: Forschung zur inkrementellen bidirektionalen Typprüfung mithilfe von Techniken aus Browser-Layout-Systemen; ausgezeichnet mit dem OOPSLA 2025 Distinguished Paper Award
- Syntactic Completions with Material Obligations: Theorie und Implementierung zur Reparatur von Syntaxfehlern mithilfe visuell konkretisierter Verpflichtungen im Tylr-System
- A FAIR Case for a Live Computational Commons: Vorschlag zur Neugestaltung wissenschaftlicher Arbeit rund um eine groß angelegte Live-Programmierumgebung
- Decomposable Type Highlighting for Bidirectional Type and Cast Systems: UI-Forschung zum Debugging statischer und dynamischer Typfehler in Hazel
- Hazel Deriver: A Live Editor for Constructing Rule-Based Derivations: Lehrwerkzeug zum Aufbau von Herleitungen im Stil der natürlichen Deduktion
- 2024 standen Themen wie Typfehlerbehebung, die Kopplung mit LLMs, Beweislernen und Rechenumgebungen für die Klimawissenschaft im Vordergrund
- Total Type Error Localization and Recovery with Holes behandelt die Lokalisierung und Behebung von Fehlern in falsch typisierten Programmen und erhielt den POPL 2024 Distinguished Paper Award
- Statically Contextualizing Large Language Models with Typed Holes kombiniert Sprachserver mit großen Sprachmodellen und verbessert so die Leistung von AI-Codevervollständigung deutlich
- Die NSF fördert ein Forschungsprojekt, das Hazel zu einem Beweisassistenten für den Unterricht weiterentwickeln soll
- Die Forschung von 2017 bis 2023 entwickelte Hazels Grundlagen für Berechnung, strukturelles Editieren, Live-Auswertung und didaktische Hilfsfunktionen schrittweise weiter
- Hazelnut: A Bidirectionally Typed Structure Editor Calculus definiert einen Kalkül für Editieraktionen, der Typed Holes automatisch einfügt
- Live Functional Programming with Typed Holes entwickelt eine reichhaltige operationale Semantik für Ausdrücke mit Typed Holes
- Program Sketching with Live Bidirectional Evaluation behandelt Smyth, eine Basiskomponente von Hazel Assistant
- Live Pattern Matching with Typed Holes behandelt das Schließen auf Programme mit Pattern Holes und erhielt den OOPSLA 2023 Distinguished Paper Award
Nutzung und Mitwirkung
- Hazel bietet einen Web-Build zum direkten Ausprobieren
- Der Quellcode ist auf GitHub veröffentlicht
- Hazel ist ein Open-Source-Forschungsprojekt, das vom Future of Programming Lab (FP Lab) der University of Michigan geleitet wird
- Für Beiträge oder Fragen kann das Team über den Leiter Cyrus Omar kontaktiert werden
Noch keine Kommentare.