Hilde schreiben: ein Leitfaden für Modelle

Dieser Leitfaden ist für ein Sprachmodell geschrieben, aber genauso für einen Menschen, der mit einem Compiler zur Hand Hilde-Code schreiben will. Für ihn gilt eine Regel: Jedes Programm hier steht in examples/ und wird von den Prüfläufen des Projekts übersetzt und ausgeführt, und hinter jeder Ablehnung, die hier vorkommt, steht ein Test mit der echten Meldung und dem echten Fehlercode. Widersprechen sich dieser Text und der Compiler, hat der Compiler recht, und der Fehler liegt im Text.

1. Was Hilde ist

Hilde ist ein Fork von Austral (Austral), eine kleine Sprache mit linearen Typen, die nach C übersetzt. Ein Wert eines linearen Typs wird genau einmal verwendet. Dafür sorgt die Typprüfung, nicht die Sorgfalt der Programmierer. Das ist die eine Idee, der alles andere dient, und die meisten Übersetzungsfehler, auf die man am Anfang stößt, haben mit ihr zu tun.

2. Dateien und Module

Ein Modul besteht aus zwei Dateien: der Schnittstelle Name.hih und dem Rumpf Name.hiq.

module Example.HelloWorld is
    """
    No contract: the exit code of the programme, the result of what it did.
    """
    function main(): ExitCode;
end module.

module body Example.HelloWorld is
    function main(): ExitCode is
        printLn("Hello, world!");
        return ExitSuccess();
    end;
end module body.

(examples/hello-world/.) Importe stehen vor module oder module body und nennen, was sie hereinholen: import Standard.String (String, length);. Ein Modul wird zusammen mit jedem Modul übersetzt, das es importiert, jeweils als Paar interface,body:

hilde compile standard/src/String.hih,standard/src/String.hiq \
    Main.hih,Main.hiq --entrypoint=Main:main --output=main

run-examples.sh zeigt die vollständige Liste für ein Programm, das etwas ausgibt; die cli.txt neben jedem Test zeigt sie für die Module, die dieser Test verwendet.

3. Einen Übersetzungsfehler lesen

Jeder Fehler hat einen Fehlercode: Error code: H4008 in der Textausgabe, "code": {"code": "H4008", ...} mit --error-format=json, das die Form von rustc schreibt, und "code": "H4008" mit --error-format=hilde-json. die Fehlercodes listet jeden Fehlercode mit der Datei auf, die ihn auslöst, und dem Anfang seiner Meldung. Die erste Ziffer nennt die Art: 0 Parser, 1 Kommandozeile, 2 Deklaration, 3 Typ, 4 Linearität, 5 Einstiegspunkt, 6 generisch, 7 @template, 8 SQL, 9 intern.

Ein Parserfehler nennt die Stelle, und bei den am häufigsten auftretenden Ursachen auch die Ursache und die Abhilfe: ein reserviertes Wort als Name (H0008, mit einem freien Namen), ein Operator nach einer Operation ohne Klammern (H0009, mit den Klammern), ein Index nach einem Aufruf (H0010), ein ausgeliehenes Literal (H0011). Jeder andere ist H0005, "Error during parse."; Abschnitt 10 listet die Schlüsselwörter, und die Fallen die Fallen hinter den Meldungen.

Ein Modul in einer Sekunde prüfen. hilde check X.hiq parst, typisiert und prüft ein Modul – Verträge und Linearität eingeschlossen – mit den Modulen, die es importiert, gefunden in der Standardbibliothek neben dem Compiler oder in den Verzeichnissen von --modules=d:d, und schreibt kein C. Es meldet den ersten Fehler wie hilde compile, in jedem der Fehlerformate; auf einem aarch64-Linux-Rechner brauchte ein Modul der Standardbibliothek mit acht Importen weniger als eine Sekunde.

Eine Form für jede Quelle. hilde fmt <Datei oder Verzeichnis...> schreibt Hilde-Quellen in ihrer einen Form – Einrückung nach Blöcken, eine Regel für die Leerzeichen zwischen Token, höchstens eine Leerzeile – und behält die Token, die Kommentare und die Zeilenumbrüche; hilde fmt --check nennt die Dateien, die nicht in dieser Form sind, und endet mit Exit 1.

Im Editor. hilde lsp ist ein Language Server auf Standardeingabe und Standardausgabe: den ersten Fehler eines Dokuments als Diagnose, während es geschrieben wird, sowie Hover und Sprung zur Definition für einen Namen – die Deklaration mit ihrem Typ, ihrem Vertrag und ihrem Docstring.

Den Compiler fragen, statt zu raten. hilde query <module...> --module=Name gibt als JSON aus, was ein Modul deklariert – die Art jeder Deklaration, ihre Typen, wie der Compiler sie aufgelöst hat, und die Datei und Zeile, in der sie steht. Über examples/learn-linear listet es main, Ticket, issue, use und peek auf und sagt zu peek: eine private Funktion mit dem Typparameter R im Universum Region, dem Parameter ticket vom Typ &[Ticket, R], Rückgabe Nat32, geschrieben ab Zeile 21 von LearnLinear.hiq. Es erhält dieselbe Modulliste wie hilde compile.

Fragen, was ein Programm in C tut. hilde guard <module...> [--entrypoint=Module:name] listet die als unsicher markierten Module, die C- Bibliotheken und Header, jede Fremdfunktion und jedes @embed auf, jeweils mit der Angabe, ob das Programm sie vom Einstiegspunkt aus erreichen kann, und die exportierten Funktionen. Über examples/learn-sqlite nennt es die zwei unsicheren Module der SQLite-Anbindung, die Bibliotheken pthread und sqlite3, 24 Fremdfunktionen, von denen das Programm 19 erreicht, und 18 Einbettungen, alle erreicht. Wieder dieselbe Modulliste wie bei hilde compile.

4. Lineare Werte

examples/learn-linear/: ein als Linear deklarierter Record wird erzeugt, zweimal über eine Lese-Referenz angesehen und einmal verbraucht.

record Ticket: Linear is
    seat: Nat32;
end;

Eine Funktion, die ihn als Wert übernimmt, muss ihn verbrauchen, hier indem sie ihn zerlegt:

function use(ticket: Ticket): Nat32 is
    let { seat: Nat32 } := ticket;
    return seat;
end;

Die Regeln, jeweils mit dem Test, der sie festhält:

Jeder Zweig muss einen linearen Wert im selben Zustand hinterlassen. Ein früher return in einem if ohne else ist der häufigste Weg, dies zu verletzen: beide Zweige schreiben und in jedem verbrauchen oder zurückgeben.

Ein String besitzt Speicher und ist Linear: jeder endet in destroyString oder wird weitergereicht (examples/learn-text/).

5. Referenzen und Regionen

examples/learn-borrow/.

• &x ist eine Lese-Referenz, &![T, R] in einer Signatur eine Schreib-Referenz; R ist eine Region, deklariert mit generic [R: Region].
• Eine Schreib-Referenz kann nur aus einem var genommen werden (H3018); eine Zuweisung an ein let wird ebenfalls abgelehnt (H6042).
• Ein Feld wird über eine Referenz mit -> gelesen und geschrieben: counter->count := counter->count + 1;. Ein Feld eines Records, der in einem Feld liegt, wird danach mit . erreicht: listener->socket.number.
• Eine an eine Funktion übergebene Schreib-Referenz ist verbraucht. &~counter übergibt eine neue und behält counter; die letzte Verwendung kann counter selbst übergeben. Weil eine Schreib-Referenz linear ist, muss eine Funktion, die eine übernimmt, sie in jedem Zweig gleich verwenden – am einfachsten mit &~ bei jedem Aufruf.
• Solange etwas ausgeliehen ist, kann es nicht verbraucht werden (H4006, H4007), und eine lesend-schreibend ausgeliehene Variable kann nicht erneut ausgeliehen werden (H4011).

6. Fehlschlag: Option, Either, ?

examples/learn-errors/.

• Eine Funktion, die fehlschlagen kann, gibt Option[T] (Some(value => x), None()) oder Either[L, R] (Left(left => e), Right(right => x)) zurück, und der Aufrufer zerlegt es mit case ... of when Some(value as x: T) do ... when None do ... end case;.
• In einem return aus einer Funktion, deren Ergebnistyp es vorgibt, kann None() unverändert stehen . Wo der Compiler nicht erkennen kann, welches Option oder Either gemeint ist, sagt es ein getyptes let: let none: Option[Int32] := None(); – die Form, die die Standardbibliothek durchgehend verwendet.
• Ein Option oder Either zu verwerfen ist ein Übersetzungsfehler (H3037). ignore(f()); verwirft es absichtlich; ignore nimmt nur Free-Werte (H3004).
• f()? gibt den Fehlschlag sofort aus der umgebenden Funktion zurück. Es darf nur als ganze rechte Seite eines let oder als ganze Anweisung stehen (H3040), und die umgebende Funktion muss dieselbe Art Ergebnis zurückgeben (H3039). Es hält Hilde explizit: das return, für das es steht, ist geschrieben, als das Zeichen ?, an der Stelle, an der es geschieht.

7. Text und Ausgabe

examples/learn-text/. print und printLn nehmen Zahlen, Bool und Zeichenketten-Literale. Ein String wird als Span ausgegeben, getSpan(text, 0, length(text) - 1) – der letzte Index ist eingeschlossen, daher muss eine leere Zeichenkette zuerst geprüft werden: getSpan auf einer leeren Zeichenkette beendet das Programm mit "getSpan: start index out of bounds" und Exit-Status 255. Standard.StringBuilder baut eine Zeichenkette; finalize verbraucht den Builder und gibt den String heraus.

Ein Programm, das so endet, verliert, was es vorher ausgegeben hat, wenn seine Ausgabe in eine Datei ging: zwei Zeilen, die vor dem fehlschlagenden getSpan ausgegeben wurden, erreichen die Datei nicht, 0 Bytes. Wenn die letzten Zeilen eines Programms zu fehlen scheinen, zuerst seinen Fehlerstrom ansehen.

8. Literale

• Ganzzahlen: 12, hexadezimal #x1B0, oktal #o660, binär #b11000. Ein Dateimodus wird oktal geschrieben: #o600.
• Ein Zeichen-Literal 'a' ist die Ganzzahl 97: der Parser macht daraus eine Ganzzahl-Konstante, es wird also wie jedes Ganzzahl- Literal typisiert – als Argument eines Nat8-Parameters ist es ein Byte.
• Zeichenketten: "...", mit \n, \r, \t, \\ und \". Eine Zeichenkette darf auf einem Backslash enden: "\\" ist ein Backslash, und der Lexer liest einen maskierten Backslash als Paar, bevor er nach einem maskierten Anführungszeichen sucht.
• Wo der Typ eines Literals nicht durch seine Stelle gegeben ist – ein Parameter oder ein getyptes let gibt ihn vor –, darf der Compiler Int32 wählen, und ein Widerspruch folgt. Ein getyptes let legt ihn fest: let limit: Nat32 := 511;.

9. Ausdrücke und Anweisungen

• Ein Operator nimmt zwei Operanden; eine Kette braucht Klammern: (n - ((n / 2) * 2)) = 0. Ein Vergleich ist ebenfalls ein Operator: dieselbe Zeile ohne das äußere Paar ist ein Parserfehler, H0005 (examples/learn-errors).
• if ... then ... else if ... then ... else ... end if;, while ... do ... end while;, for i from 0 to n - 1 do ... end for; -- to schließt das Ende ein.
• Eine Anweisung, die nichts tut, ist skip;; eine Funktion ohne Ergebnis gibt nil zurück und hat den Typ Unit.

10. Wörter, die keine Namen sein können

Reservierte Wörter: and or not module is body import as end constant type function generic record union case of when typeclass instance method if then else let var while for do from to borrow return skip Free Linear Type Region pragma sizeof nil true false Span, und die Konstrukte zur Übersetzungszeit @embed @bytes @template @query @execute @migrations. body, type, from und to sind die, die am häufigsten als Namen gewünscht werden.

11. Die Standardbibliothek

standard/src/; jede .hih sagt in ihrem einleitenden Text, wofür das Modul da ist und was es auslässt, und dieser Text ist die Referenz. Kurz: String, StringBuilder, Buffer, Text, Utf8 für Text; File für Dateien, Pipes, Kindprozesse und Unix-Domain-Sockets; Poller zum Warten auf viele Deskriptoren (epoll oder kqueue); Task für Fibers und Kanäle; Time; Path; Regex (RE2-Syntax, lineare Zeit); Template mit @template; Sqlite mit @query, @execute, @migrations; Sftp; Libcrypto; Http, Fcgi, Ip für die Webseite; Sandbox; Arena, Box. Ein Hilde-Programm bedient das Web per FastCGI über einen Unix-Domain- Socket hinter Hiawatha: Standard.Fcgi und Standard.File.listenUnix ( für eine ganze Anfrage).

12. Unsicherer Code

C wird auf drei Wegen erreicht, und jeder braucht pragma Unsafe_Module; im Modul: @embed, das C einfügt (H2038); pragma Foreign_Import, das eine C-Funktion deklariert; und Hilde.Memory. Anwendungscode tut das nicht – eine Anbindung in bindings/ und ein sicheres Modul in standard/ darüber tun es (Abschnitt A: "Anbindungen unten, eine sichere Abstraktion darüber").

*Die Abschnitte 13 bis 17 behandeln Unions und Muster, Generics und Typklassen, Tasks, die Konstrukte zur Übersetzungszeit, Verträge und Effekte. Die Regel ist dieselbe wie oben: ein hier gezeigtes Programm ist ein Auszug, Zeile für Zeile, aus einer Datei in examples/ oder aus einem Test, und jede genannte Ablehnung hat den Fehlercode und den Test, der sie festhält.

13. Unions, case und Muster

examples/learn-match/. Eine Union ist ein Typ mit mehreren Gestalten; jedes case nennt eine, mit ihren Slots. Ein Wert entsteht, indem man die Gestalt und ihre Slots nennt, Press(key => Char(code => code), shift => shift), und eine Gestalt ohne Slots entsteht mit leeren Klammern, Enter().

union Key: Free is
    case Char is
        code: Nat8;
    case Enter;
    case Escape;
end;

Ein case zerlegt einen Wert mit Mustern, die so tief gehen wie der Wert selbst:

case event of
    when Press(Char(97 .. 122), false) do
        printLn("a small letter");
    when Press(Char(97 .. 122), true) | Press(Char(65 .. 90), _) do
        printLn("a capital letter");
    when Press(Char(48 .. 57), _) do
        printLn("a digit");

Ein Bereich 97 .. 122 schließt beide Enden ein. Ein senkrechter Strich | verbindet Muster, die eine Antwort haben. _ nimmt jeden Wert ohne Namen, und ein Name nimmt ihn und bindet ihn. Das erste passende Muster wird genommen.

14. Generics und Typklassen

examples/learn-typeclass/, examples/generic-union/. Ein Typparameter steht in eckigen Klammern mit seinem Universum, Pair[T: Free]; die Universen sind Free, Linear, Type (ein Parameter, der beides nimmt: Standard.Box ist Box[T: Type], standard/src/Box.hih) und Region (Abschnitt 5). Eine Union ist auf dieselbe Weise generisch:

union Optional2[T: Type]: Type is
    case None2;
    case Some2 is
        value: T;
end;

Eine Typklasse nennt, was ein Typ kann, und eine Instanz sagt, wie ein Typ es tut. Eine generische Instanz gibt einem aus anderen aufgebauten Typ dieselbe Fähigkeit, aus den Instanzen seiner Teile, und eine generische Funktion verlangt die Fähigkeit im Universum ihres Parameters, T: Free(Shape):

typeclass Shape(T: Free) is
    method area(shape: T): Nat32;
    method name(shape: T): Span[Nat8, Static];
end;

instance Shape(Square) is
    method area(shape: Square): Nat32 is
        return shape.side * shape.side;
    end;

    method name(shape: Square): Span[Nat8, Static] is
        return "square";
    end;
end;

generic [U: Free(Shape)]
instance Shape(Pair[U]) is
    method area(shape: Pair[U]): Nat32 is
        return area(shape.first) + area(shape.second);
    end;

generic [T: Free(Shape)]
function report(shape: T): Unit is
    print(name(shape));
    print(": ");
    printLn(area(shape));
    return nil;
end;

Der Compiler wählt die Instanz nach dem Typ des Arguments, daher brauchen report(square) und report(Pair(first => square, second => Square(side => four))) nicht mehr als den Aufruf. Was abgelehnt wird:

15. Tasks

examples/learn-tasks/. Ein Task wird in einem Scope mit spawn gestartet, das den Task zurückgibt oder, wenn keiner gestartet werden konnte, das Argument; join wartet auf ihn und gibt sein Ergebnis zurück. Ein Scope endet erst, wenn jeder Task darin beendet ist, und closeScope beendet ihn.

case spawn(scope, sumSquares, Range(first => first, last => last)) of
    when Right(right as task: Task[Nat64]) do
        let started: Option[Task[Nat64]] := Some(value => task);
        return started;
    when Left(left as back: Range) do

Ein Task teilt nichts: sein Argument wird hineinkopiert, und sein Ergebnis wird von join zurückgegeben. Standard.TaskArena gibt einem Task eine eigene Arena, die mit dem Ergebnis zurückgeht (spawnWithArena). Das Beispiel führt seine vier Tasks in fester Reihenfolge zusammen, daher ist seine Ausgabe bei jedem Lauf gleich, obwohl die Tasks in beliebiger Reihenfolge enden. Was abgelehnt wird:

Wo ein Task einen Wert lesen muss, der dem Aufrufer gehört, leistet das ein Verleih-Scope für die Dauer einer Ausleihe . Ein Task kostet 64 KiB Adressraum und eine Speicherseite, sobald er läuft.

16. Konstrukte, die mit einem At-Zeichen beginnen

Jedes wird vom Compiler gelesen, und ein Fehler darin ist ein Übersetzungsfehler.

@bytes und @embed (examples/learn-embed/). @bytes("motto.txt") legt die Bytes einer Datei neben dem Modul in das Programm, als Span von Static; die Datei wird nicht gebraucht, wenn das Programm läuft. Ein Pfad, der das Verzeichnis des Moduls verlässt, oder keine Datei wird abgelehnt (H6001, H6002;). @embed fügt C ein und braucht pragma Unsafe_Module; (Abschnitt 12).

let motto: Span[Nat8, Static] := @bytes("motto.txt");

@template (examples/learn-template/). Eine Vorlage in der Syntax von Jinja2, order.jinja, wird aus einem Record gefüllt, und der Compiler macht daraus Code.

@template("order.jinja", order, out);

Ein Name, den der Record nicht hat, oder ein Filter, den es nicht gibt, ist ein Übersetzungsfehler, keine Überraschung zur Laufzeit:

@migrations, @execute, @query (examples/learn-sqlite/). Die Dateien unter migrations bauen das Schema, und der Compiler prüft jede Anweisung dagegen. Werte gehen als Parameter an die Datenbank, nie in den Text.

report("insert", @execute(&~db, "INSERT INTO notes (content) VALUES (?)", "buy bread"));

17. Verträge und Effekte

examples/learn-contracts/, examples/learn-records/. Ein Vertrag steht nach dem Rückgabetyp einer Funktion, und der Vertrag einer öffentlichen Funktion steht in der Schnittstelle, .hih, neben der Funktion. requires sagt, was beim Aufruf gelten muss, ensures, was bei der Rückkehr gilt, und old(...) nennt einen Wert, wie er beim Aufruf war. Hilde prüft sie, während das Programm läuft, und ein verletzter beendet das Programm und nennt, welcher Vertrag, wo er geschrieben steht und wo der Aufruf erfolgte (examples/learn-contracts/ hat ein Programm, das das tut).

generic [R: Region]
function withdraw(account: &![Account, R], amount: Nat64): Unit
    requires (amount > 0) and (amount <= balance(&account))
    ensures balance(&account) = (old(balance(&account)) - amount);

Ein Record kann eine Invariante tragen, die geprüft wird, sobald ein Wert sein Modul verlässt (examples/learn-records/):

record Interval: Linear is
    low: Nat32;
    high: Nat32;
    invariant low <= high;
end;

hilde test --contracts zieht Eingaben aus den Verträgen und gibt seinen Seed aus, und ein einfaches ensures wird bewiesen, wenn das Programm übersetzt wird, was seine Prüfung entfallen lässt (Suite).

Effekte. Eine Funktion nennt nach ihrem Rückgabetyp die Fehlerarten, mit denen sie enden kann, raises NotFound, und raise NotFound; beendet das Programm mit dieser Art . Die Klausel steht auch in der Schnittstelle . Eine Panik – abort, ein verletzter Vertrag, ein abgefangener Überlauf – trägt keine Art und braucht keine Klausel .

function pick(n: Int32): Int32
    raises NotFound is
    if n < 0 then
        raise NotFound;
    end if;
    return n;
end;