Funktionentypen dürfen nicht nur von Typen abhängig sein, sondern gleichermaßen von Werten. Ein einfaches Beispiel hierfür bietet der Umgang mit einem durch eine natürliche Zahl parametrisieren Typ.
Es soll durchführbar sein, zwei Längen zu addieren,
zwei Flächen zu addieren, zwei Volumina zu addieren.
Aber es soll nicht durchführbar sein, eine Länge und eine Fläche
zu addieren. Wir definieren dazu einen neuen Typkonstruktor
Quantity, der jeder Dimension einen unterschiedlichen
Typ zuordnet:
| Typ | Bedeutung |
|---|---|
Quantity 1 | eine Länge |
Quantity 2 | eine Fläche |
Quantity 3 | ein Volumen |
Der Typkonstruktor und die generische Addition sind wie folgt implementierbar:
Inductive Quantity: nat -> Type :=
quantity: forall (dim: nat), nat -> Quantity dim.
Definition length := quantity 1.
Definition add {dim: nat} (x y: Quantity dim): Quantity dim
:= match x with quantity _ xv =>
match y with quantity _ yv => quantity _ (xv + yv) end
end.
Compute add (length 12) (length 9).
Es ist add vom abhängigen Typ
∏n: ℕ (Quantity(n) → Quantity(n) → Quantity(n)).
Bereits der Wertkonstruktor quantity hat einen
abhängigen Typ, der da ist
∏n: ℕ (ℕ → Quantity(n)).
Die Summe ∑x: U B(x) kann man sich für ein unendlich großes Universum U als disjunkte Vereinigung unendlich vieler Typen vorstellen. Ein Wert dieses Typs ist ein Paar (a, b), bei dem b vom Typ B(a) ist. Weil also der Typ des rechten Eintrags vom linken abhängt, spricht man von einem abhängigen Paar. Synonym zu Summe und Sigma-Typ spricht man daher auch von einem Typ abhängiger Paare.
In Gallina werden Summen und abhängige Paare so dargestellt:
| Ausdruck | Syntax |
|---|---|
| ∑x: U B(x) | {x: U & B x}
|
| (a, b) | existT _ a b
|
Man kann Summen zum verstecken von Information nutzen, womit sich abstrakte Datentypen modellieren lassen. Ein kurzes Beispiel hierzu. Es soll ein Typ für Zeitwerte definiert werden, wobei sich der Wert über Zugriffsfunktionen bzw. Methoden in Minuten oder Sekunden auslesen lässt. Zunächst die Funktionalität:
Record Time T := {value: T; min: T -> nat; sec: T -> nat}.
Definition from_min (m: nat): Time nat
:= {| value := m; min := fun m => m; sec := fun m => 60*m |}.
Definition t := from_min 2.
Compute t.(min nat) t.(value nat).
Compute t.(sec nat) t.(value nat).
Um einen abstrakten Datentyp zu erhalten, würde wir gerne
den Zugriff auf den internen Wert verbergen. Das heißt, der
Wert soll lediglich über die Schnittstellen min
und sec auslesbar sein, aber nicht in direkter
Weise als
Compute t.(value nat).
Ändert man from_min nun so, dass die Signatur
ℕ → ∑T Time(T)
anstelle ℕ → Time(ℕ) lautet, wird der interne Wert
verborgen. Wir können zwar noch den Wert (T, t)
mit t: Time(T) erhalten, aber es bleibt
unbekannt dass T mit ℕ übereinstimmt.
Die Implementierung:
Definition from_min (m: nat): {T: Type & Time T}
:= existT _ (nat: Type) {| value := m;
min := fun m => m; sec := fun m => 60*m |}.
Definition t := from_min 2.
Compute match t with existT _ T t => t.(min T) t.(value T) end.
Compute match t with existT _ T t => t.(sec T) t.(value T) end.
Den umständlichen Zugriff kann man schließlich noch in Funktionen verpacken:
Definition in_min (t: {x: Type & Time x}): nat
:= match t with existT _ T t => t.(min T) t.(value T) end.
Definition in_sec (t: {x: Type & Time x}): nat
:= match t with existT _ T t => t.(sec T) t.(value T) end.
Definition t := from_min 2.
Compute in_min t.
Compute in_sec t.