Dieses Kapitel erläutert Beziehungen zwischen dem Typsystem von Rust und der Typentheorie. Das soll der tiefergehenden Einordnung dienen, ist aber für das Verständnis der Programmiersprache und der nachfolgenden Kapitel nicht essentiell.
Zu zwei Typen X, Y lässt sich
der Typ X×Y bilden, auch (X,Y)
geschrieben. Dies ist der Datentyp der Paare (x,y) mit
x: X und y: Y.
Die Schlussregel zur Einführung von Paaren ist eigentlich straightforward:
Γ |- x: X, Γ |- y: Y ───────────────────── (Prod.) Γ |- (x,y): (X,Y)
Hinzu kommen Regeln zur Projektion:
Γ |- t: (X,Y) ───────────── (Proj. 0) Γ |- t.0: X |
Γ |- t: (X,Y) ───────────── (Proj. 1) Γ |- t.1: Y |
Die Regeln für Produkte von mehr als zwei Faktoren sind
analog. Zu beachten ist, dass es einen Unterschied zwischen
(X,Y,Z) und (X,(Y,Z)) gibt.
Strukturen, auch Records genannt, sind Tupel mit frei wählbaren Bezeichnern zur Indizierung. Die Regel zur Einführung einer Struktur mit zwei Einträgen lautet:
Γ |- x: X, Γ |- y: Y
───────────────────────────────
Γ |- {a: x, b: y}: {a: X, b: Y}
Entsprechend gibt es wieder Regeln zur Projektion:
Γ |- s: {a: X, b: Y}
────────────────────
Γ |- s.a: X
Die Bezeichner a, b gehören zum
Typ dazu. Infolge bedeuten andere Bezeichner einen anderen Typ.
Die Regeln für Strukturen mit mehr als zwei Einträgen sind analog zu den genannten.
Für eine Enumeration
enum E{V(T), ...}
gibt es zur jeweiligen Variante E::V die Regel:
Γ |- x: T ─────────────── Γ |- E::V(x): E
Zur Zerlegung von Enumerationen bedarf es einer weiteren Regel:
Γ |- t: E
Γ ∪ {xi: Ti} |- ti: T für jedes i
──────────────────────────────────────
Γ |- match t {E::V0(x0) => t0, ...}: T
In Worten: Der Term t sei vom Typ E.
Außerdem sei angenommen, dass wenn jeweils die Variable xi
vom Typ Ti ist, dann der zugehörige Term ti
vom Typ T. Weil daher jeder der Terme vom gleichen
Typ T ist, ist auch der Musterabgleich von diesem
Typ.
Zu zwei Typen X, Y gibt es den
Typ X → Y, der alle Funktionen mit
Argument vom Typ X und Wert vom Typ Y
beschreibt. Z. B. besitzt die Funktion
fn f(x: u32) -> bool {x%2 == 0}
die Typisierung
f: u32 → bool.
Für Funktionen gilt die folgende Schlussregel:
Γ |- f: X → Y, Γ |- x: X
───────────────────────── (App.)
Γ |- f(x): Y
Diese Schlussregel nennt man die Regel der Applikation, kurz App. geschrieben. Für den Kontext
Γ := {n: u32, f: u32 → bool}
gilt z. B. die Schlussfolgerung:
1. Γ |- f: u32 → bool 2. Γ |- n: u32 3. Γ |- f(n): bool (App. 1., 2.)
Polymorphe Typisierung erkennt man an Typvariablen. Polymorphe Typen sind solche, die über Typvariablen allquantifiziert sind.
Hat ein Term den Typ ∀T.A,
bedeutet dies, der Term ist vom Typ A[T:=U] für jeden
beliebigen Typ U. Das heißt, der Term hat nicht nur
einen Typ, sondern unendliche viele, die durch die Substitution
der Typvariable T durch beliebige Typen entstehen.
Diese Substitution bezeichnet man als Spezialisierung.
In Rust stehen die Typvariablen in spitzen Klammern. Betrachten wir dazu einmal die identische Funktion, das ist:
fn id<T>(x: T) -> T {x}
Diese Funktion hat die Typisierung
id: ∀T. T → T.
Sagen wir mal, wir haben den Kontext
Γ := {n: u32, id: ∀T. T → T}.
Dann kann man schlussfolgern:
1. Γ |- id: ∀T. T → T 2. Γ |- id: u32 → u32 (1. [T:=u32]) 3. Γ |- n: u32 4. Γ |- id(n): u32 (App. 2., 3.)
Bei Vorhandensein von Trait-Bounds wird das nun ein wenig komplizierter. Betrachten wir dazu:
fn dup<T: Clone>(x: T) -> (T,T) {(x.clone(),x)}
Diese Funktion hat die Typisierung
dup: ∀T∈Clone. T → (T,T).
Eine Substitution T:=U ist nur noch dann
durchführbar, wenn U in Clone liegt, das
heißt wenn Clone für U implementiert wurde.
Existentielle Typisierung erlaubt es, Wissen über die genaue Struktur eines Wertes zu Vergessen, womit sich abstrakte Schnittstellen erstellen lassen. Dies bildet die theoretische Grundlage für Module und abstrakte Datentypen.
Regel zur Einführung existentiell quantifizierter Typen:
Γ |- t: X[T:=U] ──────────────── (Pack) Γ |- (U,t): ∃T.X
In Worten: Vorausgesetzt sei, der Term t ist vom Typ
X nachdem in X jedes Vorkommen der
Typvariable T gegen den Typ U ersetzt wurde.
Dann ist das Paar (U,t) vom
existentiellen Typ ∃T.X.
Zu bemerken ist dazu noch, dass der Term (U,t) mehrere
unterschiedliche existentielle Typen haben kann. Zur eindeutigen
Zuordnung schreibt man explizit (U,t) as ∃T.X.
Nun muss man Terme mit existentiell typisierten Variablen auch auswerten können, wofür es an weiteren Regeln bedarf. Wir definieren
unpack (T,x) = (U,t) in s
als s[x:=t][T:=U]. In Worten: Enthält der Term
s eine Variable x und ist ein Wert
(U,t) gegeben, und möchte man x=t haben,
kann man s auswerten, indem jedes Vorkommen von
x in s durch t ersetzt wird.
Damit das einen Sinn ergibt, darf für x natürlich
kein beliebiger Term ersetzt werden. Zusätzliche Forderung ist
x: X. Das führt zu der folgenden Schlussregel:
Γ |- e: ∃T.X, Γ∪{x: X} |- s: Y, T ∉ FV(Y)
─────────────────────────────────────────── (Unpack)
Γ |- (unpack (T,x) = e in s): Y
Der Typ X kodiert die abstrakte Schnittstelle und
x: X sagt aus, dass man auf x lediglich
Operationen dieser Schnittstelle anwenden darf.
Betrachten wir als Beispiel den Struktur-Typ
X := {a: T; to_string: T → String}.
Ohne die Forderung, dass T nicht in den freien
Variablen FV(Y) vorkommen darf, würde die
Abstraktion kaputt brechen, womit interne Struktur von x
in den Wert von s entweichen würde. Z. B. kann man
nicht einfach s:=x.a setzen. Dann wäre ja s: T,
also Y=T und daher T ∈ FV(Y).
In Rust ist ∃X.T für die genannte Struktur
X als opaker Typ impl ToString modellierbar.
Wir betrachten die bereits in der Standardbibliothek definierte
Schnittstelle:
trait ToString {
fn to_string(&self) -> String;
}
Man braucht nun lediglich self := a zu setzen.
Beispielprogramm:
fn f(a: i32) -> impl ToString {a}
fn main() {
let x = f(0);
println!("{}", x.to_string());
}
Die Formulierung ist äquivalent zu der existenziell quantifizierten
Struktur, weil man erstens an den Typ von a nicht mehr
herankommt, und zweitens die Funktion to_string
trotzdem auf a anwendbar bleibt. Darin besteht genau der
springende Punkt, den wir haben wollen.
Man darf sich das so vorstellen, als würde die Struktur während der
Optimierung durch den Compiler entfernt, weil kein Bedarf am
dynamischen Dispatch besteht. Nämlich kann der Compiler schon zur
Kompilierzeit in Erfahrung bringen, dass to_string auf
einen Wert des Typs i32 angewendet wird.
Im Gegensatz zu impl Trait ist beim opaken Typ
Box<dyn Trait> auch dynamischer Dispatch zulässig.
Dieser Typ entspricht dem Zeigerpaar
∃T.(Box<T>, &{to_string: &T → String}).
Das äquivalente Beispielprogramm:
fn f(a: i32) -> Box<dyn ToString> {Box::new(a)}
fn main() {
let x = f(0);
println!("{}", x.to_string());
}
Eine andere Modellierung von existentiell quantifizierten Typen sind Module mit privaten Variablen und Funktionen. Das äquivalente Beispielprogramm:
mod mx {
pub struct X {a: i32}
impl X {
pub fn to_string(&self) -> String {
format!("{}", &self.a)
}
}
pub fn f(a: i32) -> X {X {a}}
}
fn main() {
let x = mx::f(0);
println!("{}", x.to_string());
}
Wieder ist erreicht, dass man an a nicht mehr
herankommt, die Funktion to_string aber auf
a anwendbar bleibt.
Auch Closures bieten die Möglichkeit zur Auftrennung zwischen Schnittstellen und privaten Daten. Das ist ein Grund dafür, warum Closures opake Typen haben müssen. Nochmals das äquivalente Beispielprogramm:
fn f(a: i32) -> impl Fn() -> String {
move || format!("{}", a)
}
fn main() {
let to_string = f(0);
println!("{}", to_string());
}
Bei verketteten Listen und Bäumen enthalten die Knoten Einträge von der Form der Gesamtstruktur. Zur Typisierung solcher Strukturen sind rekursive Typen erforderlich.
Rekursive Typen lassen sich mit den bisherigen Mitteln nicht
darstellen. Man führt für sie die Notation μT.Term
ein, wobei T eine Typvariable ist. Diese Typvariable
kommt im Term Term vor, und steht obendrein für den
Term selbst.
Das klassische Beispiel für einen rekursiven Typ ist die Darstellung der natürlichen Zahlen als
Nat = μT.enum {Zero, Succ(T)},
oder in abstrakter Form äquivalent als
Nat = μT.Either<(), T> = μT.1+T.
In Rust sind rekursive Typen in der Gestalt nominaler Typen
darstellbar, wobei die Notwendigkeit der speziellen Notation mit
Typvariable entfällt. Die Entsprechung zu Nat kann man als
enum Nat {Zero, Succ(Rc<Nat>)}
oder
enum Either<X, Y> {Left(X), Right(Y)}
struct Nat(Either<(), Rc<Nat>>);
gestalten. Ein ähnliches Beispiel bieten die bereits in der Form
enum List<T> {
Nil, Node {data: T, next: Box<List<T>>}
}
beschriebenen einfach verketteten Listen. Wir können
Nat an und für sich sogar als äquivalent zu
List<()> betrachten.