Agda

Agda ist eine funktionale Programmiersprache, die sich durch ihr Typsystem auch als Beweisassistent eignet. 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).

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. 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, 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 soweit 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, Vim oder Visual Studio Code 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 zur Verfügung.

1. ↑ The Agda Wiki. Hauptseite. Abgerufen am 12. Mai 2025.
2. ↑ Agda-Dokumentation. Getting Started. Abgerufen am 12. Mai 2025.
3. ↑ The Agda Wiki. MAlonzo-Unterseite. Abgerufen am 12. Mai 2025.
4. ↑ Documentation for the Agda standard library. Abgerufen am 12. Mai 2025.
5. ↑ Agda-Dokumentation. Emacs-Mode. Abgerufen am 12. Mai 2025.
6. ↑ Cornelis. Github-Seite. Abgerufen am 12. Mai 2025.
7. ↑ Agda-Mode for VSCode. Visual Studio Marketplace. Abgerufen am 12. Mai 2025.
8. ↑ Agdapad. Online-Emacs mit Agdamode. Abgerufen am 12. Mai 2025.