Agda Fundamentals: (I / 1)
Ivan Molina Rebolledo 5 min read
Abstract
The following article is part of some meetings discussing Dependent Types between people in my college. I hope it can also be useful to someone else. Either way, this is just the «article» version of a couple of md slides that I made for it.
Some parts borrowed from Philip Wadler's PLFA
Hello. So I work in functional programming, where’d you guys work in the real world. I’m an academic.
— Philip Wadler
What is Agda?

Agda 1.0 ≠ Agda 2.0

Agda is a dependently typed functional programming language.

Agda is a proof assistant.

A language that has certain roots on Haskell.
The language itself
Builtins
 The unit type
 The Σtype
 Booleans
 Natural numbers
 Machine words
 Integers
 Floats
 Lists
 $\dots$
But none of these matters right now!
Let's review the syntax though.
Variables
The pattern is trivial and it's demonstration is left as an exercise for the reader \( ^{_{\text{just kidding}}} \).
$$[variable] : [type] $$ $$ [variable] = [value]$$
variable : Nat  Agda
variable = 2
variable :: Integer  Haskell
variable = 2
let variable: i32; // Rust
variable = 2;
variable: int #Python
variable = 2
And now the most ugliest one...
int variable; // C / Java / C++
variable = 2
Functional programming like in Functions
A function in Agda is similar to those that we can find in Haskell:
_! : ℕ → ℕ  Agda
0 ! = 1
(suc n) ! = (suc n) * (n !)
factorial :: Integer > Integer  Haskell
factorial 0 = 1
factorial n = n * (n  1)
There are four main differences between the function declaration in Haskell and Agda:
 Function parameters in Agda can be prefixes or suffixes.
 We use only one colon to declare the types of the function.
 Unicode! It looks prettier to have
→
instead of>
 And for naming too! (Whereas ℕ means for Natural)
However
We can declare the function just like in Haskell:
factorial : Nat > Nat  This is Agda
factorial 0 = 1
factorial n = n * (n  1)
You have freedom, use it as whatever you want.
Just as a fact, the signature of the codeblocks in this slides for Agda are defined as Haskell since there is not default syntax highlighting for Agda; and it works.
Similar to:
fn factorial(n: i32) > i32 { // Rust
match n {
0 => 1,
n => n * factorial(n  1)
}
}
int factorial(int n) { // C, I think.
switch (n) {
case 0:
return 0;
case n:
return n * factorial(n  1);
}
}
I don't even know if the C function actually works, but you get the point. However, surprisingly Java (since 14 or 15) has a prettier syntax for switch like the one in Rust.
Python
def factorial(n: int) > int:
match n:
case 0: return 1;
case n: return (n * factorial(n  1));
PEP 636  Structural Pattern Matching. It doesn't exist yet.
def factorial(n: int) > int:
if (n == 0):
return 1;
else:
return n * factorial(n  1);
But this works!
Curry
Haskell and Agda, unlike Rust or other languages, in theory can have just one parameters in a function. That's where currying comes in hand.
We have chosen to represent a function of two arguments in terms of a function of the first argument that returns a function of the second argument. This trick goes by the name currying.
Currying is named for Haskell Curry, after whom the programming language Haskell is also named. Curry’s work dates to the 1930’s.
The key is recursion!
While there are functional languages like F# or Rust (functionallikish), OCaml languages that support loops, Agda tries to be a little more like Haskell in terms of purity$^1$. So we don't have loops; recursion is our only friend.
 This does not imply that Agda is necessarily pure functional. It's a discutible topic. You can read more about it: https://semanticdomain.blogspot.com/2016/03/agdaisnotpurelyfunctionallanguage.html But that doesn't matter right now.
Algebraic Data Types
"Almost" every modern language has ADTs.
Let's talk about Natural Numbers
We know that
$$0 \in \mathbb{N}$$
so inductively, one can construct the natural numbers as successor on a value in the Natural set:
$$successor(0) \in \mathbb{N}$$
Agda
We can represent this in a simple way
data Nat : Set where
zero : Nat
suc : Nat → Nat
{# BUILTIN NATURAL Nat #}
So,
 zero = 0
 suc(zero) = 1
 suc(suc(zero)) = 2
 suc(suc(suc(...))) = ...
Haskell
data Nat
= Zero
 Suc(Nat)
Rust
enum Nat {
zero,
suc(Box<Nat>)
}
Rust it's not the topic right now, but the value is boxed because of memory management reasons. Unlike Haskell, Rust doesn't have a Garbage Collector. It's a pointer if you're wondering.
We'll be exploring Natural numbers later on.
The Set set.
Previously it was written in code that our Nat type is of the type Set. A type has a type!
About the universal set and Russell's paradox.
Since even types have types, we can't just say that Set is in Set, however, this is solved in a beautiful way:
$$Set \in Set_1 \in Set_2 \in \dots \in Set_n$$
Cool, isn't it?
Proving things
I don’t know about you, but when I try to write a proof I get sort of sad. Right. If I ever finish a proof, right, it’s exactly like a cat. Right. Cats are great, but, right, what does a cat do if just sort of lies around the house in the sun, and it says “hello, I’m a Cat. I’m very elegant; you should admire me”. […] Where I think programs are like dogs, right, what did dogs do [?] anything, huh, “hello master, what can I do for you?”. Right. Programs are great fun. So, I always get really excited about hacking. “Oh I get to sit down today and hack” I get really excited. But when I’m doing a proof “Hello. I’m doing a proof today, oh well” So the fact that they’re the same thing means now I could do my proofs by programming. Yay.
— Philip Wadler
Builtins?
I think that this topic is important, but we don't need to rush to much right now. Let's get first into the very basic: defining all by ourself.
We already defined the Natural numbers a few pages ago.
So, now it's time for
Agda in practice!
Agda in practice!
First let's make sure we have Agda correctly installed.
In macOS you can install Agda directly from Brew:
$ brew install agda
Ubuntu:
$ apt install agda
I don't know about other platforms, but if you have any problems you're not completely on your own; we can try something.
Now we need to test that all is installed correctly.
Let's make a file called nats.agda
with the following:
open import Data.Nat
ten : ℕ
ten = 10
Then run:
$ agda v 2 nats.agda
If there in not errors, then we should proceed.
IDE
Naturally one will use Emacs, but you can also use Vim or VS Code.
For vscode you can use the following extensions:
 agdamode
 languageagda
Have fun!
Natural Numbers
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
Here ℕ is the name of the datatype we are defining, and zero and suc (short for successor) are the constructors of the datatype.
Both definitions above tell us the same two things:
 Base case: zero is a natural number.
 Inductive case: if m is a natural number, then suc m is also a natural number.
Pragmas
In Agda, any text following  or enclosed between { and } is considered a comment. Comments have no effect on the code, with the exception of one special kind of comment, called a pragma, which is enclosed between {# and #}.
The pragma:
{# BUILTIN NATURAL ℕ #}
tells Agda that ℕ corresponds to the natural numbers, and it's representation.
Imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡Reasoning using (begin_; _≡⟨⟩_; _∎)
This imports brings tools that well need in order to verify equality.
How we can define the plus operator?
Hint: 3 + 1 = (2 + 1) + 1 = ((1 + 1) + 1) + 1 = \( \dots \)
Verify
We use Control + C, Control + L
Verify 2
_ : 2 + 3 ≡ 5
_ =
begin
2 + 3
≡⟨⟩
suc (1 + 3)
≡⟨⟩
suc (suc (0 + 3))
≡⟨⟩
suc (suc 3)
≡⟨⟩
5
∎
Here ∎ represents QED.
How we can define the times operator?
Hint: 3 * 1 = (2 * 1) + 1 = ((1 * 1) + 1) + 1 = \( \dots \)
How we can define the exponentiation operator?
Hint: 3 ^ 1 = (3 ^ 0) + 3
Now one more tricky:
How we can define the minus operator?
Hint: 3  2 = 2  1 = 1  0
Binary representation.
For the type
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
The following functions are left as an exercise for the reader.
inc : Bin → Bin
to : ℕ → Bin
from : Bin → ℕ
Thanks!
🤗
Slides: https://drive.google.com/file/d/1LFRA7xfxcyX5yFYPgiNb3PGbuJnHs6U/view?usp=sharing