Induktive Typen

Inhaltsverzeichnis

Induktive Typen
Rekursion

Induktive Typen

Zum Einstieg wurde bereits erklärt, wie sich mit Inductive neue Typen definieren lassen. Eigentlich handelt es sich bei der Konstruktion induktiver Typen um ein recht komplexes Werkzeug, etwas was man als eierlegende Wollmilchsau bezeichnen würde. Es enthält drei verschiedene Teilaspekte:

Die Erklärung eines einzigartigen Typen: Jeder hiermit neu definierte Typ unterscheidet sich von allen anderen. Das heißt, es steht ein Mittel zur nominalen Typisierung zur Verfügung, vergleichbar mit newtype in Haskell oder enum, struct in Rust.
Die Erklärung einer Summe: Kommt mehr als eine Konstruktorfunktion vor, handelt es sich um eine Summe.
Die Erklärung eines rekursiven Typen: Enthält eine Konstruktorfunktion den zu erklärten Typen als Typ einer ihrer Argumente, so handelt es sich um einen rekursiven Typen im eigentlichen Sinne.

Nominaler Aspekt

Zum ersten Teilaspekt legen wir Typen A und B derselben Struktur fest.

Inductive A := cons_A (n: nat).
Inductive B := cons_B (n: nat).

Definition a := cons_A 0.
Check a: A.

Wäre die Typisierung von A, B strukturell, so würde Check a: B ebenfalls aufgehen. Der Typprüfer gibt uns jedoch zu verstehen, dass dies nicht stimmt. Sollen A, B tatsächlich strukturell typisiert sein, müsste man sie vermittels Definition als Typalias zu nat festlegen.

Definition A := nat.
Definition B := nat.

Definition a: A := 0.
Check a: B.

Man stellt weiterhin fest, dass als Record definierte Typen allem Anschein nach bereits nominal typisiert sind. Wir testen dies kurzerhand am Beispiel

Record PointA := {Ax: nat; Ay: nat}.
Record PointB := {Bx: nat; By: nat}.

Definition a := {|Ax := 0; Ay := 0|}.
Check a: PointA.

aus. Läge strukturelle Typisierung vor, würde Check a: PointB aufgehen. Es tut sich die Frage auf, ob Strukturen mit benannten Feldern bzw. Projektionen überhaupt definierbar sind. Zuweilen betrifft dies auch andere Sprachen. So tat man sich bei Rust schwer, structural records zur Sprache hinzuzufügen; bisweilen sind sie nur emulierbar. Sie sind aus ergonomischen Gründen wünschenswert, dergestalt dass damit Funktionen mit benannten Argumenten erklärt werden können. In Gallina bekommen wir benannte Argumente elegant als Winkelzug via Typinferenz auf Basis der Projektionen. Betrachten wir dazu die folgende quadratische Form sq mit den benannten Argumenten x und y.

Record Point := {x: nat; y: nat}.

Definition sq (a: Point) :=
  3*a.(x)*a.(x) + 2*a.(y)*a.(y).

Compute sq {|x := 1; y := 2|}.

Eine Struktur lässt sich sogar per Musterabgleich auflösen, wie

Definition sq '(Build_Point x y) :=
  3*x*x + 2*y*y.

zeigt. Man darf dies allerdings als bedenklich erachten, weil es nun, da die Projektionen vom selben Typ sind, auf die Reihenfolge ankommt.

Rekursion

Einfache Rekursion

Zur rekursiven Festlegung einer Funktion nutzt man statt Definition das Schlüsselwort Fixpoint.

Fixpoint pow (x n: nat): nat :=
  match n with
  | 0 => 1
  | S n => x*(pow x n)
  end.

Compute pow 2 10.

Diese Festlegung entspricht der folgenden Anwendung des Rekursors nat_rec. Jeder induktive Typ induziert einen Rekursor, der automatisch definiert wird.

Definition pow x: nat -> nat :=
  nat_rec (fun n => nat) 1 (fun n y => x*y).

Wechselseitige Rekursion

Zur wechselseitigen Rekursion fügt man die weitere rekursive Erklärung mit dem Schlüsselwort with hinzu.

Fixpoint even (n: nat) :=
  match n with
  | 0 => true
  | S n => odd n
  end
with odd (n: nat) :=
  match n with
  | 0 => false
  | S n => even n
  end.

Alternativ geht es auch mit einem let-Ausdruck.

Fixpoint even (n: nat) :=
  let fix odd (n: nat) :=
    match n with
    | 0 => false
    | S n => even n
    end
  in
    match n with
    | 0 => true
    | S n => odd n
    end.