Correct by Construction Programming in Agda
In a dependently typed programming language you can get much stronger static guarantees about the correctness of your program than in most other languages. At the same time, dependent types enable new forms of interactive programming, by letting the types guide the construction of the program. Dependently typed languages have existed for many years, but only recently have they become usable for practical programming.
In this course, you will learn how to write correct-by-construction programs in the dependently typed programming language Agda. Concretely, we will together implement a verified typechecker and interpreter for a small C-like imperative language. Along the way, we will explore several modern features of the Agda language that make this task more pleasant, such as dependent pattern matching, monads and do-notation, coinduction and copattern matching, instance arguments, sized types, and the Haskell FFI.
For the exercises in this course, you need to install Agda 220.127.116.11., the Agda standard library v1.1, and the BNFC tool.
If you are brave, there is a bash script that installs all of these on a fresh installation of Ubuntu 18.04 or later. Alternatively, below are step-by-step instructions.
Installing Agda on Ubuntu
First, make sure you have git, cabal, and emacs installed. You also
zlib c library. On Ubuntu and related systems, the
following command should work:
sudo apt-get install git cabal-install emacs zlib1g-dev
Make sure that binaries installed by
cabal are available on your
path by adding the following line to
Now install Agda and its prerequisites:
cabal update cabal install alex happy cabal get Agda && cd Agda-18.104.22.168 && cabal install agda-mode setup
Installing Agda on Mac
Follow the instructions in the user manual. Alternatively, you can install the Haskell Platform and follow the instructions above.
Installing Agda on Windows
Follow the instructions by Péter Diviánszky. Alternatively, install a virtual machine with Ubuntu and follow the instructions above.
Installing the standard library
To install the Agda standard library:
git clone https://github.com/agda/agda-stdlib.git cd agda-stdlib && git checkout v1.1 && cabal install mkdir $HOME/.agda echo $PWD/standard-library.agda-lib >> $HOME/.agda/libraries echo standard-library >> $HOME/.agda/defaults
cabal install BNFC
During the exercise sessions, your first goal should be to install Agda (see above for instructions) and make yourself familiar with the Emacs mode to navigate around in the code. Some useful commands:
- C-c C-l: typecheck and highlight the current file
- C-c C-d: deduce the type of an expression
- C-c C-n: evaluate an expression to normal form
- C-c C-,: get information about the hole under the cursor
- C-c C-space: give a solution
- C-c C-r: refine the hole
- Introduce a lambda or constructor
- Apply given function to some new holes
- C-c C-c: case split on a variable
See the Agda documentation for further information. The important parts of the code are the following:
- While.cf contains the BNF grammar of the language.
- AST.agda contains the raw (untyped) syntax representation.
- Parser.agda contains bindings to the Haskell parser generated by BNFC.
- WellTypedSyntax.agda contains the intrinsically well-typed syntax representation.
- TypeChecker.agda contains the typechecker, converting from raw to well-typed syntax.
- Interpreter.agda contains an interpreter for well-typed syntax.
- runwhile.agda contains the main program.
Once you are familiar with (a part of) the codebase, you can try to extend the language in a way of your choice. Some suggestions:
- (V1) Add more operations on booleans, e.g. negation
- (V1) Add more operations on integer, e.g. minus
- (V1) Add an equality test
==that works both on booleans and integers.
- (V2) Add additional assignment operators to the language, e.g.
x += e;,
- (V2) Add uninitialized variables to the language (
int x;instead of
int x = 5;), and make sure the typechecker produces an error message when a variable is used before it is initialized.
- (V3) Add more control operators to the language, e.g.
- (any) Add more types to the language, e.g.
float, and add appropriate syntactic constructions for literals, e.g.
- (any) Add the ability to define and call additional functions apart from
- Agda documentation
- An introduction to dependent types in Agda by Andreas Abel
- Agda tutorial by Péter Diviánszky
- Dependently typed programming in Agda (video lectures) by Conor McBride
- Programming language foundations in Agda (online book)
- Type-driven development in Idris (book)
- Certified programming with dependent types (book)