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

Built-ins

  • 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 (functional-likish), 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.

  1. This does not imply that Agda is necessarily pure functional. It's a discutible topic. You can read more about it: https://semantic-domain.blogspot.com/2016/03/agda-is-not-purely-functional-language.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

Built-ins?

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 vs-code you can use the following extensions:

  • agda-mode
  • language-agda

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/1LFRA7xfxcyX5yFYPgiNb3PGb-uJnHs6U/view?usp=sharing