Agda is a research language developed at Chalmers University of Technology, in Gothenburg, Sweden, and attributed to several authors, including Catarina Coquand, Makoto Takeyama, Ulf Norell, Andreas Able, and others.
However, Agda 2, released in 2007, was a complete rewrite of the 1999 Agda 1 language.
Commonly, Agda programmers use the Emacs text editor as a basic IDE. Text is entered into a buffer in Emacs, then the text in the buffer is sent to Agda for type and proof checking. An advantage of using Emacs for Agda is that they both support the use of Unicode characters. The Agda mode for Emacs recognizes certain names that begin with a backslash, as they are typed. It then converts them to the special symbol associated with those names.
For example, when a programmer types \all into Emacs in Agda mode, Emacs will change it to ∀, which is the logical symbol used when expressing that "for all" elements of some particular type, some formula is true.
It might take practice getting used to entering text in Unicode, but this is one of the more notable features of the language.
Agda is a dependently-typed functional programming language with inductive families; for example, data types that depend on values, such as the type of vectors of a given length. It also uses parameterized modules, mixfix operators, Unicode characters, and an interactive Emacs interface that can be used to facilitate the task of programming. Agda is an interactive system that is used for writing and checking proofs.
With Agda, there are no runtime errors. The inevitable errors, such as I/O errors, are handled, while others are excluded by design. There are no non-productive infinite loops. Functional properties may be formalized and proved, and proof checking is automatic.
Agda is an open-source language licensed under a BSD-type License. It can be installed on Linux, macOS, and Windows.
The focus of this category is on the Agda computer programming language. Topics that are strongly related to the language itself, to any of its versions or implementations, or to any editors or tools that have been designed specifically to facilitate programming in Agda, are appropriate for this category, as are any Agda user groups, forums, tutorials, guides, or other content.
Recommended Resources
Hosted by the Chalmers University of Technology, the site features Agda, a programming language developed at Chalmers. Presented in a Wiki format, the site presents a brief introduction to the language, stating its history, purpose, and features, and posting development notes, links to language tutorials, installation instructions, other documentation, and community support resources. A schedule of meetings relating to the continued development of the language is included.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Presented by Eötvös Loránd University in Hungary, the tutorial offers general information about the programming language, including the design goals, installation instruction, and Emacs usage, as well as instruction and example in the use of sets, functions, modules, and records, and coinduction. Applications for which the language is used are identified, with examples and code snippets. The use of the Agda programming language in the verification of proofs is included.
https://people.inf.elte.hu/divip/AgdaTutorial/
Learn You an Agda and Achieve Enlightenment
Written by the author of Learn You a Haskell, the author makes comparisons between the Agda and Haskell programming languages and suggests that the first step in learning Agda should be to learn Haskell, as learning a language in the ML family will make learning Agda easier. An introduction to the Agda language is given, followed by some simple programming exercises in Agda. Next, some arithmetic operations are defined, and the author describes how go get Agda to check the user’s code.
http://learnyouanagda.liamoc.net/
OXIJ: Brutal [Meta] Introduction to Dependent Types in Agda
Jan Malakhovski offers an introduction to the Agda programming languages, including recommendations of tutorials and other introductions written by others, as well as to the language itself. Intended to be a basic introduction to the language, its chief purpose is to show how dependently typed languages work behind the scenes, and how Agda does this better than most. The steps required to install Agda in the Emacs editor is included, with instruction in syntax
https://oxij.org/note/BrutalDepTypes/
Programming Language Foundations in Agda
Licensed under a Creative Commons Attribution International License, and hosted on GitHub, this is an online version of a book on programming language theory using the proof assistant Agda. Written by Philip Wadler, Wen Kokke, and Jeremy Siek, the book includes a dedication, preface, a chapter on logical foundations and another on programming language foundations, both with sub-sections, as well as acknowledgments, a test page for fonts, and statistics.
https://plfa.github.io/
Read the Docs is a large, community-supported repository of software documentation. Here, the full documentation for version 2.6.0.1 of the Agda programming language is published. Sorted into chapters and sub-chapters, the documentation offers an overview of the language, instructions for getting started with Agda programming, language references, tools, information about the documentation, the Agda Team, and its licensure. Instructions are supplemented by code examples.
https://agda.readthedocs.io/en/v2.6.0.1/
