Begriff
Agda
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Haskell ist cool. Aber das Typ-System hat Grenzen. Agda ist wie Haskell auf Steroiden (Dependent Types). In Agda schreibst du keinen Code, der testet. Du schreibst Code, der beweist. Agda prüft zur Compile-Zeit, ob deine Logik wasserdicht ist. Es ist gleichzeitig eine Programmiersprache und ein Beweis-Assistent. Besonderheit: Du programmierst interaktiv. Du schreibst ein "?", und Agda sagt dir: "Hier muss ein Beweis vom Typ X hin. Soll ich es versuchen?"
Merksatz: Eine funktional typisierte Programmiersprache mit abhängigen Typen, die primär als Beweisassistent verwendet wird, um die Korrektheit von Programmen mathematisch zu verifizieren.
Die IDE (Emacs Mode) ist der Star.
rev : List A -> List A.
rev [] = [].
rev (x :: xs) = ?.
Du drückst Ctrl+C Ctrl+R (Refine).
Agda füllt das Loch.
Du beweist: rev (rev xs) == xs.
Wenn das kompiliert, hast du mathematisch garantiert, dass deine Reverse-Funktion korrekt ist.
1. Termination Checker
Agda erlaubt keine Endlosschleifen. (Sonst wäre die Logik inkonsistent -> Curry-Howard). Agda prüft, ob jede Rekursion auf "kleinere" Argumente angewendet wird. Wenn nicht (z. B. Collatz-Vermutung), lehnt Agda den Code ab, auch wenn er richtig wäre.
2. Unicode
Agda liebt Unicode.
Du schreibst nicht forall, du schreibst ∀.
Du schreibst nicht ->, du schreibst →.
Code sieht aus wie ein Mathe-Paper. $\mathbb{N} \to \mathbb{N}$.
1. Cubical Agda & Univalence
Eine der fortschrittlichsten Varianten ist Cubical Agda, basierend auf der Homotopy Type Theory (HoTT). In normalem Mathe/Informatik ist Gleichheit ($A = B$) oft schwer zu handhaben. Cubical Agda nutzt das Univalenz-Axiom. Es erlaubt es, zwischen verschiedenen aber isomorphen Typen (z. B. Binärzahlen und römische Zahlen) hin- und herzuspringen. Wenn du ein Theorem für Typ A beweist, "transportiert" Agda den Beweis automatisch zu Typ B. Das reduziert den "Beweis-Schreibaufwand" (Boilerplate) massiv und nähert sich der Art an, wie Topologen über Räume nachdenken.
2. Reflection & Elaboration
Agda kann über sich selbst nachdenken (Reflektion).
Ein Programmierer kann "Makros" schreiben, die den Agda-Typ-Checker manipulieren.
Wenn du ein triviales, aber langes Theorem hast, schreibst du ein Makro, das den Beweis automatisch generiert (Tactic-basiert wie in Coq, aber in Agda-Syntax). Agda "elaboriert" dann deine Abkürzungen zu vollwertigen Beweis-Termen. Das ist die Basis für moderne Bibliotheken wie standard-library, die tausende von Lemmata hocheffizient verwalten.
3. Definitional vs. Propositional Equality
Ein Profi-Agda-User unterscheidet streng:
- Definitional Equality ($A \equiv B$): Dinge, die per Definition gleich sind (z. B. $2+2$ und $4$). Der Compiler sieht sie als identisch an.
- Propositional Equality ($A = B$): Dinge, die zwar gleich sind, für die man aber einen Beweis liefern muss (z. B. $x+y = y+x$). Die Kunst in Agda besteht darin, seine Datentypen so "schlau" zu definieren, dass möglichst viele Eigenschaften definitorisch gelten. Je mehr der Compiler "einfach so" weiß, desto weniger Kopfschmerzen hast du beim Beweisen komplexer System-Eigenschaften.
Quick-Check
Produktion?
Kaum. Agda kompiliert zu Haskell oder JS, aber der Fokus liegt auf Verifikation, nicht Performance. Firmen nutzen eher Rust/Haskell, und Agda nur für Kern-Algorithmen.Unterschied zu Coq?
Coq nutzt Taktiken ("Mach Schritt A, dann B"). Agda ist "Term-basiert" (Du schreibst das Programm direkt, wie in Haskell). Viele finden Agda intuitiver.Schweden?
Geburtsort von Agda (Chalmers University, Göteborg). Benannt nach einer Henne (aus einer schwedischen Kindergeschichte).