Struktur und Typen

Typannotationen

Antra ist dynamisch: ein Programm läuft ohne eine einzige Typangabe. Du kannst aber Typen dazuschreiben, wo sie dir helfen, mit :-:

fn area(w :- Number, h :- Number) :- Number -> w * h

Diese Annotationen prüft antra --check, bevor das Programm läuft. Zur Laufzeit haben sie normalerweise keine Wirkung; auf Wunsch prüft antra --check-types sie auch beim Ausführen (siehe unten). Der Perl-Interpreter (antra-lang) liest sie und ignoriert sie. Der Rest des Codes muss nichts davon wissen: Typen sind graduell. Du annotierst eine Funktion, ein Feld oder einen Wert, und nur dort entsteht eine Pflicht.

Dieses Kapitel zeigt, wie man Typen schreibt und was sie bewirken. Die einzelnen Meldungen und wie man sie stummschaltet, beschreibt Kapitel 17.

Kurz: ein Beispiel#

typedef Shape = %Circle[Number] | %Rect[Number, Number]

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

val total :- Number = area(%Circle[2]) + area(%Rect[2, 3])
println(total)

area(%Square[4])                 # error: %Square passt nicht auf Shape
val name :- String = area(%Rect[1, 1])   # error: expected String, found Number

antra --check datei.ant meldet die beiden letzten Zeilen, bevor irgendetwas läuft. Ohne --check laufen sie wie gewohnt und scheitern erst zur Laufzeit.

Was eine Annotation bewirkt#

Drei Regeln reichen fürs Verständnis:

1. Nur Annotationen erzeugen Meldungen. Code ohne Typen bleibt still, auch wenn sich seine Teile widersprechen. Was nicht zusammenpasst, wird still zu Any.
2. Den Rest leitet die Prüfung selbst ab. val n = len(xs) ist ein Int, map(xs, |x| -> x + 1) mit xs :- [Int] ein [Int]. Diese abgeleiteten Typen werden gegen deine Annotationen geprüft.
3. Eine Annotation ist eine Zusicherung. Ein Wert muss zu ihr passen, und danach gilt an dieser Stelle genau der annotierte Typ.

fn untyped(a, b) -> a + b        # ohne Typen: keine Meldung, auch nicht bei untyped("x", 1)
fn typed(a :- Number) -> a + 1
typed("x")                       # error: argument 1 of 'typed': expected Number, found String

Welche Typen die Prüfung ableitet, zeigt antra --dump-types datei.ant. In VS Code (mit antra-zig) zeigt der Hover über einer Variablen ihren Typ, etwa prices :- [Number], und über einer Funktion ihre Signatur.

Zur Laufzeit ändern Annotationen nichts, solange du sie nicht ausdrücklich prüfen lässt (--check-types). Die Ausnahme sind Typen mit Bedingung (where): die gelten immer. Nur beim nativen Bau mit antra build --native --optimize legen Int-, Float-, Bool-, String- und Rat-Signaturen fest, mit welchen Typen reine Rechenfunktionen übersetzt werden; ohne Annotation nimmt der Übersetzer Typen an (Nativ bauen).

Wo Annotationen stehen#

Schreib :- immer mit Leerzeichen dahinter: :-Number ist eigentlich ein Keyword-Literal. An Annotationsstellen versteht der Parser es trotzdem, warnt aber (annotation-spacing).

Was wann geprüft wird#

Eine Annotation wird an drei Stellen wirksam:

• --check (und VS Code) prüft vor dem Lauf, was sich ohne Ausführen sagen lässt: Literale und Werte, deren Typ aus anderen Annotationen folgt.
• Zur Laufzeit prüft ein gewöhnlicher Typ (Int, [String], %{x :- Int}) nur mit antra --check-types oder unter @types(runtime).
• Ein Typ mit Bedingung (where, 0..100, in [...], "a" | "b") wird zur Laufzeit immer geprüft, auch in Arrays, Records und T?. Dann prüft die Laufzeit die ganze Annotation: bei %{x :- Age, name :- String} auch, dass name ein String ist.

Ein Wert, der erst zur Laufzeit entsteht (f(n) mit einem n aus einer Eingabe), ist statisch unbekannt; dort bleibt nur die Laufzeitprüfung. Mit --check --erase-types gelten alle Annotationen als Any, dann meldet --check auch keine Bedingungen; zur Laufzeit gelten sie weiter.

Die Typen im Überblick#

Zahlen: Int, Rat und Float#

Zur Laufzeit hat jede Zahl eine Art: eine ganze Zahl (Int, beliebig groß), ein Bruch (Rat) oder eine Fließkommazahl (Float). Die Art hängt davon ab, woher die Zahl kommt, nicht von ihrem Wert (Kapitel 5). Number steht für alle drei; Int, Rat und Float sind genauere Typen darunter.

Die Prüfung leitet die Art ab, wo sie feststeht:

Treffen zwei Arten ohne Annotation aufeinander, wird die Stelle still zur Number:

my x = 1        # Int
x = x / 2       # jetzt Number: mal Int, mal Rat

Geprüft wird wie überall nur gegen Annotationen. Ein Int passt auf Number, und eine Number, deren Art unbekannt ist, passt still auf Int. Gemeldet wird, wenn die Art feststeht und eine andere ist:

fn half(n :- Int) -> n / 2
half(3)                    # ok
half(1.5)                  # error: expected Int, found Rat (convert with int(...) or Math.round(...))
val r :- Float = 1         # error: expected Float, found Int (convert with float(...))

Eine Number unbekannter Art ist dagegen nachsichtig: sie nimmt die Art an, die eine Annotation verlangt, und wird nicht gemeldet. Das betrifft vor allem 2 ** n mit einem Exponenten, dessen Vorzeichen die Prüfung nicht kennt:

fn pow2(n :- Int) :- Int -> 2 ** n     # still: die Art passt sich an
pow2(3)                                # 8
pow2(-1)                               # 0.5, ein Rat: falsch, aber erst zur Laufzeit sichtbar

Die Prüfung meldet also nur, was sicher falsch ist, nicht, was falsch sein kann. Wer pow2(-1) ausschließen will, sagt es im Typ, etwa mit typedef Nat = 0..* und n :- Nat (dann ist pow2(-1) ein --check-Fehler und zur Laufzeit immer einer), oder macht das Ergebnis mit Math.floor(…) ausdrücklich ganz. Mit --check-types meldet die Laufzeit the result of 'pow2' must be Int.

Eine ganze Zahl ist hier also kein Float und kein Rat: float?(1) ist zur Laufzeit false, und die Annotation sagt dasselbe. int?(x), rat?(x) und float?(x) verengen eine Number (oder eine Union wie Number | String):

import Antra::Math

fn whole(n :- Number) :- Int -> if int?(n) then n else Math.floor(n)

Arrays, Tupel und getaggte Werte#

Ein Array von Zahlen ist [Number], wie in den meisten Sprachen. Steht mehr als ein Typ in den Klammern, zählen die Positionen, genau wie beim Wert: [String, Bool] ist ein Paar. ..T heißt „beliebig viele T“, dasselbe .. wie im Pattern [first, ..rest]:

[Number] und Array[Number] sind Langformen von [Number], derselbe Typ. Ein Tupel sieht aus wie sein Wert: ["a", false] hat den Typ [String, Bool], %Rect[2, 3] den Typ %Rect[Number, Number]. Zur Laufzeit ist ein Tupel ein gewöhnliches Array.

fn preset(kind) :- [String, Bool] -> if kind == :date then ["dd.MM.yyyy", false] else ["HH:mm", true]
fn names(s :- String) :- [String] -> split(s, ",")
fn total(p :- %Pts[..Number]) -> p

val [fmt, flag] = preset(:date)      # fmt: String, flag: Bool
val p :- [Number, Number] = [1, 2]   # ok
val q :- [Number, Number] = [1]      # error: Länge passt nicht
val xs :- [String] = ["a", 1]        # error: [String, Int] passt nicht auf [String]
val t = total(%Pts[1, 2, 3])         # ok
println([fmt, flag, p, t, names("a,b")])

Ungetaggt und getaggt zählen verschieden: [Number] ist ein Array, %Some[Number] dagegen genau ein Wert. Ein getaggter Wert hat feste Positionen wie ein Konstruktor; ein getaggtes Array schreibt man mit Rest, %Pts[..Number]. Das seltene ungetaggte Tupel mit einem Element bekommt ein Komma, [Number,], wie in Python. Wer es vergisst, bekommt eine Meldung mit Hinweis:

val one :- [Number,] = [1, 2, 3]     # error: … ('[Number,]' is exactly one element; an array is '[Number]')

Runde Klammern gruppieren nur: (Number | String) braucht man etwa in Lambda-Parametern; in eckigen Klammern geht es ohne, [Number | String] ist ein Array gemischter Werte.

Ohne Annotation ist ein Literal ein Array, wenn seine Elemente einen gemeinsamen Typ haben, sonst ein Tupel: [1, 2] ist [Int], ["a", false] ist [String, Bool]. Ein Tupel passt auf ein Array, wenn jedes Element passt. Ein Array passt auf ein Tupel mit Rest, wenn sein Element zu allen Teilen passt ([Any] passt also still), auf eines ohne Rest nie, weil seine Länge unbekannt ist.

map, filter, take, collect, for und die Funktionen von Antra::Enum nehmen ein Seq[T]: ein Array liefert seine Elemente, eine Range[T] ihre Werte ('a'..'c' Strings), ein String seine Zeichen, eine Map ihre Werte, ein Set seine Elemente, ein Keyword-Array seine Paare [Keyword, V], ein Generator[T] seine Elemente. Getaggte Maps und Sets laufen wie ungetaggte; ein getaggtes Array (%Ok[v], %Pair[a, b]) nur mit impl Enumerable (sein Elementtyp ist dann unbekannt), sonst ist es kein Seq. So kommt der Elementtyp auch im Callback an:

fn prices(items :- [%{price :- Number}]) -> map(items, |it| -> it.price)   # fn(...) -> [Number]

gen fn countdown(n :- Number) -> {
    my i = n
    while (i > 0) {
        yield i
        i = i - 1
    }
}
for k <- countdown(3) { println(k) }     # k: Number
map(5, |x| -> x)                         # error: expected Seq[_], found Number

Records, Maps und Keyword-Arrays#

Eine Map mit bekannten Feldern ist ein Record. Er ist exakt wie ein Map-Pattern: weitere Felder sind ein Fehler, außer der Typ endet mit .. (%{name :- String, ..}, %Vec{..} für beliebige Felder). Ein Feld, dessen Typ undef zulässt (age :- Number?), darf fehlen: ein fehlender Schlüssel liest sich als undef. Wie überall gilt: : gibt einen Wert (%{age: 36}), :- einen Typ (%{age :- Number}). Die Form %{age: Number} im Typ geht ebenfalls; antra zeigt Typen in Meldungen und im Hover mit :-.

Ein ? am Namen gehört zum Schlüssel, wie bei jedem Namen in Antra: %{ready? :- Bool} ist das Feld ready? (%{ready?: true}), nicht ein optionales ready. Optional ist ein Feld nur über seinen Typ:

fn greet(p :- %{name :- String, age :- Number?}) -> "Hi " <> p.name
greet(%{name: "Ada"})                   # ok: age darf fehlen
greet(%{name: "Ada", city: "London"})   # error: city ist kein Feld
greet(%{name: 5})                       # error: name ist kein String
fn hello(p :- %{name :- String, ..}) -> "Hi " <> p.name
hello(%{name: "Ada", city: "London"})   # ok: `..` erlaubt weitere Felder
val ages :- Map[String, Number] = %{ada: 36, alan: 41}
println(ages)

Ein Record passt auf Map[K, V], wenn alle Werte zu V passen. Ist V noch offen (fn keys(m :- Map[K, V])) und haben die Werte verschiedene Typen (%{name: "Ada", age: 36}), wird V zu Any: bei einem Record ist das der Normalfall, anders als bei einem gemischten Array, dessen Elementtyp eine Union wird. Den Schlüsseltyp legt ein Record nicht fest (%{a: 1} hat Keyword-, %{"a" => 1} String-Schlüssel). Eine getaggte Map passt ebenso auf Map[K, V] (eine Map mit Etikett), umgekehrt passt eine ungetaggte Map nicht auf %Cfg{…}; dasselbe gilt für getaggte Sets und Set[T].

Optionen am Ende einer Parameterliste sind Keyword-Arrays. Ihr Typ steht direkt am Eintrag:

Eine Option mit Default ist optional; ihr Typ zeigt das als T? (pad :- fn(String, [fill :- String?, width :- Number?]) -> String). Als Typ eines Parameters geschrieben ist es dieselbe Regel wie bei Records: [width :- Number?] darf fehlen, [strict? :- Bool] ist die Option strict?.

fn pad(s :- String, [fill :- String = " ", width :- Number = 8]) -> s
pad("a", fill: "-")       # ok
pad("a", width: "8")      # error: width ist keine Number
pad("a", filler: "-")     # error: unbekannte Option

Achtung: [fill: String] im Parameter bindet eine Variable namens String. Der Typ gehört hinter :-.

Eigene Typen: typedef#

typedef gibt einem Typ einen Namen. Je nach Mitgliedern entsteht etwas anderes:

typedef Shape  = %Circle[Number] | %Rect[Number, Number]   # Summentyp: nur Tags
typedef Id     = Number | String                           # Union
typedef Level  = :debug | :info | :warn                    # Enum aus Keywords
typedef Pair[A, B] = [A, B]                                # mit Parametern

fn log(l :- Level, msg) -> println(msg)
log(:info, "ok")
log(:inf, "tippfehler")        # error: :inf ist kein Level
val p :- Pair[String, Number] = ["a", 1]
println(p)

Ein Summentyp ist mehr als eine Union: Ein %Circle[2] gehört zu Shape, und in match kennt %Circle[r] den Typ von r. Option[T] (%Some[T] | %None[]) und Result[T, E] (%Ok[T] | %Err[E]) sind genau solche typedefs aus dem Prelude. Ein typedef ist zugleich ein Ziel für impl (impl Show for Shape); einen Wert oder einen Laufzeittyp erzeugt er nicht. Typedef-Namen haben mindestens zwei Zeichen, denn ein einzelner Großbuchstabe ist eine Typvariable. Ein typedef kann seinen Typ zusätzlich mit einer Bedingung einschränken, siehe den nächsten Abschnitt.

Rekursive Typen: Listen und Bäume#

Ein typedef darf sich selbst nennen, auch mit Typparametern und über mehrere typedefs hinweg. So entstehen Listen, Bäume und Syntaxbäume:

typedef List[T] = %Nil[] | %Cons[T, List[T]]
typedef Tree[T] = %Leaf[] | %Node[Tree[T], T, Tree[T]]
typedef Node = %{value :- Int, next :- Node?}       # ein rekursiver Record

fn sum(xs :- List[Int]) :- Int -> match xs {
    %Nil[] -> 0
    %Cons[x, rest] -> x + sum(rest)
}

fn insert(t :- Tree[Int], v :- Int) :- Tree[Int] -> match t {
    %Leaf[] -> %Node[%Leaf[], v, %Leaf[]]
    %Node[l, x, r] -> if v < x then %Node[insert(l, v), x, r] else %Node[l, x, insert(r, v)]
}

val xs :- List[Int] = %Cons[1, %Cons[2, %Nil[]]]
val bad :- List[Int] = %Cons[1, %Cons["zwei", %Nil[]]]   # error: found %Cons[Int, List[String]]

--check prüft solche Werte bis in die Tiefe, ein match muss alle Formen abdecken (%Nil[] fehlt → non-exhaustive-match), und mit --check-types prüft auch die Laufzeit die ganze Struktur. Ein typedef, der nur über Aliase auf sich selbst zeigt (typedef Left = Right, typedef Right = Left), nennt keinen Typ und ist ein Fehler (typedef-cycle). Ein ausführliches Beispiel mit Suchbaum, Ausdrucksbaum und Verzeichnisbaum steht in examples/trees.ant.

Typen mit Bedingung: where#

Ein typedef kann seinen Basistyp mit einer Bedingung einschränken (wie subset in Raku). _ ist der Wert:

typedef Age   = Int where _ >= 0 && _ < 150
typedef Name  = String where len(_) > 0
typedef Adult = Age where _ >= 18          # baut auf Age auf: beide Bedingungen

fn birthday(a :- Age) :- Age -> a + 1
println(birthday(30))                       # 31
println(try { birthday(149) } catch { e -> str(e) })
# Type error: the result of 'birthday' must be Age (Int where _ >= 0 && _ < 150), got 150 (Int) ...

Anders als andere Annotationen ist ein solcher Typ ein Vertrag, der immer gilt, wie ein Guard: an jeder Stelle, an der er steht (Parameter, Ergebnis, val, (e :- T), Felder, Lambda-Parameter), prüft die Laufzeit erst den Basistyp, dann die Bedingung, auch ohne --check-types. Normale Annotationen daneben bleiben statisch. Wer nur dokumentieren will, schreibt den Basistyp.

• Für die Prüfung ist Age ein Int: birthday("x") ist ein Fehler wie bei a :- Int.
• --check wertet die Bedingung auf Literalen aus: birthday(150) ist 150 is not a valid Age (Int where _ >= 0 && _ < 150). Werte, die erst zur Laufzeit entstehen, prüft die Laufzeit; ausgewertet werden Vergleiche, + - * %, && || ! und len auf Zahlen und Strings.
• Nativ (antra build --native --optimize) wird die Bedingung zur if-Abfrage am Anfang der übersetzten Funktion; zwei Vergleiche kosten praktisch nichts.
• Der typedef muss vor seiner Verwendung stehen, und ein typedef mit Typparametern kann keine Bedingung haben.

Ranges als Typ#

Für Zahlenbereiche gibt es eine Kurzform (wie Subrange-Typen in Ada und Pascal): eine Range mit Zahlen als Grenzen.

typedef Percent = 0..100            # Int where _ >= 0 && _ <= 100
typedef Adult   = 18..*             # Int where _ >= 18
typedef Below   = *..<0             # Int where _ < 0
typedef Unit    = 0.0..1.0          # Number where _ >= 0.0 && _ <= 1.0
typedef Five    = 0..100 by 5       # ... && _ % 5 == 0
typedef Even    = 0..100 where _ % 2 == 0

Das ist genau die where-Form daneben, mit denselben Prüfungen und Meldungen. Sind beide Grenzen ganze Zahlen, ist der Basistyp Int, sonst Number. Dahinter darf noch ein where stehen; dann gelten beide Bedingungen. Als Grenzen gehen nur Zahl-Literale, by verlangt ganze Zahlen.

Auch Zeichen gehen als Grenzen (Einzelzeichen-Strings, wie bei der Zeichen-Range 'a'..'z'); erlaubt ist dann genau ein Zeichen dazwischen:

typedef Lower = 'a'..'z'            # String where len(_) == 1 && _ >= 'a' && _ <= 'z'
typedef Digit = '0'..'9'

Eine Range kann auch direkt in der Annotation stehen, ohne eigenen Namen; sie heißt dann in den Meldungen wie geschrieben:

fn pow2(n :- 0..*) :- Int -> 2 ** n
fn letter(c :- 'a'..'z' | Digit) -> c
val step :- 0..100 by 5 = 25
pow2(-1)        # Type error: argument 1 of 'pow2' must be 0..* (Int where _ >= 0), got -1 (Int)

Ein match über einem annotierten Wert eines solchen Int-Bereichs prüft --check auf Lücken und tote Arme, auch bei der Langform Int where _ >= 0 && _ <= 100:

fn grade(p :- Percent) -> match p {   # warning: … does not cover 60..89
    90..*   -> 1
    50..<60 -> 4
    *..<50  -> 5
    101..*  -> 6        # warning: match arm never matches: Percent is 0..100
}

Gezählt werden Arme ohne Guard mit Ganzzahl-Literalen, Ranges aus Ganzzahl-Literalen und _/Namen; steht ein anderes Pattern im match, schweigt die Prüfung.

Werte aufzählen: in und |#

Statt eines Bereichs kann ein Typ eine feste Liste von Werten erlauben:

typedef Size  = in %<1, 2, 4, 8>             # Int where _ in %<1, 2, 4, 8>
typedef Vowel = in ["a", "e", "i", "o", "u"] # String where _ in [...]
typedef Color = "red" | "green" | "blue"      # dasselbe wie in ["red", ...]
typedef Dice  = 1 | 2 | 3 | 4 | 5 | 6
typedef Sign  = -1 | 0 | 1 where _ != 0

Auch das ist die where-Form mit _ in …, also ein Vertrag, der immer geprüft wird. Der Basistyp kommt aus den Werten (nur ganze Zahlen: Int, Zahlen: Number, Strings: String). Erlaubt sind nur Literale, keine Ausdrücke, und eine Liste mischt keine Arten. --check prüft Literale (7 is not a valid Dice), nativ wird daraus eine Kette von Vergleichen.

Ein match über so einem Typ meldet wie bei den Ranges fehlende und tote Arme (match over Color does not cover "blue").

Eine Liste oder ein Bereich ist immer der ganze Typ; in [1, 2] | in [:a] ist ein Parse-Fehler. Mehrere Teile benennt man und verbindet die Namen, die Union erbt deren Bedingungen:

typedef Nums  = 1 | 2 | 3
typedef Names = in %<:a, :b>
typedef Mixed = Nums | Names        # 2 und :a passen, 4 nicht

Der Name eines typedef braucht mindestens zwei Zeichen: ein einzelner Großbuchstabe (typedef X = …) wäre in Annotationen eine Typvariable und könnte nie benutzt werden, deshalb ist er ein Parse-Fehler.

Keywords sind anders: typedef Level = :debug | :info bleibt ein rein statischer Enum (siehe oben), zur Laufzeit prüft ihn niemand. Wer das will, schreibt typedef Level = in %<:debug, :info>.

Funktionen und Typvariablen#

Ein einzelner Großbuchstabe ist eine Typvariable. In einer Signatur steht sie für „ein beliebiger, aber fester Typ“:

fn first(xs :- [T]) :- T -> xs[0]
fn apply(f :- fn(T) -> U, x :- T) :- U -> f(x)

val s :- String = first(["a", "b"])     # ok: T ist String
val n :- String = first([1, 2])         # error: T ist Number
fn bad(x :- T) :- Number -> x           # error: x ist irgendein T, nicht Number
println([s, apply(|v| -> v + 1, 2)])

Ohne Annotation werden Funktionen trotzdem allgemein: fn id(x) -> x hat den Typ fn(T) -> T.

Beliebig viele Argumente: ..xs :- ..T#

Ein Rest-Parameter ..xs nimmt die übrigen Argumente. Sein Typ steht mit .. davor und nennt den Typ jedes einzelnen Arguments; im Rumpf ist xs ein [..T], also ein [T]. Der Funktionstyp zeigt den Rest genauso:

fn concat(..vecs :- ..[T]) :- [T] -> vecs[0]   # fn(..[T]) -> [T]
fn tagged(name :- String, ..xs :- ..Int) -> len(xs)

val a = concat([1], [2, 3])        # ok: T ist Int
val b = concat([1], ["x"])         # error: expected [Int], found [String]
val c = tagged("a", 1, "x")        # error: argument 3, expected Int

Ohne .. vor dem Typ ist es ein Parse-Fehler: bei ..vecs :- [T] bliebe offen, ob jedes Argument oder das ganze Array gemeint ist. Mit --check-types wird zur Laufzeit jedes Argument geprüft. Ohne Annotation leitet der Checker den Typ ab (fn loose(..xs) -> xs ist fn(..T) -> [T]), meldet aber nichts.

Parameter, die ein Callback weglassen darf: fn(T, ?Int) -> U#

Ein ? vor einem Parameter eines Funktionstyps heißt: Eine Funktion darf ihn weglassen. So beschreibt man Callbacks, denen der Aufrufer etwas anbietet, das sie nicht nehmen müssen, wie die Position bei Array.map:

fn each_indexed(xs :- [T], f :- fn(T, ?Int) -> _) -> map(xs, f)

each_indexed(["a", "b"], |x| -> println(x))            # ok: ohne Index
each_indexed(["a", "b"], |x, i| -> println(i, x))      # ok: i ist Int
each_indexed(["a"], |x, i, j| -> x)                    # error: drei Parameter

Optionale Parameter stehen am Ende (fn(?Int, String) ist ein Parse-Fehler). Antra::Enum und die Builtins map/filter beschreiben ihre Callbacks so (fn(T, ?Any) -> U, die Position ist ein Index oder ein Map-Schlüssel), Antra::Array mit fn(T, ?Int) -> U. Das ? vor dem Typ ist etwas anderes als Int? dahinter: Int? heißt „der Parameter ist da, kann aber undef sein“. Wer die Funktion aufruft, muss selbst damit umgehen, dass sie weniger Parameter nehmen kann; die Funktionen aus Antra::Enum und die Builtins map/filter geben die Position nur einer Funktion, die sie nimmt.

Kurz-Lambdas: \_ * 2, { _1 + _2 }#

Wird ein Lambda mit Platzhaltern dort übergeben, wo ein Funktionstyp erwartet wird, prüft der Checker es wie eines mit benannten Parametern: _ und _1 sind der erste Parameter, _2 der zweite, und das Ergebnis muss passen.

import Antra::Array

val xs :- [Int] = [1, 2, 3]
val a = Array.map(["a"], \_ <> "!")        # [String]
val b = Array.map(xs, { _1 + _2 })         # [Int]: Element plus Index
val c = Array.filter(xs, \_ * 2)           # error: liefert Number, nicht Bool

fn apply(f :- fn(String) -> Int) -> f("a")
val n = apply(\_ * 2)                      # error: _ ist ein String

Ohne erwarteten Typ (val f = \_ * 2) bleiben die Platzhalter Any.

Typvariablen ausdrücklich nennen: fn name[…]#

Wer sprechende Namen will, nennt die Typvariablen zwischen Funktionsname und Parameterliste, wie bei typedef List[T]:

fn get[Key, Val](m :- Map[Key, Val], k :- Key) :- Val -> m[k]
fn pair[A, B](a :- A, b :- B) :- [A, B] -> [a, b]

val v :- String = get(%{"a" => "x"}, "a")    # ok: Val ist String
val n :- Int = get(%{"a" => "x"}, "a")       # error: found String
fn bad[T](x :- U) -> x                       # error: 'U' is not declared in 'fn bad[...]'

Steht eine Liste da, sind genau ihre Namen Typvariablen, auch längere; ein vergessener Name ist ein Fehler statt still Any. Ohne Liste gilt weiter: jeder einzelne Großbuchstabe ist eine. Die Liste ist rein statisch, zur Laufzeit ändert sie nichts. Hover und --dump-types zeigen die Namen, wie sie geschrieben sind (get :- fn(Map[Key, Val], Key) -> Val); abgeleitete Variablen bekommen einen Buchstaben, den die Signatur nicht schon nutzt.

Schranken: T :- Ord#

In der Liste darf hinter einer Typvariable eine Schranke stehen: was der eingesetzte Typ können muss. Das ist ein Protokoll, ein Typ oder mehreres, mit + verbunden:

fn insert[T :- Ord](t :- Tree[T], v :- T) :- Tree[T] -> …      # vergleichbar
fn index[K :- Ord + Hash, V](m :- Map[K, V]) -> …               # beides
fn sum[T :- Number](a :- T, b :- T) :- T -> a + b               # ein Typ
fn label[T :- Int | String](x :- T) :- String -> str(x)         # eine Union
fn clamp[T :- Number + Ord](x :- T, lo :- T, hi :- T) :- T -> …

insert(%Leaf[], true)   # error: Bool does not satisfy 'T :- Ord' of 'fn insert'
sum("a", "b")           # error: String does not satisfy 'T :- Number' of 'fn sum'

• Protokolle (Ord, Eq, Hash, Add, … aus Antra::Ops, Display, Enumerable und eigene): Builtin-Typen erfüllen die Stdlib-Protokolle, wo sie die Operation haben (Ord: Zahlen und Strings, Add: Zahlen, Contains: Strings, Arrays, Maps, Sets, Ranges, Eq/Hash/Display: alle). Ein getaggter Typ erfüllt ein Protokoll, wenn es ein impl dafür gibt.
• Typen: der eingesetzte Typ muss dazu passen. Im Rumpf darf T dann wie dieser Typ benutzt werden: a + b bei T :- Number; ebenso erlaubt eine Protokoll-Schranke wie Add den passenden Operator.
• Geprüft wird an jedem Aufruf, sobald der eingesetzte Typ bekannt ist; ist er unbekannt (Any, eine andere Typvariable), schweigt --check. Wie die Liste selbst wirken Schranken nur statisch.

Unions und undef: verengen#

T? ist T | Undef. Einen solchen Wert kannst du nicht einfach als T benutzen; erst eine Prüfung verengt ihn:

fn label(name :- String?) :- String -> {
    val bad :- String = name                       # error: union-not-narrowed
    val a :- String = name // "unbekannt"          # ok: // liefert einen Ersatz
    if defined? name then name else a              # ok: im then-Zweig ist name ein String
}
fn kind(x :- Number | String) :- String -> if number?(x) then "Zahl " <> str(x + 1) else "Text " <> x
println([label(undef), kind(1)])

Verengt wird mit defined?, undef?, x == undef, den Prädikaten (string?(x), number?(x), …), in den Armen eines match und mit //. Eine Ascription (x :- Number) verengt ausdrücklich.

Ein Guard mit einem solchen Test verengt den Arm und nimmt seinen Typ den folgenden Armen weg:

fn show(x :- Int | String) :- String -> match x {
    n when int?(n) -> str(n)     # n ist hier Int
    s -> s                       # übrig bleibt String
}

Ein anderer Guard (n when n == 1) verengt nichts, der Arm danach sieht weiter Int | String. Eine Zuweisung im verengten Zweig prüft gegen die Annotation und hebt die Verengung auf: nach x = undef ist x wieder Int?.

Rechnen mit einer Union#

Auch ein Operator braucht einen verengten Wert. x % 2 mit x :- Int | String ist ein Fehler, denn x kann ein String sein (zur Laufzeit: „String cannot be used with '%'“). Erst eine Prüfung macht x im passenden Zweig zum Int:

fn odd?(x :- Int | String) :- Bool -> x % 2 == 1                      # error: union-not-narrowed
fn odd2?(x :- Int | String) :- Bool -> if int?(x) then x % 2 == 1 else false   # ok

Im then-Zweig ist x ein Int, im else-Zweig ein String. So verengen int?, rat?, float?, number?, string?, bool?, keyword?, array?, map?, defined?/undef? und x == undef, in if/unless, nach && und || (int?(x) && x > 0), in match-Armen und in Guards.

Gemischte Arrays und Callbacks#

Ein Array-Literal mit Elementen verschiedener Typen hat als Elementtyp ihre Union: an [T] übergeben ist T bei [1, 2, "drei"] also Int | String. Ein Callback bekommt dann genau diesen Typ für sein Element, und der Checker prüft seinen Rumpf damit, bei |x| -> … wie bei \_ …:

import Antra::Array

val xs = [1, 2, "drei"]
Array.count(xs, \_ % 2 == 1)                                  # error: '_' may be String
Array.count(xs, |x| -> x % 2 == 1)                            # error: 'x' may be String
Array.count(xs, |x| -> if int?(x) then x % 2 == 1 else false) # ok: 1
Array.count(xs)                                               # ok: 3, zählen geht immer

Das gilt für jeden Callback, dessen Typ bekannt ist: die Parameter des Lambdas bekommen die erwarteten Typen (aus der Signatur von Array.count, map, filter, Enum.* oder einer eigenen annotierten Funktion), bevor sein Rumpf geprüft wird; deshalb wirkt if int?(x) darin.

Packages als Typen#

Ein Package mit Feldern ist ein Typ. Annotierte Felder werden geprüft, beim bless, beim Literal und beim Schreiben:

package Wallet {
    pub field cents :- Number = 0
    pub field code :- String = "EUR"
    pub fn new(c :- Number) :- Wallet -> bless(%{cents: c}, Wallet)
}
fn total(w :- Wallet) :- Number -> w.cents
val w = Wallet.new(950)      # w: Wallet, aus der Signatur von new
w.cents = "viel"             # error: cents ist eine Number
println(total(w))

Protokolle#

Auch Protokoll- und impl-Methoden tragen Annotationen. Die der Protokoll-Deklaration gelten für jedes impl, das selbst keine schreibt: der Rumpf wird gegen sie geprüft, und ein Operator auf einem getaggten Wert liefert den annotierten Ergebnistyp seiner Methode.

protocol Measure {
    fn __add__(a, b :- Number) :- Number
}

impl Measure for %Len[..] {
    fn __add__(%Len[a], b) -> a + b     # erbt: b ist Number, das Ergebnis auch
}

val n = %Len[3] + 2                     # n: Number, aus der Deklaration
val s :- String = %Len[3] + 2           # error: expected String, found Number
println(n)

Schreibt ein impl (oder eine Methode eines package P with Proto) eigene Annotationen, müssen sie zur Deklaration passen, sonst meldet --check impl-signature-mismatch. --check-types prüft dieselben Annotationen beim Aufruf. Antra::Ops deklariert die Ergebnisse von Eq (Bool), Ord (:lt | :eq | :gt) und Contains (Bool), Antra::Display das von __str__ (String). Add und die übrigen Rechenprotokolle lassen das Ergebnis offen; dort annotiert man es am impl.

Ein getaggter Wert mit __call__ passt überall, wo eine Funktion erwartet wird (map(xs, adder)), und adder(2) liefert den annotierten Ergebnistyp von __call__.

x[k] und v in x laufen genauso über die Annotationen von __get__ und __contains__: der Index bzw. das gesuchte Element wird gegen Parameter 2 geprüft, x[k] liefert das annotierte Ergebnis.

Self steht in Protokoll- und impl-Methoden für den implementierenden Typ. In einem impl for %V[..] ist das %V[..], in package Money with … der Package-Typ, und beim Operator ist es der linke Operand selbst:

protocol Semigroup {
    fn __add__(a :- Self, b :- Self) :- Self
}
impl Semigroup for %V[..] {
    fn __add__(%V[a, b], %V[c, d]) -> %V[a + c, b + d]
}

val v :- %V[Number, Number] = %V[1, 2] + %V[3, 4]   # ok: Self ist %V[Int, Int]
val n :- Number = %V[1, 2] + %V[3, 4]              # error: found %V[Int, Int]
println(v)
println(n)

In den Methoden eines Packages ist Self das Package selbst (%Body{…}):

package Body {
    pub field m :- Int
    pub fn heavy(self :- Self) :- Self -> %{self | m: self.m * 2}
}
println(Body.heavy(%Body{m: 2}).m)   # 4

Außerhalb von Protokoll-, impl- und Package-Methoden ist Self ein Fehler (unknown-type-name). --check-types prüft Self gegen das Ziel des impl bzw. gegen das Package: ein %W[2] als zweiter Summand eines %V ist ein Typfehler.

Typen aus Bibliotheken#

Annotierte Funktionen importierter Pakete prüfen ihre Aufrufer, auch wenn dein eigener Code keine einzige Annotation hat. Das gilt ebenso für die Builtins (len, split, map, …) und die nativen Module:

import Antra::String
import Antra::Logger

String.upper(5)                  # error: expected String, found Number
split(5, ",")                    # error: expected String, found Number
val n = len("abc")               # n: Number
fn level(l :- Logger.Level) -> l # typedefs importierter Pakete heißen qualifiziert
println([n, level(:info)])

In der Standardbibliothek sind bisher unter anderem Antra::String, Antra::Math, Antra::Path, Antra::Array, Antra::Map, Antra::Set, Antra::Range, Antra::Enum, Antra::Regex, Antra::Result, Antra::Option und die einfachen Funktionen von Antra::FS annotiert.

Antra::Enum nimmt jede Sequenz (Seq[T]); ein Callback darf die Position als zweiten Parameter nehmen, je nach Sequenz ein Index oder ein Map-Schlüssel, daher ?Any:

fn Enum.map(seq :- Seq[T], f :- fn(T, ?Any) -> U) :- [U]
fn Enum.reduce(seq :- Seq[T], acc :- A, f :- fn(A, T, ?Any) -> A) :- A

Antra::Array exportiert dieselben Funktionen weiter, aber mit eigenen, engeren Signaturen: nur Arrays, die Position ist ein Int:

fn Array.map(array :- [T], f :- fn(T, ?Int) -> U) :- [U]
fn Array.count(array :- [T]) :- Int
fn Array.count(array :- [T], pred :- fn(T, ?Int) -> Bool) :- Int

Array.map(1..3, f) ist deshalb ein --check-Fehler (im REPL ein Laufzeitfehler); für Strings und Generatoren sind Enum.* oder die Builtins map/filter da. Genauso haben Antra::Set (set :- Set[T], Position ?Int), Antra::Range (range :- Range[T]) und Antra::Map eigene Signaturen; bei einer Map ist die Position der Schlüssel:

fn Map.map(map :- Map[K, V], f :- fn(V, ?K) -> U) :- [U]
fn Range.take(range :- Range[T], n :- Int) :- [T]
fn Set.union(a :- Set[T], b :- Set[T]) :- Set[T]

Die Funktionen von Antra::Map, die eine Map liefern (assoc, dissoc, merge, map_values, …), haben keinen Ergebnistyp: sie behalten Tag und Felder der Eingabe (Map.assoc(w, :a, 6) auf einem %Wallet{…} ist wieder ein %Wallet{…}), ein Map[K, V] würde das verlieren. :t und :doc im REPL zeigen die Signaturen.

Ein Re-Export kann die Typen einschränken: hinter dem Namen steht dann eine Signatur ohne Rumpf, wie in einem @extern-Paket. #:-Zeilen davor sind seine eigene Doku, und ein Name darf mehrmals stehen, wenn sich die Signaturen in der Zahl der Parameter unterscheiden (wie die Stelligkeiten einer fn):

package Ar {
    import Antra::Enum
    export Antra::Enum.{
        #: Applies `f` to every element of the array.
        map(array :- [T], f :- fn(T, ?Int) -> U) :- [U],
        count(array :- [T]) :- Int,
        count(array :- [T], pred :- fn(T, ?Int) -> Bool) :- Int,
        filter
    }
}

So macht es Antra::Array. Ar.map(1..3, f) ist dann ein --check-Fehler (und mit --check-types bzw. im REPL ein Laufzeitfehler), Enum.map(1..3, f) bleibt erlaubt; aufgerufen wird dieselbe Funktion. Die Signatur muss ein Spezialfall der ursprünglichen sein, sonst meldet --check export-not-narrower; zwei Signaturen gleicher Stelligkeit sind ein Parse-Fehler. Ein Eintrag ohne Signatur (filter) hat die Typen und die Doku des Originals; :doc Ar.filter nennt dann die Herkunft ((re-exported from Antra::Enum.filter)).

Strenger prüfen: @types(strict)#

Standardmäßig bleibt alles still, was nicht annotiert ist. @types(strict) vor einer fn oder einem package macht dort auch Widersprüche zwischen unannotierten Teilen zu Fehlern:

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

@types(strict)
fn name(p) -> p.name                 # error: Feld auf unbekanntem Typ

Mit :- Any hältst du darin eine Stelle bewusst offen, @types(gradual) öffnet eine einzelne Funktion wieder. Mehr dazu in Kapitel 17.

Zur Laufzeit prüfen: --check-types#

--check sieht nur, was sich vor dem Start ableiten lässt. Werte aus unannotiertem Code, aus Dateien oder aus Any kommen ungeprüft durch. Mit --check-types prüft antra jede Annotation beim Ausführen gegen den Wert, der dort ankommt:

antra --check-types programm.ant

fn half(n :- Int) :- Rat -> n / 2
println(half(3))   # 1.5
half(1.5)          # error: Type error: argument 1 of 'half' must be Int, got 1.5 (Rat) (annotation at line 1)

Der Fehler ist ein gewöhnlicher Laufzeitfehler und lässt sich mit try/catch abfangen. Geprüft wird genau, was der Wert zur Laufzeit ist: Ein Array prüft jedes Element, ein Tupel Länge und Positionen, ein Record seine Felder, ein typedef seine Mitglieder (mit Typargumenten, Option[Number]), ein Package mit Feldern seine getaggte Map. Großzügig bleibt die Prüfung, wo der Typ zur Laufzeit zu wenig sagt: Typvariablen wie T, _ und Any passen immer, ebenso Namen, die sie nicht auflösen kann. Bei einem Funktionstyp fn(A, B) -> C prüft sie nur, dass eine Funktion mit zwei Parametern kommt (bei fn(A, ?B) -> C mit einem oder zwei); Argumente und Ergebnis prüft die Funktion selbst, wenn sie annotiert ist.

Nur einen Teil prüfen: @types(runtime) vor einer fn, einem package oder einem impl (auch vor einer einzelnen impl-Methode) schaltet die Prüfung dort ein, auch ohne --check-types. Das eignet sich für die öffentlichen Funktionen einer Bibliothek, deren Aufrufer man nicht kennt:

@types(runtime)
package Wallet {
    pub field cents :- Int = 0
    pub fn new([cents:, ..rest]) -> bless([cents: cents, ..rest], Wallet)
}

Wallet.new(cents: 1.5)   # Type error: field 'cents' of 'Wallet' must be Int, got 1.5 (Rat) (annotation at line 3)

Ohne Schalter und Attribut kosten Annotationen zur Laufzeit nichts. Mit Prüfung wird jeder annotierte Aufruf etwas langsamer, eine eng rekursive Funktion wie fib etwa um die Hälfte.

Häufige Fehler#

Quelle dieser Seite