Hazel, eine Live-Umgebung für funktionale Programmierung mit Typed Holes

Hazel

• Hazel ist eine Live-Umgebung für funktionale Programmierung, die unvollständige Programme mit Typed Holes typprüfen, bearbeiten und ausführen kann
• Es gibt keine bedeutungslosen Editorzustände

Motivation

• Beim Programmieren verbringt man viel Zeit mit formal unvollständigem Programmtext, etwa durch Lücken, Typfehler oder Merge-Konflikte
• Bestehende Programmiersprachdefinitionen weisen solchen Strukturen keine formale Bedeutung zu
• Programm-Editoren und Tools müssen sich daher auf komplexe Behelfslösungen stützen
• Hazel modelliert unvollständige Programme auf Grundlage der Typentheorie

Merkmale von Hazel

• Eine funktionale Programmiersprache ähnlich wie Elm/ML, umgesetzt als webbasierte Umgebung
• Auch unvollständige Programme sind statisch und dynamisch wohldefiniert
• Kann als Forschungs- und Lehrplattform genutzt werden

Neuigkeiten und Veröffentlichungen

• Januar 2025: Grove-Paper bei POPL 2025 bedingt angenommen
• Oktober 2024: Forschung vorgestellt, die große Sprachmodelle mit Typed Holes kombiniert, auf der OOPSLA 2024
• Oktober 2024: Geplante Keynote von Cyrus auf der HATRA 2024
• September 2024: NSF-Fördermittel für die Entwicklung eines Beweisassistenten für den Unterricht bewilligt
• Januar 2024: Paper zu Fehlerlokalisierung und -behebung auf der POPL 2024 vorgestellt
• Oktober 2023: Forschung zu Pattern Matching auf der OOPSLA 2023 vorgestellt
• Januar 2023: Mit dem NSF CAREER Award ausgezeichnet

Team Hazel

• Hazel ist ein Open-Source-Forschungsprojekt unter der Leitung des Future of Programming Lab an der University of Michigan
• Bei Fragen oder Interesse an Beiträgen kann man den Teamleiter Cyrus Omar kontaktieren

Zusammenfassung von GN⁺

• Hazel schlägt einen neuen Ansatz für den Umgang mit unvollständigen Programmen vor und ist eine nützliche Plattform für Programmierausbildung und Forschung
• Auf Grundlage der Typentheorie macht es auch unvollständige Programme ausführbar und trägt so zur Erforschung der Zukunft des Programmierens bei
• Ähnliche Projekte mit vergleichbaren Funktionen sind Elm, ML und verschiedene Werkzeuge für die Programmierausbildung

[GN⁺]

Hacker-News-Kommentar

• Eine der Eigenschaften von Eclipse war die Fähigkeit, unvollständigen oder fehlerhaften Code auszuführen. Das war möglich, weil der Java-Compiler von Eclipse für fast jede Datei Bytecode erzeugen konnte. Diese Funktion bot eine sehr produktive Umgebung, und es ist schade, dass sie in anderen großen Systemen nicht umgesetzt wurde.

• Haskell bietet Typed Holes, und es gibt ein Plugin mit Code-Aktionen, um diese zu vervollständigen oder Fälle aufzuspalten. Agda hat ebenfalls Typed Holes und bietet noch leistungsfähigere Funktionen.

• Ich beantworte gern Fragen zu Hazel und habe in den letzten vier Jahren als Doktorand von Cyrus an Hazel gearbeitet. Derzeit entwickle ich für Hazel eine moldable projectional interface für Live Programming.

  • Liste der Funktionen, die ich zu Hazel hinzugefügt habe: GitHub-Link
  • Video eines Vortrags darüber, wie Typed Holes und der Hazel Language Server Code-Kontext für LLM-Code-Vervollständigung bereitstellen: YouTube-Link

• Hazel ist eine Live-Functional-Programming-Umgebung mit Typed Holes als zentralem Merkmal. Weitere Informationen: Hacker-News-Link

• Tylr ist eine Demo für tile-basiertes Editing, eine neue Form des Struktur-Editings. Weitere Informationen: Hacker-News-Link

• Mir gefallen die Codebeispiele von Hazel, und ich mag den Live-Editor sowie die rechts eingeblendete Dokumentation. Ich frage mich aber, ob es über einen Live-Editor und Type Checker hinaus noch mehr bietet und ob man damit tatsächlich Programme schreiben kann.

• Die Editor-UI ist wunderschön und funktioniert auch auf Mobilgeräten gut. Sehr beeindruckend.

• Interessant ist die Syntax, bei der ein "let"-Binding mit "in" endet. Beispiel:

  let comparison =
   (0 == 0, 0 < 1, 1 <= 1, 2 > 1, 1 >= 1) 
  in
  

  Weiß jemand, warum es das Schlüsselwort "in" gibt?

• Idris wurde zwar nicht erwähnt, aber dort habe ich diese Art der Entwicklung zum ersten Mal gesehen. Zugehöriges Video: YouTube-Link

• Ich habe den Playground auf einem Android-Smartphone ausprobiert, aber Tastatureingaben werden nicht in den Quellcode übernommen. Ich kann den Cursor per Tippen positionieren und die virtuelle Tastatur erscheint, aber Eingaben sind nicht möglich. Ich frage mich, ob das ein Bug oder eher ein UX-Problem ist.

• Ich mochte Hazel schon immer und es wäre wahrscheinlich ein großartiges Werkzeug für die Lehre. Ich frage mich, was mit Hazel bisher gebaut wurde.