Agda ist eine funktionale Programmiersprache, die sich durch ihr Typsystem auch als Beweisassistent eignet. The Agda Wiki. Hauptseite. Abgerufen am 12. Mai 2025. Das Wort „funktional“ bezieht sich hier auf die Verwendung von Funktionen als Objekte, die nicht nur definiert und aufgerufen werden, sondern auch als Variablen übergeben und als Wert zurückgegeben werden können. Es ist eine sog. totale Sprache, in der alle Funktionen terminieren und einen Wert des Ergebnistyps zurückgeben. Diese Eigenschaft ist notwendig, damit die Beweise, die man in Agda formuliert, stichhaltig sind. Das Typsystem basiert auf Arbeiten von Per Martin-Löf und kann über die Curry-Howard-Korrespondenz zur Formulierung logischer Aussagen genutzt werden. Dazu ist es notwendig, dass die Typen in Agda auch von Werten abhängen können (engl. dependently typed). Agda-Dokumentation. Getting Started. Abgerufen am 12. Mai 2025.
In Agda kann man einerseits klassische Programme schreiben, die zuerst in Haskell und über den Glasgow-Haskell-Compiler in eine ausführbare Datei übersetzt werden The Agda Wiki. MAlonzo-Unterseite. Abgerufen am 12. Mai 2025.. Andererseits – und das ist eher die Regel – kann man auch Programme schreiben, bei denen der Typprüfer sämtliche zur Übersetzungszeit vorliegenden Informationen nutzt, um bestimmte Berechnungen durchzuführen. Das Programm braucht nicht in eine ausführbare Datei übersetzt zu werden und benötigt dementsprechend keinen Einsprungpunkt (main-Funktion).
Weiterhin kann man in Agda mit einem leeren Quelltext beginnen und von Grund auf eigene Typen und Funktionen definieren, ohne dass man eine Standardbibliothek für Basisfunktionen nutzen muss. Es sind dann auch keine impliziten Typ- oder Funktionsdefinitionen vorhanden (außer der Set-Hierarchie). Es gibt jedoch eine Standardbibliothek Documentation for the Agda standard library. Abgerufen am 12. Mai 2025., die derzeit (Stand 2025) aktiv weiterentwickelt wird.
Der Quelltext in Agda kann an bestimmten Stellen Lücken (eingegeben durch ein ?) enthalten. Diese verhindern zwar die Erstellung eines ausführbaren Programms, gelten aber nicht als Fehler während der Kompilierung. Vielmehr meldet der Compiler, welchen Typ er an der entsprechenden Stelle erwartet. Dies wird üblicherweise als Ziel (engl. Goal) bezeichnet. Ist der Typ so weit eingeschränkt, dass der Compiler bestimmen kann, welcher Wert eingesetzt werden muss, kann dieser den fehlenden Wert automatisch einsetzen.
Agda wird normalerweise über Plug-ins in Emacs Agda-Dokumentation. Emacs-Mode. Abgerufen am 12. Mai 2025., Vim Cornelis. Github-Seite. Abgerufen am 12. Mai 2025. oder Visual Studio Code Agda-Mode for VSCode. Visual Studio Marketplace. Abgerufen am 12. Mai 2025. bedient. Hier werden bestimmte Tastenkombinationen genutzt, um den Quelltext auf Typ-Korrektheit zu prüfen, die Typziele der Lücken abzufragen, automatische Einsetzungen vorzunehmen, Typen abzufragen oder auch den vom Compiler berechneten Wert einer Variable zu ermitteln. Ist der Quelltext typkorrekt, dann wird er auch entsprechend der Syntax eingefärbt. Dies ist eine andere Reihenfolge als bei Programmiersprachen, bei denen die integrierte Entwicklungsumgebung den Quelltext zuerst einfärbt (und eventuelle Syntaxfehler aufzeigt) und später bei der Kompilierung nachträglich noch Typfehler aufdeckt.
Die Syntax von Agda basiert auf der Verwendung von Leerzeichen zur Trennung von Syntaxelementen oder zur Einrückung. Bezeichner können (fast) beliebige Unicode-Zeichen enthalten. Zum Beispiel ist 1≤2 (ohne Leerzeichen) ein gültiger Bezeichner, während 1 ≤ 2 (mit Leerzeichen) einen Ausdruck darstellt. Funktionen werden mit Hilfe von Pattern Matching definiert.
Es ist möglich und vorgesehen, dass man Agda-Quelltexte auch direkt in Dokumenten und Artikeln (engl. literate programming) verwendet. Die Quelltexte haben dann nicht mehr die Endung .agda, sondern z. B. .lagda.md für Markdown-Text oder .lagda.tex für LaTeX-Dokumente. Der Quelltext wird in entsprechende Blöcke im Dokument eingefasst.
Agda ist auf verschiedenen Plattformen verfügbar und kann mittels des Cabal-Paketsystems von Haskell installiert werden. Für die Benutzung ohne Installation steht das Onlinetool Agdapad Agdapad. Online-Emacs mit Agdamode. Abgerufen am 12. Mai 2025. zur Verfügung.
Compilerdialog und Programme ohne Einsprungpunkt
Ein sehr einfaches Agda-Programm, das einen Daten-Typ Bool definiert und das logische UND implementiert, könnte wie folgt aussehen:
module wiki-simple where -- jede Quelldatei ist ein Modul
data Bool : Set where -- Bool ist ein: true : Bool -- entweder "true" false : Bool -- oder "false"
_∧_ : Bool → Bool → Bool -- logisch-UND ist eine Funktion, die zwei Bool-Argumente benötigt und einen Bool zurückgibt true ∧ b = b -- 1. Fall: 1. Argument = true, 2. Argument beliebig: Rückgabe = 2. Argument. false ∧ b = false -- 2. Fall: 1. Argument = false, 2. Argument beliebig: Rückgabe = false
x : Bool -- x ist vom Typ Bool x = true -- x ist "true"
y : Bool -- y ist vom Typ Bool y = false -- y ist "false"
z : Bool -- z ist vom Typ Bool z = x ∧ y -- z ist x UND y; C-n z (normalisieren von z) ergibt false Hierzu einige Bemerkungen: data ist notwendig, damit man mit einem leeren Quelltext starten kann. Es ist die Basis dafür, dass man „alles“ selbst implementieren kann. In Agda wird durch den Doppelpunkt : ein Typurteil gekennzeichnet. Man sieht, dass Bool den Typ Set hat. Das bedeutet so viel wie, dass Bool ein „kleiner“ Typ ist. Set (ist implizit Set 0) selbst hat den Typ Set 1. Somit wird eine unendliche Hierarchie an Typen aufgebaut. Dies vermeidet z. B. die Russellsche Antinomie. true und false nennt man (Daten)konstruktoren. Das logische UND wird durch _∧_ repräsentiert. Die zwei Unterstriche weisen ∧ als Infix-Funktion aus. Der Pfeil _→_ repräsentiert einen Funktionstyp. Verkettete Pfeile sind eine andere Schreibweise für Funktionen mit mehreren Eingaben. Der Pfeil ist rechtsassoziativ, d. h., Bool → Bool → Bool bedeutet eigentlich Bool → (Bool → Bool). Wenn man also das linke Argument in _∧_ einsetzt, erhält man eine Funktion, die einen Bool braucht (das rechte Argument) und daraus einen Bool macht. Siehe hierzu Currying oder Schönfinkeln. Die Definitionen von _∧_ decken alle Fälle ab, dafür sorgt der Typprüfer. Er prüft auch, ob die Funktion terminiert. Die Vorgaben von x und y zur Typprüfungszeit ermöglichen es, z bei der Typprüfung auszurechnen. Daher kann man z nach der Typprüfung abfragen. Ein Einsprungpunkt main ist in diesem Beispiel nicht vorhanden.
Definiert man nun eine Funktion für das logische ODER, sieht das so aus: _∨_ : Bool → Bool → Bool -- logisch-ODER ist eine Funktion, die zwei Bools als Argumente braucht und einen Bool zurückgibt a ∨ b = {!!} -- Definition mit Lücke Die Lücke wird nach der Typprüfung mit { }0 bezeichnet und im Meldungsfenster wird ?0 : Bool gezeigt. Das ist ein Hinweis darauf, dass noch Lücken existieren, die geschlossen werden müssen. Man kann die Ziele noch detaillierter anzeigen lassen. Die Ziel-Ansicht der Lücke { }0 zeigt Goal: Bool ———————————————————————————————————————————————————————————— b : Bool a : Bool Dies besagt, dass hier ein Bool erwartet wird und dafür a und b, beide jeweils Bool, im Kontext verfügbar sind. Bool ist an dieser Stelle allerdings so unspezifisch, dass der Typprüfer nicht eindeutig ermitteln kann, was in die Lücke eingesetzt werden muss. Die Semantik muss hier also vom Programmierer festgelegt werden. Das weitere Vorgehen ist es, eine Fallunterscheidung für a nach true oder false vorzunehmen und dann die beiden Zeilen entsprechend auszufüllen: _∨_ : Bool → Bool → Bool true ∨ b = true false ∨ b = b
Programme mit Einsprungpunkt
Um ein Programm mit Einsprungpunkt in Agda zu erstellen, empfiehlt es sich, die Standardbibliothek zu nutzen.
{-# OPTIONS --guardedness #-} module wiki-hello where
open import IO -- notwendig für "Main", "putStrLn", "getLine", alle Ein-/Ausgabeoperationen open import Data.String using (_++_) -- notwendig für Stringoperationen: _++_ = Stringverkettung
main : Main -- Einsprungpunkt main = run do -- do-Notation wie in Haskell putStrLn "Gib Deinen Namen ein: " -- putStrLn kann nur innerhalb von "do" verwendet werden name ← getLine -- "Zuweisung" des Outputs von getLine an "name" putStrLn ("Hallo, " ++ name) -- Verwendung von "name" in putStrLn Hier muss man auch noch ein paar Bemerkungen machen: --guardedness ist notwendig für z. B. unendliche Listen (Streams) oder allgemein coinduktive Agda-Dokumentation. Coinductive Data. Abgerufen am 14. Mai 2025 Daten, wie sie von IO genutzt werden. import importiert aus einem Modul alles oder mit using nur die spezifizierten (vollständig qualifizierten) Bezeichner in das aktuelle Modul. open entfernt den vorderen Teil des vollständigen Bezeichners (also statt IO.Main nur Main). Die Importe sind aus der Standardbibliothek. Main ist eine Abkürzung für den Typ IO ⊤, wobei ⊤ für den sog. Einheitstyp steht. Die do-Notation funktioniert wie in Haskell. IO ist eine Monade und do ist nur syntaktischer Zucker für eine monadische Verkettung von Operationen wie putStrLn und getLine.
Mit Hilfe der hier genannten Mittel kann man ein ausführbares Programm in Agda erzeugen, welches Terminaleingaben entgegennimmt und -ausgaben erzeugt.
Unendliche, indizierte und parametrisierte Datentypen
Oben wurde der einfache Datentyp Bool eingeführt. Mit endlichen „ist ein“-Datentypen kann man genauso verfahren, also die Konstruktoren einfach aufzählen. Bei „unendlichen“ Datentypen hingegen sind meistens Argumente der Konstruktoren durch den Datentyp selbst gegeben. Daneben unterstützt das data-Schlüsselwort noch Typindizes (rechts vom Doppelpunkt) und Typparameter (links vom Doppelpunkt).
Natürliche Zahlen
Für die natürlichen Zahlen funktioniert die endliche Aufzählung der Konstruktoren nicht mehr. Hier behilft man sich mit den Peano-Axiomen, unter anderem: Null ist eine natürliche Zahl und jede andere natürliche Zahl ist Nachfolger einer natürlichen Zahl. Das wird in Agda wie folgt dargestellt: data ℕ : Set where zero : ℕ -- Null: kann direkt konstruiert werden suc : ℕ → ℕ -- Nachfolger: braucht ein Argument vom Typ ℕ Hier kommt neu hinzu, dass der Konstruktor suc (für Nachfolger) eine natürliche Zahl als Parameter braucht, um ein gültiges Element des Typs zu erzeugen. Dann ist z. B. eins = suc zero und zwei = suc (suc zero) usw.
Nun kann man noch eine Addition natürlicher Zahlen definieren, die sich die Formulierung in Form von Null und Nachfolger zunutze macht: _+_ : ℕ → ℕ → ℕ zero + m = m -- 0 + m = m (aber NICHT m + 0 = m!) suc n + m = suc (n + m) -- suc n + m = suc (n + m) Hier gibt es eine Fallunterscheidung im ersten Argument. Die Addition wird rekursiv definiert, und zwar so, dass für den Fall „Null“ rechts keine Rekursion mehr steht (Basisfall) und für den Fall „Nachfolger“ rechts „strukturell kleinere“ Argumente für _+_ stehen (insbesondere kein suc mehr).
Typindizes als Relationen
Will man nun natürliche Zahlen mit Hilfe der Kleiner-gleich-Beziehung vergleichen, hat man mehrere Möglichkeiten. Die erste ist, dass man eine Funktion schreibt, die den Typ ℕ → ℕ → Bool hat. Hier verliert man aber sehr viele Informationen sowie die Semantik (engl. Boolean Blindness Boolean Blindness. Blogeintrag von Bob Harper. Abgerufen am 20. Mai 2025.). Die zweite Möglichkeit ist, dass man einen Typ anlegt, der das leistet. Gemäß der Curry-Howard-Korrespondenz sind Typen auch als Aussagen zu verstehen Agda-Tutorial von Jesper Cockx. Seite 15ff, insbesondere Seite 21. Version vom 20. März 2023.. Dazu braucht man eine sog. (homogene, zweistellige) Relation. Mathematisch ist das eine Teilmenge des kartesischen Produkts der Ausgangsmenge mit sich selbst, also . In Agda modelliert man das mit sog. indizierten Datentypen (hier mit zwei Indizes): data _≤_ : ℕ → ℕ → Set where -- jeder Konstruktor braucht zwei Argumente z≤n : {n : ℕ} → zero ≤ n -- z≤n kann direkt generiert werden