Prism: Eine nicht-reine funktionale Sprache mit typisierten Effekten

 (stephendiehl.com)
1 Punkte von GN⁺ 2 시간 전 | 1 Kommentare | Auf WhatsApp teilen
  • Prism ist ein experimenteller Compiler, der Effekte wie veränderliche Variablen, Exceptions und Streams nicht verbirgt, sondern im Typ sichtbar macht, während lokal nicht von außen beobachtbare Änderungen weiterhin reine Typen wie Int -> Int behalten
  • Im Kern stehen algebraische Effekt-Handler und Row Polymorphism: Effekte werden in die Zeile des Funktionstyps zusammengeführt, und Handler behandeln nur die benötigten Labels und reichen den Rest weiter
  • Dasselbe Effektsystem beschreibt Exceptions, Generatoren/Streams, Lenses, var-Zustand und fail/guard-Kontrollfluss; einige Pfade werden ohne Zwischenlisten oder Laufzeit-Komposition lowered
  • Auf der Performance-Seite kombiniert Prism Evidence Passing mit Perceus-Referenzzählung, um Allokationen pro Effektaufruf zu vermeiden, und optimiert funktionale Updates eindeutig besessener Werte zu In-Place-Änderungen
  • Prism liefert LLVM IR, MLIR, eine C-Runtime, einen Rust-Interpreter, ein Lean-4-Modell und einen WASM-Playground mit, sodass sich Typinferenz und Lowering-Ergebnisse direkt prüfen lassen

Von außen unsichtbare Änderungen und typisierte Effekte

  • Ausgangspunkt von Prism ist die Beobachtung, dass auch eine fib-Funktion, die intern var und Zuweisungen nutzt, für externe Beobachter wie eine reine Funktion aussehen kann
    • Das Beispiel fib aktualisiert zwei Variablen in-place, gibt aber keinen Zustand nach außen preis
    • Der Typ ist Int -> Int, und der Effekt erscheint nicht im Typ
  • Prism ist ein in den letzten drei Jahren entwickelter Proof-of-Concept-Compiler für funktionale Programmierung, der Effekte auf Basis moderner Typideen aus OCaml 5, Haskell und der Koka-Familie modelliert
  • Die zentrale Richtung besteht nicht darin, Effekte zu vermeiden, sondern sie ins Typsystem aufzunehmen und den Compiler so zu optimieren, dass die Kosten verschwinden

Effekte verhalten sich wie Interfaces

  • Effekte in Prism folgen dem Ansatz algebraischer Effekt-Handler: Ein Effekt deklariert Operationen, und ein Handler gibt diesen Operationen ihre Bedeutung
    • effect Gen { ctl yield(Int) : Unit } deklariert die Operation yield
    • !{Gen} in fn produce(n) : !{Gen} Unit kennzeichnet im Typ, dass die Funktion yield ausführt
  • Selbst derselbe Producer wird je nachdem, wie die Continuation k behandelt wird, unterschiedlich interpretiert
    • total summiert die yield-Werte
    • count zählt die Anzahl der yield-Aufrufe
    • Wird k verworfen, ergibt sich eine Exception; wird sie einmal aufgerufen, entstehen Zustand oder Generator; wird sie mehrfach aufgerufen, entsteht Suchverhalten
  • Das Amb-Effektbeispiel beschreibt die Suche nach pythagoreischen Tripeln mit choose und reject
    • choose(n) liefert Werte im Bereich 0..n-1
    • Der Handler setzt dieselbe Continuation für jeden Kandidaten fort und erzeugt so einen Suchbaum
  • Anders als OCaml 5 nimmt Prism Effekte in den Typ auf, ohne dass man wie bei Haskells Monad-Transformer-Stacks manuell Schichten hochziehen muss
    • Effektzeilen werden über Aufrufe hinweg strukturell zusammengeführt
    • Sie verhalten sich nicht wie ein Stack, sondern wie eine Menge von Labels

Funktionen, die mit einem einzigen Mechanismus ausgedrückt werden

  • Exceptions

    • Exceptions sind in Prism Handler, die die Continuation verwerfen
    • Eine final ctl-Klausel verwirft k und verwendet den Wert ihres Bodys als Handler-Ergebnis
    • Das ist kein Ansatz, bei dem Result weitergereicht oder ? über den Call Stack verstreut wird
    • Da Exceptions Labels in der Effektzeile sind, werden sie als erweiterbare Exceptions komponiert
    • Jeder Fehler ist eine eigene Operation, und die Zeile im Funktionstyp zeigt an, welche Exceptions nach außen gelangen können
    • Im Beispiel mit Abort und Timeout hat fetch den Typ !{Abort, Timeout}
    • with_default behandelt nur Timeout, gibt als Fallback "cached" zurück, und nach der Behandlung bleibt im Typ nur !{Abort} übrig
    • Anders als Javas checked exceptions sind sie nicht an eine Klassenhierarchie gebunden, sondern funktionieren als offene strukturelle Menge

  • Generatoren und Streams

    • Ein Stream besteht aus einem Producer, der emit ausführt, aus Transformern, die dies abfangen und erneut ausgeben, und aus Consumern, die folden
    • Die Pipeline ist eine Schachtelung von Handlern um einen Producer herum, sodass strukturell keine Zwischenlisten entstehen
    • Beispiel: srange(1, n).smap(square).skeep(even).stake(5).ssum()
    • Frühes Abbrechen wie bei stake(5) ist ein Handler, der nach Erhalt der benötigten Werte die Continuation verwirft
    • Die Stream-Bibliothek ist von Haskells pipes und conduit beeinflusst

  • Lenses

    • Lenses in Prism sind keine separate Bibliothek, sondern eine Kombination aus Record-Update-Pfaden und Speichermodell
    • In verschachtelten Records lassen sich mit einem einzigen Pfadausdruck mehrere tiefe Felder aktualisieren
    • Beispiel: { g | player.pos.x = 30, player.hp = 95, score = 110 }
    • Die Spine des verschachtelten Records wird neu aufgebaut; wenn ein Wert eindeutig besessen ist, werden die zerlegten Zellen wiederverwendet
    • Durch diese Struktur können funktionale Updates zu Pointer-Schreibvorgängen kompiliert werden
    • Zur Laufzeit werden keine Optic-Typen alloziert oder komponiert
    • deriving (Lens) erzeugt gewöhnliche Funktions-Accessors wie score_of und with_score

  • Veränderlicher Zustand

    • var wird zu get/set-Operationen eines privaten Effekts desugared
    • Ein am Ende des Blocks installierter Handler behandelt diesen Effekt
    • Escape-Analyse für Closures weist Fälle zurück, in denen Zustand nach außen entweicht
    • Die umschließende Funktion kann eine leere Effektzeile behalten

  • Fehlschlag

    • Fehlschlag wird als anonymer Fail-Effekt dargestellt; das Typsystem behandelt damit „dieser Ausdruck erzeugt möglicherweise keinen Wert“
    • fail() führt einen Fehlschlag aus, und guard(cond) schlägt fehl, wenn die Bedingung falsch ist
    • ?? verwendet einen Fallback, wenn die linke Seite fehlschlägt
    • ?. bricht beim Durchlaufen einer Optionskette früh ab
    • Ein Comprehension-Guard beschneidet fehlgeschlagene Elemente, statt einen Crash auszulösen
    • Da auch var Handler-Sugar ist, kann ein transact-Block Live-Variablen snapshotten und bei Fehlschlag zurückrollen

Moderne Typ-Features

  • Prism nutzt bidirektionale Higher-Rank-Typinferenz nach Dunfield-Krishnaswami, damit in den meisten Codeabschnitten keine Typsignaturen geschrieben werden müssen
  • An Grenzen, an denen Higher-Order-Polymorphie nötig ist, werden Binder mit forall explizit gemacht
    • pick(g : forall a. (a) -> a) kann g sowohl auf Bool als auch auf Int anwenden
    • In einem Damas-Milner-Kern würde a beim ersten Aufruf mit Bool unifiziert, sodass der zweite Aufruf abgelehnt würde
  • Ad-hoc-Polymorphie wird durch Type Classes im Lean-Stil dargestellt
    • Instanzen sind benannte Werte
    • given Ord(a) verlangt ein Dictionary
    • Gibt es mehrere Instanzen, wird eine als canonical markiert, die anderen werden mit using explizit angegeben
  • deriving erzeugt wiederkehrende Instanzen und Feld-Accessors wie Eq, Ord, Show und Lens
  • Auch Pattern Matching ist mit Klassen verknüpft
    • pattern First(n) for Peek = view peek ist ein Pattern, das eine Klassenmethode als View nutzt
    • head_or kann dasselbe Pattern für mehrere Typen verwenden, die eine Peek-Instanz haben
  • show funktioniert typorientiert, ohne separate Klasse
    • Der Compiler synthetisiert aus dem statischen Typ einen strukturellen Printer
    • Er liest keine Laufzeit-Typ-Tags, um die Ausgabeform zu bestimmen
  • Auch Effektzeilen sind polymorph
    • fn twice(f : (Unit) -> Int ! {| e}) addiert die Ergebnisse der übergebenen Funktion, unabhängig davon, welche Effektzeile e hat
    • Bei einem reinen Thunk wird e mit der leeren Zeile {} unifiziert
    • Bei einem Thunk, der Effekte wie Tick oder Say ausführt, wird diese Zeile unverändert weitergereicht

Kompilierungsansatz zur Senkung der Effektkosten

  • Lehrbuchimplementierungen algebraischer Effekte rekonstruieren Berechnungen oft als Baum in Form einer Free Monad und können pro Operation eine kleine Zelle allozieren
  • Prisms schneller Pfad ist Evidence Passing aus der Koka-Familie
    • Statt Berechnungen zu rekonstruieren, um Handler zu finden, werden aktive Handler-Klauseln wie normale Parameter an jede Operationsstelle übergeben
    • do op wird zu einem direkten Aufruf lowered
    • Beim Installieren eines Handlers wird nur eine Closure alloziert; die Kosten sind daher O(handlers) und nicht proportional zur Anzahl der Operationen
  • Die Free-Monad-Codierung bleibt als Fallback erhalten
    • Berechnungen, die in Datenstrukturen entweichen
    • Echte Multishot-Resumptions
    • Muster wie masked Handler
  • Stream-Pipelines berechnen mit interprozeduraler Flow Analysis die benötigte Effect Evidence über Funktionsgrenzen hinweg
    • Evidence wird durch Producer und Transformer durchgereicht
    • Die ganze Kette wird zu einer einzelnen Schleife lowered
    • Es gibt weder Zwischenlisten noch Zellallokationen pro Operation
  • Dieser Ansatz erzielt in einem Effekt-Compiler eine Struktur mit ähnlichen Ergebnissen wie Haskells Stream Fusion oder die Vereinheitlichung von Rust-Iterator-Adaptern

Speichermodell und Runtime

  • Prism verwendet Perceus-Referenzzählung
    • Heap-Zellen werden an statisch bekannten Punkten deterministisch freigegeben
    • Es gibt keine Pausen und kein Tracing
  • Frame-limited Reuse reicht eine gerade per Pattern Match zerlegte Zelle an die Konstruktorseite zurück
    • map über einer eindeutig besessenen Liste sieht wie eine reine Funktion aus, die eine neue Liste zurückgibt, kann tatsächlich aber in-place ändern
    • Dass Lens-Updates zu Pointer-Schreibvorgängen kompiliert werden, basiert auf demselben Mechanismus
  • Die Runtime-Struktur ähnelt den Speicherregeln von Lean 4, doch Prism gibt LLVM IR aus
    • LLVM IR wird über inkwell erzeugt
    • Für dasselbe Programm wird außerdem ein textuelles MLIR-Modul erzeugt
    • Das Ergebnis wird mit clang gegen die handgeschriebene C-Runtime prism_rt.c gelinkt
  • prism_rt.c ist eine kleine Runtime von rund 2.000 Zeilen
    • Heap-Zellen haben die Form { refcount, tag, arity, fields... } und bestehen aus mindestens vier Words
    • Enthalten sind Allocator, rc_inc/rc_dec, ein Allocator für In-Place-Reuse sowie Primitive für Bignums und Strings
    • Es gibt keinen Collector Thread, keine Card Table und keine Safepoints
  • Der Standard-Allocator ist malloc aus libc; für Benchmarks gibt es eine opt-in-mimalloc-Konfiguration
  • Ein Live-Cell-Oracle assertet beim Beenden, dass die Heap-Balance 0 ist, damit die Testsuite die garbage-free-Eigenschaft prüft

Lean-Modell und Backend-Verifikation

  • Der Prism-Interpreter gehört zur Familie der CEK-Maschinen, und diese Maschine ist im Lean-4-Modell models/Prism.lean abgebildet
  • Das Lean-4-Modell enthält einen maschinengeprüften Satz, dass die Small-Step-Relation deterministisch ist
    • Ein Programm geht in genau einen nächsten Zustand über
  • Der Interpreter der Rust-Implementierung wird auch als differential Oracle verwendet
    • Alle Programme im Corpus müssen den Interpreter sowie die Backends für LLVM, MLIR und C-linked binary durchlaufen
    • Die Ausgaben der vier Ergebnisse müssen byte-identical sein, damit der Build besteht
  • Determinismus ist die Grundlage für replayable durable execution
    • Die Idee ist, dass bei fixierten Eingaben und aufgezeichneter Ausführung eine bitgenaue Wiedergabe möglich ist
    • Für künftige Versionen ist ein Prism skizziert, das Replay-Sicherheit nach einem Crash als Typeigenschaft prüft

WASM-Playground und Quellcode

  • Derselbe Interpreter wird nach WASM kompiliert und kann im Playground ohne Installation Prism-Code ausführen
  • Der Playground führt Programme in einem Worker aus
  • Per Button lassen sich inferierte Typsignaturen, Effect Row und lowered Core IR ausgeben
    • So lässt sich sehen, in welche Form var-Schleifen oder Stream-Pipelines tatsächlich lowered werden
  • Die Beispiele aus dem Text sind im Dropdown enthalten
  • Der gesamte Quellcode, das Lean-Modell und die C-Runtime befinden sich im Prism-Repository auf GitHub

Implementierungslinie und Projektcharakter

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2 시간 전
Kommentare auf Lobste.rs

  • Ich verstehe nicht, was Lenses mit Effekten zu tun haben. Jedes Mal, wenn der Artikel Lenses erwähnt, wirken sie, abgesehen davon, dass sie unter „ein Trick auf fünf Arten“ zusammengefasst werden, ziemlich unabhängig voneinander.
    Und ich verstehe auch nicht, was tick_use() überhaupt tun soll. Erwartet man, dass Leser ein so verknotetes Beispiel ohne Erklärung verstehen? Typannotationen hätten vermutlich geholfen.

    • Lenses werden hier ausführlicher erklärt: https://sdiehl.github.io/prism/spec.html#86-optic-paths
      Trotzdem sehe ich, abgesehen von der metaphorischen Ebene, nicht wirklich, was Lenses mit Effekten zu tun haben. Der Autor schreibt:

      This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
      Die Metapher scheint also diese zu sein: Monaden sind Werte, Effekte sind dagegen keine Werte, sondern eine Art Kontrollstruktur. Ebenso sind Lenses Werte, während Prisms optic paths keine Werte sind, sondern eher Kontrollstrukturen mit fest verdrahteter Syntax.

  • Ich muss mir mehr Zeit nehmen, um es zu verstehen, aber es sieht wirklich schön aus.

  • Wirklich beeindruckend. Umso mehr frage ich mich, warum Diehl den Compiler am Ende des Artikels als Spielzeug bezeichnet. Es wirkt wie ein gelungener Proof of Concept, der ein neues Maß an Eleganz zeigt.

  • Ich würde gern genauer sehen, wie die Call-by-Push-Value-Zwischendarstellung tatsächlich aussieht. Besonders interessiert mich, wie sie Join Points behandelt.
    Es gab Arbeiten zur Theorie, Effekte an CBPV zu hängen. Zu sagen, dass Berechnungen Effekttypen haben und Werte nicht, ist ziemlich natürlich; ich habe es aber noch nicht so konkretisiert gesehen, dass es sich direkt auf Kokas Evidence Passing anwenden ließe, daher ist das spannend.
    Insgesamt würde ich gern wissen, wo es im Vergleich zu Koka steht. Mit Blick auf FBIP, Perceus und Evidence Passing ist klar, dass es stark von der Koka-Arbeit inspiriert ist, zugleich ist es durch CBPV als Zwischendarstellung auch eindeutig anders. Nur wie anders, ist nicht ganz ersichtlich.

  • Es sieht sehr nach dem aus, wofür ich mir immer wieder Zeit nehmen wollte, um es zu bauen. Schön!

  • Etwas off-topic, aber ich fand es immer ein bisschen schade, dass Stephens Projekt „write you a haskell“ vor ein paar Jahren stehen geblieben ist. Für Prism würde ich mir eine Implementierungserklärung auf Tutorial-Niveau wünschen.

  • Ich frage mich, was an dieser Sprache „impure“ ist. Das Wort taucht nur im Titel auf und danach im Text nicht mehr.
    Da alle Effekte nachverfolgt zu werden scheinen, sind effektfreie Funktionen weiterhin mathematische Funktionen. Übersehe ich etwas?

    • Es scheint damit zusammenzuhängen, dass man innerhalb von Funktionsdefinitionen lokale veränderliche Variablen verwenden kann, wie in der gegebenen fib-Definition. var x ist eine impure veränderliche Variable, während let x eine pure unveränderliche Variable ist.

  • Wirklich cool ist, dass Dinge, die normalerweise als Features einer Sprache behandelt werden, etwa yield in Sprache X oder throw in Sprache Y, als eine weitere Schnittstelle implementiert wurden.
    Dass sich verschiedene Kontrollflüsse wie Nebenwirkungen, Ausnahmen und Continuations auf einer einzigen Abstraktion aufbauen lassen, ist eine interessante Art, die gesamte Designfrage neu zu betrachten. Ich hoffe, dass das mehr Erkundung und Innovation ermöglicht oder anstößt. Ich werde wohl noch über Jahre hinweg darauf zurückkommen, um Inspiration zu finden.