Programming Tutorials

Excellent Free Tutorials to Learn Agda

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.

Read the tutorial


2. Lectures by Thorsten Altenkirch

This is a computer aided formal reasoning course.

Read the material


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.

Read the tutorial


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.

Read the tutorial


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

Read the tutorial


6. Agda Tutorial by Péter Diviánszky

This tutorial covers general information, sets, functions, modules and records, applications, and coinduction.

Read the tutorial


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.

Read the tutorial


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.

Watch the videos


All tutorials in this series:

Free Programming Tutorials
JavaGeneral-purpose, concurrent, class-based, object-oriented, high-level language
CGeneral-purpose, procedural, portable, high-level language
PythonGeneral-purpose, structured, powerful language
C++General-purpose, portable, free-form, multi-paradigm language
C#Combines the power and flexibility of C++ with the simplicity of Visual Basic
JavaScriptInterpreted, prototype-based, scripting language
PHPPHP has been at the helm of the web for many years
RubyGeneral purpose, scripting, structured, flexible, fully object-oriented language
AssemblyAs close to writing machine code without writing in pure hexadecimal
SwiftPowerful and intuitive general-purpose programming language
GroovyPowerful, optionally typed and dynamic language
GoCompiled, statically typed programming language
PascalImperative and procedural language designed in the late 1960s
PerlHigh-level, general-purpose, interpreted, scripting, dynamic language
RDe facto standard among statisticians and data analysts
COBOLCommon Business-Oriented Language
ScalaModern, object-functional, multi-paradigm, Java-based language
FortranThe first high-level language, using the first compiler
ScratchVisual programming language designed for 8-16 year-old children
LuaDesigned as an embeddable scripting language
LogoDialect of Lisp that features interactivity, modularity, extensibility
RustIdeal for systems, embedded, and other performance critical code
LispUnique features - excellent to study programming constructs
AdaALGOL-like programming language, extended from Pascal and others
HaskellStandardized, general-purpose, polymorphically, statically typed language
SchemeGeneral-purpose, functional, language descended from Lisp and Algol
PrologGeneral purpose, declarative, logic programming language
ForthImperative stack-based programming language
ClojureDialect of the Lisp programming language
JuliaHigh-level, high-performance language for technical computing
SQLAccess and manipulate data held in a relational database management system
ErlangGeneral-purpose, concurrent, declarative, functional language
VimLPowerful scripting language of the Vim editor
OCamlGeneral-purpose, powerful, high-level language
AwkVersatile language designed for pattern scanning and processing
RacketPlatform for programming language design and implementation
BASICFamily of general-purpose, high-level programming languages
CoffeeScriptA very succinct programming language that transcompiles into JavaScript
LaTeXProfessional document preparation system and document markup language
ElixirRelatively new functional language that runs on the Erlang virtual machine
DartClient-optimized programming language for fast apps
ABAPAdvanced Business Application Programming
F#General purpose, strongly typed, multi-paradigm language. Part of ML
ChapelParallel-programming language in development at Cray Inc.
DylanMulti-paradigm language, supports functional & object-oriented programming
DGeneral-purpose systems programming language with a C-like syntax
SolidityObject-oriented, high-level language for implementing smart contracts
XMLSet of rules for defining semantic tags that describe the structure and meaning
ValaObject-oriented language with a self-hosting compiler that generates C code
ECMAScriptBest known as the language embedded in web browsers
KotlinStatically typed, general-purpose programming language with type inference
TypeScriptStrict syntactical superset of JavaScript, adding optional static typing
MarkdownPlain text formatting syntax designed to be easy-to-read and easy-to-write
PikeInterpreted, general-purpose, high-level, cross-platform, dynamic language
HTMLHyperText Markup Language
FactorDynamic stack-based language
Objective-CGeneral purpose language which is a superset of C
Standard MLOne of the two main dialects of the ML language
AliceEducational language with an integrated development environment
AgdaDependently typed functional language based on intuitionistic type theory
IconHigh-level, general-purpose language
PureScriptSmall strongly, statically typed language with expressive types
Share this article

Share your Thoughts

This site uses Akismet to reduce spam. Learn how your comment data is processed.