Agda

Niet te verwarren met Ada (programmeertaal).

Agda is een afhankelijk getypeerde functionele programmeertaal, oorspronkelijk ontwikkeld door Ulf Norell aan de Technische Universiteit Chalmers. Agda is niet Turingvolledig.

Agda
Paradigma	zuiver functioneel programmeren
Verschenen	2007 (16 jaar)
Ontwerper	Ulf Norell, Catarina Coquand
Ontwikkelaar	Ulf Norell, Catarina Coquand
Huidige versie	2.7.0.1 (12 september 2024)
Typesysteem	sterke typering, manifest typering, afhankelijke typering, statisch typesysteem, nominatief typesysteem, type-inferentie
Beïnvloed door	Coq, Epigram, Haskell
Invloed op	Idris (programmeertaal)
Besturings­systeem	Platform-onafhankelijke software
Licentie	BSD-licentie
Bestands­extensies	agda, lagda
Website	(en) Projectpagina
Portaal    Informatica

Agda is een bewijsassistent gebaseerd op het propositions-as-types paradigma, maar heeft in tegenstelling tot Coq geen aparte tactiektaal. Bewijzen worden geschreven in een functionele programmeerstijl. De taal heeft gebruikelijke programmeerconstructies zoals datatypes, pattern matching, records, let expressies en modules, en een Haskell-achtige syntaxis. Het systeem heeft interfaces voor Emacs, Atom en VS Code, maar kan ook in batchmodus worden uitgevoerd vanaf de commandoregel.

Agda is gebaseerd op Zhaohui Luo's unified theory of dependent types (UTT), een typetheorie die lijkt op de Martin-Löf typetheorie.

Kenmerken

Metavariabelen

Een van de onderscheidende kenmerken van Agda, vergeleken met andere vergelijkbare systemen zoals Coq, is de grote afhankelijkheid van metavariabelen voor programmaconstructie. Je kunt bijvoorbeeld functies als deze schrijven in Agda:

 add : ℕ → ℕ → ℕ
 add x y = ?

Hier is ? een metavariabele. Bij interactie met het systeem in emacs-modus wordt het verwachte type aan de gebruiker getoond en kan deze de metavariabele verfijnen, d.w.z. vervangen door meer gedetailleerde code. Deze functie maakt incrementele programmaconstructie mogelijk op een manier die vergelijkbaar is met bewijsassistenten gebaseerd op tactieken, zoals Coq.

Termination checking

Agda is een totale functionele programmeertaal. Dat wil zeggen dat elk programma moet eindigen en dat alle mogelijke patronen moeten worden gematched. Zonder deze eigenschap wordt de logica achter de taal inconsistent en wordt het mogelijk om willekeurige beweringen te bewijzen.

Bewijsautomatisering

Programmeren in pure typetheorie brengt veel vervelende en repetitieve bewijzen met zich mee. Hoewel Agda geen aparte tactiektaal heeft, is het mogelijk om nuttige tactieken in Agda zelf te programmeren. Typisch werkt dit door een Agda-functie te schrijven die optioneel een bewijs van een interessante eigenschap retourneert. Een tactiek wordt dan geconstrueerd door deze functie uit te voeren tijdens typechecking.

Daarnaast heeft Agda ondersteuning voor automatisering via reflectie, om complexere tactieken te schrijven. Het reflectiemechanisme maakt het mogelijk om programmafragmenten te quoten in - of te unquoten uit - de abstracte syntaxisboom. De manier waarop reflectie wordt gebruikt is vergelijkbaar met de manier waarop Template Haskell werkt.

Unicode

Een van de meest opmerkelijke kenmerken van Agda, is een sterke afhankelijkheid van Unicode in de programmabroncode. De standaard emacs-modus gebruikt snelkoppelingen voor invoer, zoals \Sigma voor Σ.

Bronnen, noten en/of referenties