Homotopy Type Theory (HoTT)

In Sprachen wie Agda oder Cubical Type Theory. Es erlaubt, Dinge zu beweisen, die vorher unmöglich waren. Beispiel: "Ein Integer-Array ist gleich einem Integer-Array" ist einfach. Aber: "Ein isomorphicer Graph ist gleich dem anderen Graphen"? In HoTT: Ja! (Structure Identity Principle). Man kann Bibliotheken schreiben, die automatisch Code für alle isomorphen Strukturen generieren.

1. Univalence Axiom

Der Kern von HoTT. $(A \simeq B) \simeq (A = B)$. "Isomorphie ist äquivalent zu Gleichheit." Das ist in klassischer Mengenlehre falsch (Zahlenmenge ist nicht gleich Buchstabenmenge, auch wenn beide Größe 26 haben). In HoTT darf man sie als gleich behandeln. Das erlaubt "Transport": Wenn ich einen Algorithmus für Menge A habe, und A=B, gilt er sofort auch für B.

2. Higher Inductive Types (HIT)

In normalen Sprachen hast du Inductive Types (Listen, Bäume). In HoTT hast du HITs: Du definierst Punkte und Pfade. Der Typ "Kreis" (S1):

• Ein Punkt base.
• Ein Pfad loop von base zu base. Das definiert mathematisch exakt einen Kreis im Typ-System.

1. Identity Types as Path Spaces

In HoTT ist der Typ a = b (Identitätstyp) nicht einfach ein Wahrheitswert, sondern ein eigener Typ, dessen Bewohner Pfade sind. Das führt zur infty-Groupoid-Struktur:

• Es gibt einen Refl-Pfad (Identität).
• Pfade können invertiert werden (Symmetrie).
• Pfade können komponiert werden (Transitivität). Da aber Pfade selbst Typen sind, gibt es auch Pfade zwischen Pfaden ($p = q$). Dies bildet exakt die Struktur von höheren Homotopiegruppen in der Topologie ab. HoTT ist damit die erste Programmiersprache, die "nativ" die Geometrie von hochdimensionalen Räumen versteht.

2. Computational Content of Univalence

Lange Zeit war das Univallenz-Axiom umstritten, weil es in Coq keine "Rechenregel" hatte (es war ein Axiom). In der Cubical Type Theory wurde bewiesen, dass Univalenz berechenbar ist. Wenn man beweist, dass Typ A isomorph zu Typ B ist, kann der Compiler Funktionen zwischen A und B automatisch "transportieren". Das bedeutet in der Produktion: Wenn du bewiesen hast, dass eine Funktion auf SinglyLinkedList korrekt ist, und du zeigst, dass SinglyLinkedList isomorph zu DoublyLinkedList ist, dann "rechnet" der Compiler den Korrektheitsbeweis automatisch für die doppelt verkettete Liste um.

3. Higher Observational Type Theory (HOTT)

HoTT löst ein fundamentales Problem der Informatik: Extensionalität. Normalerweise sind zwei Funktionen $f$ und $g$ im Computer nur gleich, wenn sie den gleichen Pointer haben. Mathematisch sind sie gleich, wenn sie für alle $x$ das gleiche Ergebnis liefern ($f(x) = g(x)$). HoTT macht diese "Funktionale Extensionalität" beweisbar und nutzbar. Damit nähert sich die Programmierung der idealen mathematischen Welt an, in der wir über das Verhalten von Code argumentieren können, anstatt über die zufällige Speicheradresse.