Agda is a dependently typed functional programming language based on intuitionistic type theory. Type theory is concerned both with programming and logic.
Agda is an extension of Martin-Löf’s type theory, and is the latest in the tradition of languages developed in the programming logic group at Chalmers. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Other languages in this tradition are Alf, Alfa, Agda 1, Cayenne. Some other loosely related languages are Coq, Epigram, and Idris.
This language is also a proof assistant based on the propositions-as-types paradigm, but has no separate tactics language, and proofs are written in a functional programming style.
Agda is open-source and enjoys contributions from many authors. The center of the Agda development is the Programming Logic group at Chalmers and Gothenburg University.
Here’s our recommended tutorials to learn Agda.
1. Dependently Typed Programming in Agda by Ulf Norell and James Chapman
This tutorial begins with an introduction to the basic features of Agda and how they can be employed in the construction of dependently typed programs. The authors then move on to describe and exemplify a couple of programming techniques which are made available in dependently typed languages: views and universe constructions.
The final part deals with the topic of getting Agda programs to interact with the real world.
2. Lectures by Thorsten Altenkirch
This is a computer aided formal reasoning course.
3. Dependent Types at Work by Ana Bove and Peter Dybjer
The authors give an introduction to functional programming with dependent types. They use the dependently typed programming language Agda which is an extension of Martin-L ̈of type theory. First they show how to do simply typed functional programming in the style of Haskell and ML. Some differences between Agda’s type system and the Hindley-Milner type system of Haskell and ML are also discussed.
Then they show how to use dependent types for programming and we explain the basic ideas behind type-checking dependent types. They go on to explain the Curry-Howard identification of propositions and types. This is what makes Agda a programming logic and not only a programming language. According to Curry-Howard, we identify programs and proofs, something which is possible only by requiring that all program terminate. However, at the end of these notes they present a method for encoding partial and general recursive functions as total functions using dependent types.
4. Interactive Theorem Proving for Agda Users by Anton Setzer
This material contains the slides of the module “Interactive Theorem Proving”, a third year/postgraduate course held at Swansea University, with a guide to material specifically directed at Agda.
5. Agda: Equality by Andreas Abel
Agda has an internal notion of program equality. In essence, two programs are equal ifthey compute the same value
6. Agda Tutorial by Péter Diviánszky
This tutorial covers general information, sets, functions, modules and records, applications, and coinduction.
7. Introduction to Dependent Types in Agda by Jan Malakhovski
This material does not aim to teach Agda, but to show how dependently typed languages work behind the scenes without actually going behind the scenes.
8. Dependently Typed Programming in Agda by Daniel Licata
The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
All tutorials in this series:
| Free Programming Tutorials | |
|---|---|
| ABAP | Advanced Business Application Programming |
| Ada | ALGOL-like programming language, extended from Pascal and others |
| Agda | Dependently typed functional language based on intuitionistic type theory |
| Alice | Educational language with an integrated development environment |
| Arduino | Inexpensive, flexible, open source microcontroller platform |
| Assembly | As close to writing machine code without writing in pure hexadecimal |
| Awk | Versatile language designed for pattern scanning and processing |
| Bash | ‘Bourne-Again-SHell’ is both a shell and programming language |
| BASIC | Family of general-purpose, high-level programming languages |
| C | General-purpose, procedural, portable, high-level language |
| C++ | General-purpose, portable, free-form, multi-paradigm language |
| C# | Combines the power and flexibility of C++ with the simplicity of Visual Basic |
| Chapel | Parallel-programming language in development at Cray Inc. |
| Clojure | Dialect of the Lisp programming language |
| ClojureScript | Compiler for Clojure that targets JavaScript |
| COBOL | Common Business-Oriented Language |
| CoffeeScript | A very succinct programming language that transcompiles into JavaScript |
| Coq | Dependently typed language similar to Agda, Idris, F*, Lean, and others |
| Crystal | General-purpose, concurrent, multi-paradigm, object-oriented language |
| CSS | CSS (Cascading Style Sheets) specifies a web page’s appearance |
| D | General-purpose systems programming language with a C-like syntax |
| Dart | Client-optimized programming language for fast apps |
| Dylan | Multi-paradigm language, supports functional & object-oriented programming |
| ECMAScript | Best known as the language embedded in web browsers |
| Eiffel | Object-oriented language |
| Elixir | Relatively new functional language that runs on the Erlang virtual machine |
| Elm | Functional language that compiles to JavaScript |
| Emacs Lisp | A dialect of the Lisp programming language. |
| Erlang | General-purpose, concurrent, declarative, functional language |
| F# | General purpose, strongly typed, multi-paradigm language. Part of ML |
| Factor | Dynamic stack-based language |
| Forth | Imperative stack-based programming language |
| Fortran | The first high-level language, using the first compiler |
| Go | Compiled, statically typed programming language |
| Groovy | Powerful, optionally typed and dynamic language |
| Hack | For the HipHop Virtual Machine (HHVM), created as a dialect of PHP |
| Haml | HTML Abstraction Markup Language |
| Haskell | Standardized, general-purpose, polymorphically, statically typed language |
| HTML | HyperText Markup Language |
| Icon | High-level, general-purpose language |
| Imba | Full-stack language that compiles to performant JavaScript |
| J | Array programming language based primarily on APL |
| Java | General-purpose, concurrent, class-based, object-oriented, high-level language |
| JavaScript | Interpreted, prototype-based, scripting language |
| Julia | High-level, high-performance language for technical computing |
| Kotlin | Statically typed, general-purpose programming language with type inference |
| LabVIEW | Designed to enable domain experts to build power systems quickly |
| LaTeX | Professional document preparation system and document markup language |
| Less | Backwards-compatible language extension for Cascading Style Sheets |
| Limbo | Designed for applications running distributed systems on small computers |
| Lisp | Unique features - excellent to study programming constructs |
| Logo | Dialect of Lisp that features interactivity, modularity, extensibility |
| Lua | Designed as an embeddable scripting language |
| Markdown | Plain text formatting syntax designed to be easy-to-read and easy-to-write |
| Nim | Statically typed compiled systems language with syntax resembling Python |
| Objective-C | General purpose language which is a superset of C |
| OCaml | General-purpose, powerful, high-level language |
| Octave | High-level language, primarily intended for numerical computations |
| OpenCL | Open Computing Language |
| Pascal | Imperative and procedural language designed in the late 1960s |
| Perl | High-level, general-purpose, interpreted, scripting, dynamic language |
| Pike | Interpreted, general-purpose, high-level, cross-platform, dynamic language |
| PHP | PHP has been at the helm of the web for many years |
| Pony | Pony is an actor-model, capabilities-secure, high-performance language |
| PostScript | Page description language in electronic and desktop publishing |
| Prolog | General purpose, declarative, logic programming language |
| PureScript | Small strongly, statically typed language with expressive types |
| Python | General-purpose, structured, powerful language |
| QML | Hierarchical declarative language for user interface layout with a syntax to JSON |
| R | De facto standard among statisticians and data analysts |
| Racket | Platform for programming language design and implementation |
| Raku | Member of the Perl family of programming languages |
| Ruby | General purpose, scripting, structured, flexible, fully object-oriented language |
| Rust | Ideal for systems, embedded, and other performance critical code |
| Scala | Modern, object-functional, multi-paradigm, Java-based language |
| Scheme | General-purpose, functional, language descended from Lisp and Algol |
| Scratch | Visual programming language designed for 8-16 year-old children |
| Solidity | Object-oriented, high-level language for implementing smart contracts |
| SQL | Access and manipulate data held in a relational database management system |
| Standard ML | One of the two main dialects of the ML language |
| Swift | Powerful and intuitive general-purpose programming language |
| Tcl | Dynamic language based on concepts of Lisp, C, and Unix shells |
| TypeScript | Strict syntactical superset of JavaScript, adding optional static typing |
| V | Statically typed compiled language to build maintainable software |
| Vala | Object-oriented language with a self-hosting compiler that generates C code |
| VHDL | Very High Speed Integrated Circuit Hardware Description Language |
| VimL | Powerful scripting language of the Vim editor |
| XML | Set of rules for defining semantic tags that describe the structure and meaning |