In Gallina besitzt jeder Term einen Typ, womit der Typ des Resultats
der Auswertung des Terms gemeint ist. Die Notation
t: T drückt aus, dass der Term t
vom Typ T sein soll. Beispielsweise gilt
0: nat, womit gesagt wird, dass 0 eine
natürliche Zahl ist.
Man benutzt Check um prüfen zu lassen, ob ein Term
wohltypisiert ist. Damit verbunden lässt sich der Typ des Terms
ermitteln. So liefert
Check 1 + 2.
den Typ nat, was für den Typ der natürlichen Zahlen
steht. Der Wert des Terms wird mit
Compute 1 + 2.
berechnet. Der Befehl Definition bindet eine Variable
an einen Wert.
Definition x: nat := 1. Compute x + 1.
Typinferenz gestattet hierbei die Auslassung der Typangabe.
Definition x := 1. Compute x + 1.
Mit einer Funktion darf man umgehen wie mit einem gewöhnlichen Wert. Möchte wir die Funktion f(x) := 2x + 1 definieren, können wir dies als Bindung von x ↦ 2x + 1 an die Variable f ausdrücken. Man schreibt dies so:
Definition f := fun x => 2*x + 1. Compute f 10.Die übliche Schreibweise geht aber auch:
Definition f x := 2*x + 1. Compute f 10.
Bei der Applikation muss man keine Klammern benutzen.
Für f(10) darf man also f 10
anstelle von f(10) schreiben. Bei der Definition ist
zwingend f x anstelle von f(x) zu
schreiben.
Wie jeder Term muss eine Funktion einen Typ besitzen. Fügt man überall die Typangabe hinzu, nimmt die Definition die Form
Definition f: nat -> nat := fun x: nat => 2*x + 1.
bzw.
Definition f (x: nat): nat := 2*x + 1.
an. Eine zweistellige Funktion wie f(x, y) := x + y wird in geschönfinkelter Form beschrieben, also als f(x)(y) := x + y bzw.
f := x ↦ y ↦ x + y.
Man formuliert dies so:
Definition f := fun x => fun y => x + y. Compute f 1 2.
Auch hier darf man Kurzschreibweise nutzen:
Definition f x y := x + y. Compute f 1 2.
Der Typ von f ist nat -> nat -> nat.
Eine Typ wie A → B → C
wird also leichter verständlich, wenn man ihn inhaltlich als
A × B → C
auffasst. Eigentlich lässt sich eine Funktion sogar in dieser üblichen
Form formulieren. Man schreibt:
Definition f t := match t with (x, y) => x + y end. Compute f (1, 2).
Der Typ von f ist nun nat*nat -> nat,
was ℕ×ℕ → ℕ entspricht. Das Beispiel
Definition t0 := (1, 2). Compute f t0.
macht deutlich, dass die Argumente hierbei tatsächlich eine Zusammenfassung zu einem Tupel bilden, welches sich von der Applikation trennen lässt.
Zu jedem Typ ist die identische Funktion definierbar, die ihr Argument unverändert lässt. Für die natürlichen Zahlen würde man
Definition id (x: nat) := x.festlegen, für Wahrheitswerte dagegen
Definition id (x: bool) := x.
Es ist machbar und ein Kernkonzept, diese Funktion in allgemeiner
Weise definieren zu können. Hierzu bekommt die Funktion den Typ
von x als weiteres Argument:
Definition id T (x: T) := x. Compute id nat 0. Compute id bool false.
Es tut sich nun die Frage auf, welchen Typ diese Funktion denn eigentlich haben soll. Hier hängt der Typ des zweiten Arguments vom ersten Argument ab. Eingehender betrachtet hängt der Typ der Funktion vom ersten Argument ab.
Für tieferes Verständnis möchte ich eine Betrachtung in der Mengenlehre einwerfen. Es sei das Tupel
(1, 2, 3, 4) ∈ ℕ×ℕ×ℕ×ℕ
gegeben. Auslesen der Komponenten des Tupels geschieht per Indizierung. Nun verhält es sich so, dass diese Indizierung als Funktion betrachtet bereits die gesamte Information über das Tupel enthält. Schärfer, das Tupel und dessen Indizierung charakterisieren sich gegenseitig, sind in gewissem Sinn isomorph. Dem gegebenen Tupel entspricht demzufolge die Funktion
{0 ↦ 1, 1 ↦ 2, 2 ↦ 3, 3 ↦ 4} ∈ (I → ℕ)
für die Indexmenge I = {0, 1, 2, 3}. Diese alternative Sichtweise öffnet uns nun die Tür, ein allgemeines Produkt von Mengen zu definieren. Es findet sich das Monstrum
∏i∈I Xi := {f: I → ⋃i∈I Xi | ∀i∈I: f(i) ∈ Xi}.
Einfach gesprochen ordnet die Funktion f hier jedem Index ein Element einer anderen Menge zu, sofern die Mengen Xi unterschiedlich sind. Im Spezialfall, wo die Mengen gleich einer Menge X sind, vereinfacht sich das Produkt zur Menge der Abbildungen I → X. So ist es im obigen Beispiel, wo Xi = ℕ und f(i) = i + 1 gilt.
Zu diesem allgemeinen Produkt gibt es in der Typentheorie eine Entsprechung. Ein solches Produkt ist genau das, was wir haben wollen. Der Typ T nimmt die Rolle des Index ein. Nun ordnet id jedem T eine Funktion id(T) eines anderen Typs zu, und dieser Typ ist T → T. Es findet sich somit die Typisierung
id: ∏T: Type (T → T).
In Gallina schreibt man dies so:
id: forall(T: Type), T -> T
Der Grund für die Notation forall liegt darin, dass dem Produkt
aufgrund der Curry-Howard-Korrespondenz die Allquantifizierung entspricht.
Typinferenz ist ebenfalls zur Ableitung von Typargumenten fähig.
Anstelle von id nat 0 darf man
id _ 0 schreiben, wobei der Unterstrich eine
Leerstelle beschreibt. Wird das Typargument in der Definition von
geschweiften Klammern umfasst, darf der Unterstrich bei der Applikation
entfallen:
Definition id {T} (x: T) := x.
Compute id 0.
Compute id false.
Möchte man das Typargument dennoch explizit aufführen, wird dem Bezeichner der Funktion ein at-Zeichen vorangestellt:
Compute @id nat 0.
Erwähnen möchte ich noch, dass die gezeigte Art von abhängigen Funktionen ebenfalls in vielen anderen Programmiersprachen zu finden ist. Man nennt sie generisch oder parametrisch polymorph. Das Typargument nennt man Typparameter. In Rust kommen Typparameter in spitze Klammern. In Standard ML und Objective Caml wird ein Typparameter nicht explizit als Argument aufgeführt.
| Sprache | Notation |
|---|---|
| Gallina | Definition id T (x: T): T := x.
|
| Rust | fn id<T>(x: T) -> T {x}
|
| SML | fun id (x: 'T): 'T = x;
|
| OCaml | let id (x: 'T): 'T = x;;
|
In SML/OCaml schreibt man üblicherweise 'a anstelle
von 'T.
Obwohl die vier Sprachen eng miteinander verwandt sind, ist hier bereits ein erheblicher Wildwuchs an unterschiedlicher Syntax zu verzeichnen.
In der Mengenlehre kann man zu je zwei Mengen A und B die Vereinigungsmenge A ∪ B betrachten, die ein Element genau dann enthält, wenn es in A oder in B enthalten ist. Nun kann es sein, dass sich die Mengen A und B überschneiden, dass es also Elemente gibt, die sowohl in A als auch in B enthalten sind. Wir wollen die Überschneidung nun künstlich verhindern, indem die Elemente vor der Vereinigung ein Tag bekommen. Alle Elemente von A bekommen das Tag left und alle Elemente von B das Tag right. Auf diese Weise ist die disjunkte Vereinigung
A + B := {(left, a) | a ∈ A} ∪ {(right, b) | b ∈ B}
definiert. Mit den beiden injektiven Funktionen
inl(a) := (left, a),
inr(b) := (right, b)
erhält man eine Charakterisierung der Konstruktion. In der Typentheorie gibt es nun eine Summe genannte direkte Entsprechung der disjunkten Vereinigung, wobei auch die Begriffe Enumeration und diskriminierte Vereinigung gebräuchlich sind. Zur Definition der Summe schreiben wir:
Inductive S := inl: A -> S | inr: B -> S.
Hierbei darf man inl und inr als Tags
oder als Injektionen auffassen. So gesagt steht inl
stellvertretend für left und inr
stellvertretend für right.
Ein Tag muss nicht unbedingt Informationen tragen.
Der Typ bool lässt sich als Summe definieren,
die lediglich aus den beiden Tags true und
false besteht:
Inductive bool := true | false.
Wahrheitsfunktionen definiert man nun per Fallunterscheidung,
wofür der Musterabgleich mit match zur Verfügung
steht.
Definition not (a: bool) := match a with
| false => true
| true => false
end.
Definition and (a: bool) (b: bool) := match a with
| false => match b with
| false => false
| true => false
end
| true => match b with
| false => false
| true => true
end
end.
Definition or (a: bool) (b: bool) := match a with
| false => match b with
| false => false
| true => true
end
| true => match b with
| false => true
| true => true
end
end.
Compute or (not false) false.
Kommentare stehen wie in SML/OCaml zwischen von runden Klammern umfassten Sternchen.
(* Kommentar *)
Sie dürfen verschachtelt werden.
(*
(* Kommentar *)
*)