Struktur und Typen

Statische Prüfung und Warnungen

Antra kann deinen Code prüfen, ohne ihn auszuführen: die statische Prüfung liest nur den Syntaxbaum und meldet typische Fehler und Aufräum-Warnungen — Tippfehler in Namen, ungenutzte Variablen, falsche Argumentzahlen und Ähnliches.

Wie man Typannotationen schreibt, erklärt Kapitel 16; dieses Kapitel beschreibt die Prüfung und ihre Meldungen. Es zeigt praktisch:

• wie du die Prüfung startest,
• welche Meldungen es gibt,
• wie du einzelne Warnungen bewusst stummschaltest (# ignore: und @ignore_warning(...)),
• und wie du mit @dynamic Pakete markierst, deren Member erst zur Laufzeit entstehen.

Die Kurzversion#

• antra --check datei.ant prüft ohne auszuführen.
• Fehler führen zu Exit-Code 1, Warnungen nicht.
• Eine einzelne Zeile beruhigst du mit # ignore: <code> am Zeilenende.
• Eine Funktion oder ein Package beruhigst du mit @ignore_warning(<code>).
• Ein Package, das seine Member zur Laufzeit füllt, markierst du mit @dynamic.

Für den Alltag reicht das schon.

Die Prüfung starten#

antra --check mein_skript.ant

Die Prüfung läuft, ohne das Skript auszuführen. Meldungen erscheinen auf stderr. Gibt es mindestens einen Fehler, endet der Aufruf mit Exit-Code 1 — praktisch für CI oder einen Pre-Commit-Hook. Reine Warnungen lassen den Exit-Code bei 0.

Beispielausgabe:

warning: 'a' is never used - prefix with '_' to silence
  1 | fn f(a) -> 1
           ^

Wenn du die Meldungen maschinenlesbar brauchst (z.B. für ein eigenes Werkzeug), gibt es antra --dump-check datei.ant, das die Diagnosen als JSON auf stdout schreibt. Der Editor-Integration (VS Code) nutzt genau diesen Weg für die roten und gelben Unterstreichungen.

Das graduelle Typsystem ist im Aufbau. Welche Typen es für deine Bindungen ermittelt, zeigt antra --dump-types datei.ant (JSON auf stdout, die Typen in Annotationssyntax). types listet die Top-Level- und Package-Bindungen, locals die lokalen (Parameter, val/my im Rumpf, Pattern-Variablen) mit der Zeile, in der sie gebunden werden. Die VS-Code-Extension zeigt daraus den Typ im Hover:

fn id(x) -> x                  # fn(T) -> T
fn f(x :- Number, y) -> x + y  # fn(Number, Number) -> Number
val mixed = [1, "a"]           # [Int, String]

Die Inferenz selbst meldet nichts: Widersprechen sich Teile ohne Annotation, bekommt die Stelle den Typ Any. Ein _ steht für einen Typ, den nichts festlegt (my f = |x| -> x ergibt fn(_) -> _).

Was die Prüfung meldet#

Jede Meldung hat einen kurzen Code (kebab-case). Den brauchst du gleich zum gezielten Stummschalten.

Die letzten sechs Codes betreffen das dynamische Scoping mit given/requires (siehe Kapitel 18). Bemerkenswert ist vor allem, wo sie melden: eine Anforderung wandert still durch alle Zwischenfunktionen nach oben — die müssen also nichts deklarieren, was sie selbst nicht benutzen. Gemeldet wird erst dort, wo die Kette endet: bei einem Aufruf auf oberster Ebene oder unter @main (unsatisfied-dynamic), und an einer pub fn, die eine Anforderung aus der Datei heraus trägt (undeclared-public-requirement). Letzteres ist kein Schönheitsfehler: beim Prüfen einer fremden Datei liest Antra nur deren Signaturen, nicht deren Aufrufketten — was nicht deklariert ist, kann beim Aufrufer also gar nicht geprüft werden.

Wie überall gilt: nicht analysierbar heißt nicht gemeldet. Aufrufe über eine Variable, Lambda-Rümpfe und Protokoll-Dispatch erzeugen keine Meldung, und in einem given-Block, der so etwas enthält, schweigen auch unused-given und Verwandte.

Zu discarded-branch-value: |> bindet nach else nur an den else-Zweig — wie in F#, OCaml und Haskell, wo der else-Zweig so weit wie möglich nach rechts reicht. Damit tut

if cond then "full" else "empty" |> println   # then-Fall: gibt nichts aus

im then-Fall sichtbar nichts: "full" wird berechnet und verworfen. Gemeint war meist die Klammerform:

(if cond then "full" else "empty") |> println

Zweige mit Seiteneffekten (if c then println(a) else println(b)), die Block-Form { … } und das letzte Statement eines Funktionsrumpfs (dort ist der Wert der Rückgabewert) sind ausgenommen.

Zu one-armed-if-value: wird ein if/unless ohne else als Wert gebunden, landet still undef in der Bindung, sobald die Bedingung nicht greift — nirgends im Code steht, dass das passieren kann:

val x = if cond then compute()            # warning: one-armed-if-value
val x = if cond then compute() else undef # ok: Fallback explizit

Statement-Position (if debug then println("...")) und Postfix-if (x = 5 if cond — das Statement wird uebersprungen, es entsteht kein Wert) sind bewusst nicht betroffen.

Zu yield-block-lambda: hinter yield sind geschweifte Klammern ein Block-Lambda, kein Block. Die Comprehension liefert dann eine Funktion pro Element statt des Blockwerts:

select (x <- xs) yield { val y = x * 2
    y + 1 }                                 # warning: yield-block-lambda
select (x <- xs) yield do { val y = x * 2
    y + 1 }                                 # ok: der Wert des Blocks
select (x <- xs) yield { _ + x }            # ok: gewolltes Lambda (nutzt _)

Blöcke, die _ oder _1, _2, … nutzen, und explizite Lambdas (|v| -> …, || -> …) sind bewusst nicht betroffen.

Zu stored-generator: select (...) yield ... liefert keinen fertigen Wert, sondern einen Generator, der nur einmal durchlaufen werden kann. Liegt er in einer Map oder einem Array — typisch: ein State, der jeden Frame neu gelesen wird —, ist er ab dem zweiten Durchlauf leer:

val state = %{bars: select (x <- xs) yield x * 2}            # warning: stored-generator
val state = %{bars: [..select (x <- xs) yield x * 2]}       # ok: ein Array
val state = %{bars: collect(select (x <- xs) yield x * 2)}   # ok: dasselbe

An einen Namen gebunden oder zurückgegeben bleibt der Generator unbeanstandet; dort ist das einmalige Durchlaufen meist gewollt.

Zu defer-in-use-callback: use macht den Rest des Blocks zum Callback. Ein defer dahinter gehoert damit zum Callback und laeuft bei jedem Aufruf — bei einer Hauptschleife jeden Frame statt einmal am Ende:

use app, s, _dt <- RL.run(app, start)
defer RL.close(app)                                 # warning: defer-in-use-callback

Richtig ist das defer vor dem use; dort laeuft es, wenn RL.run fertig ist.

Zu self-reference-in-initializer: die rechte Seite einer Deklaration laeuft vor dem Binden — eine Referenz auf den eigenen Namen stirbt dort zur Laufzeit mit Variable not defined, sobald der Pfad ausgefuehrt wird:

my q = q + 1                                        # error
val z = if cond then "x" else println("##", z)      # error: z im else-Zweig

Legitime Faelle bleiben frei: Selbstrekursion im Lambda-Body (my fact = |n| -> ... fact(n - 1) — der Body laeuft erst nach dem Binden) und gleichnamige Muster-Bindungen, die den Namen shadowen (val z = match n { z -> z }).

Zu loop-keyword-variable: next, last und redo duerfen auch Variablen- namen sein ([first, ..rest, last], %Emit[data, next]). Ein alleinstehendes next liest dann die Variable, solange eine sichtbar ist, und springt nur sonst. Lexikalisch in einer Schleife ist fast immer der Sprung gemeint:

for x <- xs {
    val next = step(x)
    next                  # warning: liest die Variable, die Schleife springt nicht
}

Als Rueckgabewert eines Funktions- oder Lambda-Rumpfs (val next = s + 1 und dann next) ist das gewollt und wird nicht gemeldet. Funktionen namens last (etwa aus import Antra::Array.*) zaehlen nicht als Variable.

Zu char-range-endpoint: ein Zeichen-Range entsteht aus zwei Strings der Länge 1 ('a'..'z'). Ist ein literaler Endpunkt länger oder leer, stirbt der Range zur Laufzeit mit „must be single characters" — der Checker meldet das schon vorher:

val r = 'ab'..'z'   # warning: character range endpoint 'ab' must be a single-character string
val r = 'a'..'z'    # ok

Gemeldet wird nur, wenn beide Endpunkte String-Literale sind. Variable Endpunkte (lo..hi) und Strings mit Escapes/Interpolation sind zu unsicher und werden ausgelassen.

Zu cross-type-comparison: == wandelt nicht um, ein Vergleich über Typgrenzen ist deshalb einfach false (nur <, > und Co. werfen). Steht auf beiden Seiten ein Literal oder ein val/const-Name, der an ein Literal gebunden ist, kennt der Checker beide Typen und meldet den Vergleich:

val port = 8080
if port == "8080" then println("ok")   # warning: comparing a Number with a String using '==' is always false - convert explicitly with num(...) or str(...)
if str(port) == "8080" then println("ok")   # ok

Unterschieden werden Zahl, String, Keyword und Boolean. undef ist ausgenommen (x == undef ist ein normaler Test), ebenso my-Variablen und Parameter, deren Typ sich ändern kann.

Zu unknown-type-name: Typannotationen mit :- (val s :- String = "a", fn f(x :- Number) :- String -> …) und die rechte Seite eines typedef dürfen nur Namen enthalten, die der Checker kennt:

• die Builtins Number (genauer Int, Rat, Float), String, Bool, Undef, Keyword, Any, Range, Generator, ByteString, Blob, FileHandle, Process, Socket, Regex (ein regex"…"-Literal oder Regex.compile(…).!) sowie Array, Map und Set, die ihre Elementtypen als Argumente nehmen (Map[String, Number]) oder nackt für Any-Elemente stehen
• Typvariablen: ein einzelner Großbuchstabe (T, E); in einem typedef nur dessen deklarierte Parameter
• typedefs der Datei (auch weiter unten oder rekursiv), der importierten Pakete und des Preludes (Result[T, E], Option[T])

val s :- Strng = "a"                  # error: Unknown type name 'Strng'
fn ok(b :- Boolean) -> b              # error: … (the builtin type is 'Bool')
val m :- Map[String] = %{}            # error: 'Map' takes 2 type arguments, got 1
typedef Box[T] = %Box[U]              # error: 'U' is not a parameter of typedef 'Box'
val o :- Option = %None[]             # ok: nackt wie Map, Argumente sind Any

Zu impl-signature-mismatch: die Annotationen einer Protokoll-Deklaration gelten für jedes impl. Eines ohne eigene erbt sie (sein Rumpf wird gegen sie geprüft), eines mit eigenen muss zu ihnen passen:

protocol Measure {
    fn __add__(a, b :- Number) :- Number
}
impl Measure for %Len[..] {
    fn __add__(%Len[a], b :- String) -> a   # error: impl-signature-mismatch
}

Zu clause-annotation-mismatch: die Klauseln einer Funktion mit derselben Stelligkeit sind eine Funktion mit einem Typ; welche Klausel läuft, entscheiden Muster und Guards, nicht die Annotationen. Annotiert werden muss nur eine Klausel (meist die erste); schreibt eine spätere die Annotation noch einmal, muss sie passen. Verschiedene Stelligkeiten haben je einen eigenen Typ:

fn fact(0 :- Int) :- Int -> 1
fn fact(n) -> n * fact(n - 1)                 # ok: fact :- fn(Int) -> Int

fn show(x :- Int) -> str(x)
fn show(x :- String) when x != "" -> x        # error: clause-annotation-mismatch

fn count(xs :- [T]) :- Int -> len(xs)
fn count(xs :- [T], p :- fn(T) -> Bool) :- Int -> len(filter(xs, p))   # ok

Zu export-not-narrower: ein Re-Export darf eine engere Signatur tragen (Array.map nimmt nur Arrays, obwohl Enum.map jede Seq nimmt). Sie muss ein Spezialfall des Originals sein; ihre Typvariablen gelten als fest:

package Ar {
    import Antra::Enum
    export Antra::Enum.{
        map(array :- [T], f :- fn(T) -> U) :- [U],     # ok: [T] ist eine Seq[T]
        filter(x :- Int, f :- fn(Int) -> _) :- [Int]   # error: export-not-narrower
    }
}

Zu annotation-mismatch, rigid-type-variable und union-not-narrowed: eine Annotation ist eine Zusicherung. Die Prüfung ermittelt die Typen der übrigen Stellen selbst (siehe --dump-types) und meldet nur dort, wo ein Wert gegen eine Annotation läuft. Code ohne Annotationen bekommt keine Meldungen, auch wenn sich seine Teile widersprechen.

val s :- String = 5                      # error: expected String, found Int
fn inc(x :- Number) -> x + 1
inc("a")                                 # error: argument 1 of 'inc'
val v :- Number = if c then 1 else "a"   # error am else-Zweig
fn bad(x :- T) :- Number -> x            # error: rigid-type-variable
val maybe :- Number | Undef = undef
val n :- Number = maybe                  # error: union-not-narrowed
val m :- Number = maybe // 0             # ok
val k :- Number = (maybe :- Number)      # ok: die Ascription verengt
fn inc2(n :- Int?) -> n + 1               # warning: possibly-undef
fn inc3(n :- Int?) -> (n // 0) + 1        # ok: // verengt (ebenso defined?)
val r :- %{name :- String, ..} = %{name: "a", age: 3}   # ok: `..` erlaubt weitere
val e :- %{name :- String} = %{name: "a", age: 3}       # error: age ist kein Feld
package Wallet {
    pub field code :- String = 5         # error: default of field 'code'
}

T? ist die Kurzform für T | Undef (String?, [Number]?, (A | B)?); so zeigen auch die Meldungen eine solche Union an. Ein Wert passt zu einer Union, wenn er zu einem Mitglied passt. Ein Record hat genau seine Felder, außer der Typ endet mit ..; optionale Felder (age? :-, oder ein Typ mit Platz für undef wie age :- Number?) dürfen fehlen. Bei if, unless, match und Blöcken geht der erwartete Typ in die Zweige; die Meldung steht dann am Zweig, der nicht passt. Any passt überall.

Eigene Typen kommen aus typedef. Getaggte Mitglieder ergeben einen Summentyp, dessen Konstruktoren typisiert sind: %Ok[1] ist ein Result[Number, _], und in match bekommt %Ok[n] den Typ des Payloads. Andere Mitglieder ergeben einen Union-Typ (typedef Id = Number | String), ein einzelnes einen Alias. Ein Package mit Feldern ist ebenfalls ein Typ: fn total(w :- Wallet) -> w.cents kennt den Feldtyp, und bless(%{…}, Wallet), %Wallet{…} und w.cents = … prüfen annotierte Felder.

typedef Shape = %Circle{r :- Number} | %Rect{w :- Number, h :- Number}

fn area(s :- Shape) :- Number -> match s {
    %Circle{r:} -> r * r * 3
    %Rect{w:, h:} -> w * h
}

fn d(r :- Result[Number, String]) -> match r {   # warning: non-exhaustive-match
    %Ok[n] -> n                                   # (%Err fehlt)
}

fn g(x :- Number | Undef) :- Number -> if defined? x then x else 0   # ok: verengt

Verengt wird in den Armen eines match, mit defined?, undef?, x == undef und den Typ-Prädikaten (string?, number?, …) in if/unless, rechts von &&/|| und nach return … if undef? x. Die Warnung non-exhaustive-match kommt nur, wenn der Typ des geprüften Werts aus einer Annotation stammt.

Auch Pakete bringen Signaturen mit. Ruft dein Code eine annotierte pub fn eines importierten Pakets auf, prüft --check die Argumente, auch wenn dein Code selbst keine einzige Annotation hat. In der Standardbibliothek sind das bisher Antra::String, Antra::Math, Antra::Path, Antra::Regex, Antra::Array, Antra::Result und Antra::Option (generisch, etwa Array.head: fn([T]) -> Option[T]). Keyword-Enums haben Antra::Logger (Level, TimeZone), Antra::Time (Zone, Locale, LocaleKind, DiffUnit, FormatStyle; Time.format nimmt String | FormatStyle), Antra::Duration (DurationUnit) und HTTP.serve (Concurrency); Logger.log(:warning, …) ist damit ein Fehler. Ein typedef eines importierten Pakets heißt in Meldungen qualifiziert (Logger.Level) und kollidiert nicht mit gleichnamigen typedefs der eigenen Datei. Funktionen mit mehreren Stelligkeiten (year(t) und year(t, [zone: …])) werden pro Stelligkeit geprüft:

import Antra::String
import Antra::Path

String.upper(5)                        # error: argument 1 of 'String.upper': expected String, found Number
val p :- String = Path.parent(dir)     # error: union-not-narrowed (Path.parent liefert String?)
val q :- String = Path.parent(dir) // "/"   # ok

Als Vertrag gilt nur, was annotiert ist. Was die Prüfung aus dem Rumpf eines Pakets nur ableitet, wird beim Aufrufer zu Any. Ein undef ohne Annotation ist ein Platzhalter für einen Wert, der später kommt (%{main: undef}), und hat ebenfalls den Typ Any.

Zu annotation-spacing: der Lexer liest :- mit direkt folgenden Namenszeichen als ein Keyword, :-Number ist also das Keyword :-Number. An den Stellen, an denen eine Annotation stehen kann (nach dem Namen einer Deklaration, nach einem Parameter, vor -> und in (e :- T)), kann kein Keyword stehen; dort liest der Parser es trotzdem als Annotation und der Checker warnt:

fn f(x :-Number) -> x          # warning: annotation-spacing
fn f(x :- Number) -> x         # ok
val k = :-Number               # ok: ein Keyword, keine Annotation

Getaggte Typen schreibt man mit % (%Ok[Number]); Ok[Number] ohne % liest der Checker als Anwendung eines typedef namens Ok. Paketqualifizierte Namen (Pkg.Type) bleiben vorerst ungeprüft, und lässt sich ein Import nicht auflösen, schweigt die Prüfung bei unbekannten Namen. Zur Laufzeit haben die Annotationen noch keine Wirkung.

Die Garantie hinter D1: --erase-types#

Mit --erase-types liest --check jede Annotation als Any, auch in importierten Paketen und den Builtin-Signaturen. Dann darf die Typprüfung nichts mehr melden, und alle anderen Diagnosen müssen gleich bleiben. Ein Test (t/186_erase_types_property.t) prüft das über alle Beispiele, die Stdlib und sämtliche Antra-Schnipsel der Tests. Neue Typregeln, die ohne Annotation etwas melden würden, fallen dort auf. Ausgenommen sind die Codes von @types(strict), das bewusst auch unannotierte Konflikte meldet.

antra --check --erase-types programm.ant

Modus strict: @types(strict)#

Ohne Annotation meldet die Typprüfung nichts. Widersprechen sich unannotierte Teile, bekommt die Stelle still den Typ Any. Das Attribut @types(strict) vor einer fn oder einem package macht dort aus diesen stillen Stellen Fehler, ähnlich wie bei ML. Es gilt wie @ignore_warning(...) für das direkt folgende fn oder package, im Package für alle Funktionen darin, und ebenso für Lambdas und verschachtelte Funktionen. @types(gradual) öffnet darin eine einzelne Funktion wieder:

@types(strict)
fn f(x) -> x(x)                    # error: type-conflict (unendlicher Typ)

@types(strict)
fn pick(c) -> if c then 1 else "a" # error: type-conflict

@types(strict)
fn name(p) -> p.name               # error: field-of-unknown-type

@types(strict)
fn name2(p :- %{name :- String}) -> p.name   # ok

@types(strict)
package Money {
    pub fn add(a :- Number, b :- Number) :- Number -> a + b
    @types(gradual)
    pub fn legacy() -> [1, "a"]    # ok: gradual
}

Wer in strict eine Stelle bewusst dynamisch halten will, schreibt :- Any; # ignore: type-conflict stummt eine Zeile. Ein gemischtes Array-Literal (["dd.MM.yyyy", false]) ist kein Konflikt, sondern ein Tupel (siehe unten). Da es keine Row-Typen gibt, brauchen Zweige, die Records verschiedener Breite liefern, eine Annotation, ebenso Klauseln mit verschiedenen Tags ohne gemeinsamen typedef. Verengte match-Arme, die wieder zur Summe werden (%Ok[_] -> r, %Err[e] -> %Err[e]), sind kein Konflikt. Was die Prüfung grundsätzlich nicht versteht (Builtins, Protokollaufrufe), bleibt auch in strict Any. Zur Laufzeit hat der Modus keine Wirkung; dafür gibt es @types(runtime) und antra --check-types, die jede Annotation beim Ausführen prüfen (Kapitel 16).

Builtins#

Auch die Builtins haben Signaturen (src/check/builtins.ant, ein @extern-Package, siehe unten). Ihre Ergebnistypen fließen in die Inferenz: len(…) ist Number, str(…) String, split(…) [String], map([1, 2], |x| -> x + 1) [Int]. Geprüft werden nur Parameter mit geschlossenem Wertebereich, dafür auch in unannotiertem Code:

split(5, ",")        # error: argument 1 of 'split': expected String, found Number
split("a b", 5)      # error: expected String | Regex
keyword(5)           # error: expected String
len(%Ok[1])          # ok: len nimmt vieles, nur das Ergebnis ist typisiert

map, filter, grep, take und collect nehmen ein Seq[T]: was sich elementweise durchlaufen lässt. Ein Array [T] liefert T, eine Range Zahlen, ein String seine Zeichen, eine Map ihre Werte, ein Generator[T] seine Elemente. So kommt der Elementtyp im Callback an, auch bei Feldzugriffen:

fn prices(items :- [%{price :- Number}]) -> map(items, |it| -> it.price)
# fn([%{price :- Number}]) -> [Number]; im Callback ist it ein %{price :- Number}
map(5, |x| -> x)     # error: expected Seq[_], found Number

Was zur Laufzeit nicht durchlaufbar ist (Zahl, Bool, Keyword, Set, getaggter Wert), passt nicht. Unbekanntes und Gemischtes (ein unannotierter Parameter, [1, "a"]) passt still. Seq[T] ist kein Typ eines Werts, sondern nur eine Erwartung, und kann auch in eigenen Annotationen stehen (fn sum(xs :- Seq[Number])); for x <- xs bindet dann x als Number.

Generatoren haben den Typ Generator[T]. Ein gen fn liefert ihn mit T aus seinen yields, select (...) yield expr mit dem Typ von expr; next(g) ergibt Option[T], collect(g) [T]. Widersprechen sich die yields, ist T still Any. Mit annotiertem Ergebnis wird jedes yield geprüft:

gen fn nums(n) -> { … yield i … }   # fn(Number) -> Generator[Number]
gen fn names() :- Generator[String] -> {
    yield 5                         # error: expected String, found Number
}

Ein nacktes Generator (ohne Argument) steht für Generator[Any].

Eine eigene Funktion gleichen Namens verdeckt das Builtin samt Signatur. Typprädikate (string?(x), …) verengen weiter, solange sie nicht verdeckt sind.

Arrays, Tupel und getaggte Werte#

[Number] (lang [..Number], auch Array[Number]) ist ein Array, [String, Bool] ein Tupel, [Number,] ein Tupel mit genau einem Element, [String, ..Number] ein Tupel mit Rest. Getaggt zählen die Positionen: %Some[Number] ist genau ein Element, %Pts[..Number] beliebig viele. Die Regeln mit Tabelle und den typischen Verwechslungen stehen in Kapitel 16. Für die Prüfung wichtig: Ein Literal ohne gemeinsamen Elementtyp ist ein Tupel (["a", false] ist [String, Bool]), ein Tupel passt auf ein Array, wenn jedes Element passt, ein Array auf ein Tupel ohne Rest nie. t[0] und t[-1] mit literalem Index liefern den Typ der Position.

Enums: Keyword-Literaltypen und Tags#

Ein Keyword kann selbst ein Typ sein: :debug steht für genau dieses Keyword. Eine Union daraus ist ein Enum:

typedef Level = :debug | :info | :warn

fn label(l :- Level) :- String -> match l {   # warning: non-exhaustive-match (:warn fehlt)
    :debug -> "D"
    :info  -> "I"
}
val a :- Level = :info          # ok
val b :- Level = :inf           # error: annotation-mismatch (expected Level, found :inf)
fn lv(x :- :on | :off) -> x     # auch direkt an einer Annotation

Geprüft wird ein Keyword-Literal nur dort, wo ein Keyword-Literaltyp erwartet wird. Ein Keyword aus unannotiertem Code passt still zu jedem Enum, und ein Enum-Wert passt überall, wo Keyword erwartet wird. Wer Werte mit Daten braucht, nimmt Tags: typedef Shape = %Circle[Number] | %Square[Number] (oder ohne Payload %Red[] | %Green[]) wird genauso auf Vollständigkeit geprüft. Zur Laufzeit gibt es keine Liste der Enum-Werte; der typedef ist rein statisch.

Keyword-Arrays: [fill :- String, width :- Number?]#

Optionen und [k: v]-Literale haben einen eigenen Typ. Ein Typ mit Platz für undef (T?) macht einen Schlüssel optional, ein abschließendes .. erlaubt weitere, [..] ist ein beliebiges Keyword-Array. Ein ? am Namen gehört zum Schlüssel ([strict? :- Bool] ist die Option strict?):

fn pad(w, s, [fill: = " ", width: = 0]) -> fill   # fn(T, U, [fill :- String?, width :- Int?]) -> String
val a = pad(1, "a", fill: "0")                    # ok
val b = pad(1, "a")                               # ok: alle Optionen haben Defaults

fn opt(x, [fill: = " "] :- [fill :- String?]) -> fill
opt(1, fill: 5)                       # error: annotation-mismatch (fill ist String)
opt(1, fil: "x")                      # error: unknown-keyword-arg

fn plain(o :- [fill :- String?]) -> o
plain([fil: "x"])                     # error: annotation-mismatch (unbekannter Schlüssel)

Ein Optionsparameter bekommt seinen Typ aus dem Pattern. Ein Schlüssel mit Default ist optional, ein Rest (.., ..rest) macht den Typ offen. Ein unbekannter Schlüssel an einem Optionsparameter meldet die Keyword-Prüfung, an einem annotierten gewöhnlichen Parameter die Typprüfung. [] passt als leere Optionsliste.

Kürzer schreibt man den Typ direkt an den Eintrag, wie bei einem Parameter (x :- T = default):

fn pad(w, [fill :- String = " ", width :- Number = 0, d: dd :- Number = 7, ..]) -> …
#          Kurzform: Schlüssel fill bindet fill    Langform: Schlüssel d bindet dd

Ein Eintrag mit Typ macht den Parameter zu einem annotierten: Aufrufer werden geprüft, und der Default muss zum Typ passen ([fill :- String = 5] ist ein Fehler). Einträge ohne Typ daneben sind Any. Haben Klauseln verschiedene Schlüssel, ist nur ein Schlüssel Pflicht, den jede Klausel ohne Default nimmt.

Aufrufe importierter Funktionen#

Die Arity- und Keyword-Prüfungen gelten nicht nur für lokale Funktionen, sondern auch für importierte. Rufst du Array.drop([1, 2, 3]) mit einem Argument auf, obwohl Antra::Array es als pub fn drop(array, n) definiert, meldet der Checker arity-mismatch — schon vor dem Ausführen:

import Antra::Array as Array
Array.drop([1, 2, 3])        # arity-mismatch: erwartet 2 Argumente

import Antra::Bytes.{from_file}
from_file()                  # arity-mismatch, falls die Signatur ein Argument verlangt

Der Checker löst dazu das importierte Paket über denselben Suchpfad wie die Laufzeit zu seiner .ant-Datei auf und liest deren pub fn-Signaturen. Das gilt für aliasierte Methodenaufrufe (Alias.method(...)) und für selektiv importierte Namen (import Pkg.{fn} + fn(...)). Pipe-Aufrufe zählen das durchgereichte Argument korrekt mit (xs |> Array.drop(1) = zwei Argumente).

Re-exportierte Funktionen (export Other.{...}) werden mitgeprüft: der Checker folgt dem Export zur Quell-.ant und übernimmt deren Signatur (so wird z. B. Array.reduce gegen die Definition in Antra::Enum geprüft).

Multi-clause-Funktionen (mehrere fn-Klauseln gleichen Namens, auch re-exportiert wie Array.count) werden konservativ geprüft: gemeldet wird nur, wenn keine Klausel die Argumentzahl akzeptieren kann — dann stirbt der Aufruf zur Laufzeit ohnehin mit „no matching clause". Jede Klausel trägt einen Bereich [min, max] bei (Obergrenze offen bei trailing ..rest); ein Aufruf ist gültig, sobald er in irgendeinen Bereich passt.

fn count(seq) -> ...
fn count(seq, pred) -> ...

count()            # arity-mismatch: erwartet 1 oder 2
count([1, 2, 3])   # ok

Ein Default-Parameter macht die Arity nur dann variabel, wenn er wirklich weggelassen werden kann. Steht hinter einem optionalen Parameter noch ein Pflicht-Parameter, muss der optionale gefüllt werden (sonst bliebe der spätere Pflicht-Slot ohne Argument) — die Arity ist dann wieder fest. Das gilt auch für eine Pflicht-Keyword-Array als letzten Parameter:

fn zz(x = 1, [a: , b: = x * 10] as opts) -> opts

zz(2)             # arity-mismatch: das Keyword-Array (a: ist Pflicht) fehlt
zz(2, [a: 3])     # ok

Ausgenommen bleibt eine Keyword-Array, deren Keys alle Defaults haben: sie darf als letzter Parameter (oder vor einem Callback/..rest) weggelassen werden und hält die Arity variabel.

Passt die Argumentzahl, aber die Keyword-Argumente in keine Klausel, meldet der Checker no-matching-clause. Das greift nur, wenn alle Klauseln dieselbe Parameterzahl haben, keine einen trailing ..rest trägt und jede ein geschlossenes Keyword-Pattern hat — dann ist ein Aufruf mit einem literalen Keyword-Array, das in keine Klausel passt (fremder Key oder fehlender Pflicht-Key überall), zur Laufzeit ein garantiertes „No matching clause".

fn zz([a: , b: = 3] as o) -> o
fn zz([x: , b: = 3] as o) -> o

zz([u: 2, b: 3])   # no-matching-clause: weder a: noch x:
zz([a: 1])         # ok (Klausel 1 matcht, b: hat Default)

Passt die Argumentzahl dagegen auf genau eine Klausel, ist die Positionszuordnung eindeutig — dann meldet der Checker statt der vagen no-matching-clause den präzisen Keyword-Befund dieser Klausel (unknown-keyword-arg / missing-keyword-arg), inklusive der Liste der erlaubten Keys. Das ist der häufige Fall von Options-Funktionen mit einer (wert)- und einer (wert, [opts])-Klausel (z. B. Console.ask).

fn m([x:]) -> x
fn m(a, b) -> a

m(y: 1)   # unknown-keyword-arg 'y:' (+ missing 'x:') — nur m([x:]) hat arity 1

Ein Nicht-Keyword-Mismatch (Tag, Länge, Skalar-Wert) bleibt dagegen bei no-matching-clause, ebenso mehrere arity-passende Klauseln (dann ist unklar, welche gemeint war).

Trägt ein Keyword-Key ein Wert-Sub-Pattern (Array, Map, Set, Tagged Value oder Skalar-Literal statt eines Bindings), wird der übergebene Wert für diesen Key rekursiv gegen das Sub-Pattern geprüft — mit denselben Codes wie bei gewöhnlichen Parametern (type-mismatch, literal-mismatch, array-length-mismatch, unknown-map-key/missing-map-key). Im Multi-Clause- Fall greift auch hier no-matching-clause, wenn kein Wert eine Klausel matchen kann.

fn zz([a: , b: [1, 2]] as o) -> o

zz([a: 2, b: []])      # array-length-mismatch: b erwartet genau 2 Elemente
zz([a: 2, b: 1])       # type-mismatch: b erwartet ein Array
zz([a: 2, b: [1, 2]])  # ok

Dieselbe Prüfung gilt für Map-Patterns %{...} als Parameter — auch sie sind ohne .. exakt (ein fremder Key oder ein fehlender Pflicht-Key ist ein No-Match). Ein literales Map-Argument wird gegen das geschlossene Map-Pattern geprüft (unknown-map-key / missing-map-key), und im Multi-Clause-Fall gilt wieder no-matching-clause.

fn f(%{c:, d:}) -> c

f(%{c: 1})            # missing-map-key: d fehlt
f(%{c: 1, d: 2, e: 3}) # unknown-map-key: e
f(%{c: 1, d: 2})      # ok

Für Tagged-Map-Patterns (%Person{...}) gelten dieselben Key-Checks, plus ein strikter Tag-Abgleich in beide Richtungen (wie bei Array-/Set-Patterns und im Laufzeit-Matcher): Ein %Person{...}-Pattern verlangt eine Map mit genau diesem Tag, und ein untagged %{...}-Pattern lehnt eine getaggte Map ab. Jede Tag-Abweichung ist ein tag-mismatch.

fn f(%Person{name:, age:}) -> name

f(%Person{name: "x"})              # missing-map-key: age
f(%Other{name: "x", age: 1})       # tag-mismatch: %Other statt %Person
f(%{name: "x", age: 1})            # tag-mismatch: untagged Map, erwartet %Person
f(%Person{name: "x", age: 1})      # ok

Tagged Scalars und Tagged Strings (10min, tag"sss") werden als skalare Literale behandelt — wertgleiche Schreibweisen gelten als gleich (10min == %min[10], tag"sss" == %tag["sss"]), und ein abweichender Wert oder Tag ist ein literal-mismatch. Die Meldung zeigt beide Seiten in derselben Notation, damit klar wird: gleiche Art, nur anderer Wert.

fn f(%min[10]) -> 1

f(11min)   # literal-mismatch: passes %min[11], but expects %min[10]
f(10sec)   # literal-mismatch: passes %sec[10], but expects %min[10]
f(10min)   # ok (wertgleich zu %min[10])

Die Prüfung ist rekursiv: Ist der Wert eines Feldes selbst ein geschlossenes Map-Pattern (address: %{ street: }), wird das übergebene Map-Literal an dieser Stelle eine Ebene tiefer gegen dasselbe Regelwerk (Tag, Keys) geprüft. Offene verschachtelte Patterns (%{ street:, .. }) und andere Formen (z. B. Array-Patterns) bleiben konservativ ausgespart.

fn f(%Person{ name:, address: %{ street: } }) -> name

f(%Person{ name: "x", address: %{ street: "E", hn: 1 } })  # unknown-map-key: hn (geschachtelt)
f(%Person{ name: "x", address: %{ street: "E" } })         # ok

Dieselbe rekursive Logik gilt für Skalar-Literale, Array- und Set-Patterns sowie deren Tagged-Varianten (%Ok[...], %S<...>) — jeweils nur bei literalen Argumenten und einem garantierten No-Match. Zahlen werden numerisch verglichen (10 == 10.0), Strings wertgleich (Quote-Stil egal); ein Binding-Parameter akzeptiert weiterhin alles. Passt schon die Form des Arguments nicht zum Pattern (z. B. ein String an ein Array-Pattern, ein Set an ein Map-Pattern), meldet der Checker type-mismatch. Die Diagnose markiert das fehlerhafte Argument selbst (die beim Parsen erfasste Argument-Position), und der Meldungstext nennt den Pfad (z. B. „argument 2 array element 1", „… field 'addr'").

fn f(a, [1, 2, ..], %<:a, :b>, "sss") -> a

f(0, [9, 2], %<:a>, "x")
#      ^^^^^ literal-mismatch: array element 1 passes 9, but expects 1
#            ^^^^^ missing-set-member: :b
#                   ^^^ literal-mismatch: passes "x", but expects "sss"

Bewusst nicht geprüft werden — mangels eindeutiger statischer Signatur:

• rein native Pakete (Antra::Native::* ohne .ant)
• multi-clause Funktionen mit on_use-Parametern (Keyword-Aufrufkonvention macht die Argumentzahl unbestimmt)

Die Prüfung ist bewusst konservativ: Im Zweifel schweigt sie lieber, als gültigen Code fälschlich zu melden.

Der Editor kennt zusätzlich unknown-member — die rote Markierung bei Pkg.tippfehler, wenn Pkg zwar existiert, der Member aber nicht. Diesen Check macht die VS-Code-Erweiterung; auf der Kommandozeile fällt derselbe Fall erst zur Laufzeit auf (siehe Kapitel 13, Abschnitt Package-Variablen).

Warnungen bewusst stummschalten#

Manchmal ist eine Warnung falsch für deinen Fall — ein Parameter erfüllt einen Interface-Vertrag, eine Bindung ist absichtlich da, ein Name wird dynamisch aufgelöst. Dann willst du gezielt stummschalten, nicht die ganze Prüfung abschalten.

Es gibt drei Granularitäten, alle mit demselben Code-Vokabular aus der Tabelle oben.

_-Präfix — die einfachste Stummschaltung für „unused"#

Für ungenutzte Bindungen und Parameter reicht ein Unterstrich vorne. Das signalisiert auch dem Leser „bewusst ungenutzt":

fn handler(req, _ctx) -> handle(req)   # _ctx bewusst ignoriert

Das wirkt nur auf die unused-*-Warnungen.

# ignore: — eine einzelne Zeile#

Für alles andere (oder wenn dir _ nicht passt) schreibst du ein Pragma ans Zeilenende:

my scratch = compute()        # ignore: unused-variable
Plugins.late_bound            # ignore: unknown-member

Mehrere Codes trennst du mit Komma:

risky_call()                  # ignore: unknown-call, unreachable-code

Ein nacktes # ignore (ohne Doppelpunkt) bzw. # ignore: all oder # ignore: * schaltet alle Codes dieser Zeile stumm:

Experimental.thing            # ignore

Das Pragma wirkt exakt auf die Zeile, auf der es steht — nicht auf die nächste, nicht auf den Block.

@ignore_warning(...) — eine Funktion oder ein Package#

Wenn eine ganze Funktion oder ein ganzes Package eine bestimmte Warnung nicht bekommen soll, setzt du das Attribut direkt davor. Es wirkt für den gesamten Bereich des annotierten Knotens:

@ignore_warning(unused-parameter)
pub fn on_event(event, context) -> log(event)   # context Teil des Vertrags

Auch mehrere Codes sind erlaubt:

@ignore_warning(unused-parameter, unused-variable)
fn scaffold(a, b) -> {
    my todo = "später"
    nil
}

Das Attribut kann an fn, gen, pub und package stehen. Es leakt nicht auf Nachbarknoten — eine zweite Funktion daneben wird wieder normal geprüft.

Welche Ebene wann?#

Als Faustregel: so eng wie möglich. Ein # ignore: auf genau der Zeile ist ehrlicher als ein Attribut über der ganzen Funktion, weil es beim nächsten Leser keine anderen echten Warnungen mitverschluckt.

@dynamic — Pakete mit Laufzeit-Membern#

Standardmäßig ist ein Zugriff auf einen unbekannten Package-Member ein Fehler — zur Laufzeit ein throw, im Editor eine rote Markierung. Das fängt Tippfehler früh.

Manche Pakete füllen ihre Member aber absichtlich erst zur Laufzeit (etwa eine Plugin-Registry oder generierte Zugriffe per Metaprogrammierung). Für die wäre der strikte Check ein Dauer-Fehlalarm. Markiere solche Pakete mit @dynamic:

@dynamic
package Plugins {
    pub our registry = %{}
}

Plugins.registry              # bekannter Member: normal
Plugins.late_bound            # unbekannt, aber @dynamic → undef statt Fehler

Für ein @dynamic-Package gilt:

• Laufzeit: ein unbekannter Member wirft nicht, sondern liefert undef.
• Editor: die statische „No member"-Markierung entfällt für dieses Package.

Damit bleibt die strikte Prüfung der Normalfall (fängt Tippfehler), und dynamische Pakete kennzeichnen sich selbst als bewusste Ausnahme.

Für einen einzelnen unsicheren Zugriff musst du nicht gleich das ganze Package öffnen. Der Safe-Access-Operator Pkg?.member liefert undef ohne Fehler, und Meta.get_subject(Pkg, "name") fragt einen Member ab, ohne zu werfen.

@extern — Deklarationen ohne Rumpf#

Ein Package mit @extern darf Funktionen nur deklarieren: Signatur ohne -> und Rumpf, wie eine Protokoll-Methode. So bekommen Funktionen, die nativ implementiert sind, Typen für --check:

@extern
package Builtins {
    pub fn len(x) :- Number
    pub fn split(s :- String, sep :- String | Regex) :- [String]
    pub fn split(s :- String, sep :- String | Regex, n :- Number) :- [String]
    pub fn upper(x :- T) :- T
}

Eine Deklaration ohne Rückgabetyp liefert Any. Mehrere Stelligkeiten, Typvariablen und Keyword-Optionen gehen wie bei normalen Funktionen, ein when-Guard nicht. Normale Funktionen mit Rumpf dürfen daneben stehen. Ruft man eine Deklaration zur Laufzeit auf, wirft sie ('len' is only declared (@extern); it is implemented natively). Außerhalb von @extern bleibt ein fehlender Rumpf ein Parse-Fehler, ein vergessenes -> wird also nicht still zur Deklaration. unused-parameter gilt für Deklarationen nicht.

Dieselbe Form tragen die nativen Module: lib/Antra/Native/String.ant, FS.ant usw. deklarieren Antra::Native::String & Co. Der Checker liest diese Dateien, zur Laufzeit läuft weiter das Zig-Modul. Erzeugt werden sie aus den annotierten Wrappern der Stdlib:

python3 tools/gen_native_decls.py           # zeigen, was entstuende
python3 tools/gen_native_decls.py --write   # schreiben
python3 tools/gen_native_decls.py --check   # Exit 1, wenn veraltet

Ein Wrapper zählt, wenn er in einer Zeile annotiert an das native Modul durchreicht (pub fn exists(path :- String) :- Bool -> N.exists(path)). Von Hand geschriebene Deklarationen stehen unter der Zeile # -- hand-written below und bleiben beim Neuschreiben erhalten. Gegen @extern-Packages prüft der Checker keine Stelligkeit, denn native Funktionen nehmen fehlende Argumente als undef.

Strategie: strikt lassen, gezielt öffnen#

Die statische Prüfung ist am wertvollsten, wenn sie laut ist. Deshalb:

• Lass die Prüfung in CI mitlaufen (antra --check), damit Fehler nicht durchrutschen.
• Schalte einzelne Warnungen bewusst und so eng wie möglich stumm, statt Codes pauschal zu ignorieren.
• Nutze @dynamic nur für Pakete, die wirklich zur Laufzeit wachsen — nicht als bequeme Abkürzung, um Tippfehler zu verstecken.

So bleibt der Normalfall streng, und jede Ausnahme steht sichtbar und begründet im Code.

Quelle dieser Seite