Agda

whoami

• Eduardo Jorge Barbosa
• Masters Student
• Effectful component-based programming: the case of time

Where does Agda fit in?

Where does Agda fit in?

• Formalise concepts - Programming language

record Semigroup (a : Set) : Set where
  field
    _⊛_ : a → a → a
    associative : ∀ a b c → (a ⊛ b) ⊛ c ≡ a ⊛ (b ⊛ c)

andSemigroup : Semigroup Bool
andSemigroup = record
  { _⊛_ = _∧_
  ; associative = andAssociative
  }

Where does Agda fit in?

• Formalise proofs - Proof assistant

andAssociative : ∀ a b c → (a ∧ b) ∧ c ≡ a ∧ (b ∧ c)
andAssociative false b c = refl
andAssociative true b c = refl

Agda

• Programming language
• Proof assistant

Types, in programming languages, are propositions, in intuitionistic logic, and objects of a cartesian closed category.

Types as propositions, programs as proofs

• Curry-Howard isomorphism
• Curry-Howard-Lambek correspondence

Types as propositions, programs as proofs

• Types = Propositions
• Programs = Proofs

Logic vs Haskell vs Agda

a ∨ b	Either a b	Either A B
a ∧ b	(a, b)	A × B
a => b	a -> b	A → B
a <=> b	isomorphism	isomorphism
False	Void	False
True	()	True
¬a	a -> Void	A → False
∀	forall	Π
∃	clever trick	Σ

Why not Haskell?

Haskell’s type system

Corresponds to propositional logic

Is inconsistent as a logic

f :: a -> b
f = unsafeCoerce

what :: a -> b
what = undefined

Functions can be non-terminating

let brexit = brexit

Agda introduction

Agda is a dependently typed language with pure, total functions.

Meaning

Pure functions

The same inputs yield the same outputs (no side effects)

Meaning

Total

Functions must terminate and be defined for every possible input

-- Brilliant example by Conor McBride
brexit : ⊥
brexit = brexit

Meaning

Dependently typed

Types may depend on values

+-identityʳ : (m : ℕ) → m + zero ≡ m

Syntax

Set

The type of all boring types

Bool : Set
Nat : Set
List Bool : Set

• Haskell’s * (or TYPE)

Bool :: *
Int :: *
[Bool] :: *

Algebraic data types

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

• GADTs in Haskell

Algebraic data types

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

• GADTs in Haskell

{-# LANGUAGE GADTs #-}

data Nat = Zero | Suc Nat

data Nat where
  Zero :: Nat
  Suc  :: Nat -> Nat

A simple function

×-comm : (A : Set) → (B : Set) → (A × B) → (B × A)
×-comm A B (a , b) = (b , a)

A simple function

×-comm : (A B : Set) → (A × B) → (B × A)
×-comm A B (a , b) = (b , a)

A simple function

×-comm : (A B : Set) → (A × B) → (B × A)
×-comm _ _ (a , b) = (b , a)

• Haskell’s version

x-comm :: (a, b) -> (b, a)
x-comm (a, b) = (b, a)

Postulate

postulate A B : Set

×-comm : (A × B) → (B × A)
×-comm (a , b) = (b , a)

Implicit arguments

×-comm : {A B : Set} → (A × B) → (B × A)
×-comm (a , b) = (b, a)

Implicit types

×-comm : {A B : Set} → ...

Implicit types

×-comm : {A B : Set} → ...

×-comm : {A B : _} → ...

×-comm : ∀ {A B} → ...

Operators

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)

 3 + 4
 3 +_

if_then_else_ : {A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

Practice!

Records

record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

make-pair : {A B : Set} → A → B → Pair A B
make-pair a b = record { fst = a ; snd = b }

make-pair : {A B : Set} → A → B → Pair A B
make-pair a b = a , b

proj₁ : {A B : Set} → Pair A B → A
proj₁ p = Pair.fst p

proj₁ : {A B : Set} → Pair A B → A
proj₁ record { fst = a } = p

Co-pattern matching

p23 : Pair Nat Nat
p23 = record { fst = 2; snd = 3 }

p23 : Pair Nat Nat
Pair.fst p23 = 2
Pair.snd p23 = 3

Co-pattern and pattern matching

record Pair (A B : Set) : Set where
  field
    fst : A
    snd : B

make-pair : {A : Set} → ℕ → A → Pair ℕ A
Pair.fst (make-pair 0 _) = 4
Pair.fst (make-pair (suc x) _) = x
Pair.snd (make-pair _ y) = y

Many useful concepts…

• Co-induction
• Reflection
• Rewriting

Universe levels

Set

The type of all boring types

• Haskell’s * (or TYPE)

Bool : Set
Nat : Set
List Bool : Set

From the Russell’s paradox follows

• The collection of all sets is not itself a set

This is inconsistent

Set : Set

Explicit universe levels to the rescue

Int  : Set
Set  : Set₁
Set₁ : Set₂
Set₂ : Set₃
...

Universe Polymorphism

data List {n : Level} (A : Set n) : Set n where
  []   : List A
  _::_ : A → List A → List A

List Nat : Set
List Set : Set₁
List Set₁ : Set₂

Dependent types

Types may depend on values!

Type checking

• Values are allowed in dependent types
• Equality of dependent types may require computations
• Deciding type equality may involve deciding whether two arbitrary programs produce the same result
• Type checking can be undecidable!

It’s decidable in Agda

• Force all programs to terminate

Back to the good stuff

First-order logic, quantifiers and oh my

Logic

• First-order predicate logic extends propositional logic
• Propositions may depend on terms

Universal quantifiers (Π-type)

(a : A) → B

An example

p : (n : ℕ) → n >= zero

There’s already notation but…

data Π (A : Set) (B : A → Set) : Set where
  Λ : ((a : A) → B a) → Π A B

Existential quantifier (Σ-type)

Dependent products

data Σ (A : Set) (B : A → Set) : Set where
  ⟨_,_⟩ : (x : A) → B x → Σ A B

An example

dif : (m : ℕ) → (n : ℕ)
    → m >= n
    → Σ ℕ (λ r → m ≡ (n + r))

Quintessential example

Vector

data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)

• Indexed data type

Dependent pattern matching

head : ∀ {n} {A : Set} → Vec A (suc n) → A
head (x ∷ _) = x

Small example

CP with Agda?

Some auxiliary definitions

record True : Set where

data _⊕_ (A B : Set) : Set where
  inl : A → A ⊕ B
  inr : B → A ⊕ B

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

uncurry : {A B C : Set} → (A → B → C) → A × B → C
uncurry f (x , x₁) = f x x₁

const : {A B : Set} → A → B → A
const x _ = x

-- [_||_] : {A B C : Set} → (A → C) → (B → C) → A ⊕ B → C
[ f || g ] (inl x) = f x
[ f || g ] (inr y) = g y

Polynomial Functors

data Functor : Set₁ where
  |Id|  : Functor
  |K|   : Set → Functor
  _|+|_ : Functor → Functor → Functor
  _|*|_ : Functor → Functor → Functor

|1| = |K| True

Polynomial Functors

map : (F : Functor) {X Y : Set} → (X → Y) → [ F ] X → [ F ] Y
map |Id| f x = f x
map (|K| A) f x = x
map (F |+| G) f (inl x) = inl (map F f x)
map (F |+| G) f (inr x) = inr (map G f x)
map (F |*| G) f (x , y) = map F f x , map G f y

Decode function

[_] : Functor → Set → Set
[ |Id| ] X = X
[ |K| A ] X = A
[ F |+| G ] X = [ F ] X ⊕ [ G ] X
[ F |*| G ] X = [ F ] X × [ G ] X

Least fixed point

data μ_ (F : Functor) : Set where
  <_> : [ F ] (μ F) → μ F

Lists

ListF = λ A → |1| |+| (|K| A) |*| |Id|
List = λ A → μ (ListF A)

nil : {A : Set} → List A
nil = < inl _ >

cons : {A : Set} → A → List A → List A
cons x xs = < inr (x , xs) >

Catamorphisms

cata : (F : Functor) {A : Set} → ([ F ] A → A) → μ F → A
cata F φ < x > = φ (map F (cata' F φ) x)

• Can’t verify termination!

Catamorphisms

mapCata : ∀ {X} F G → ([ G ] X → X) → [ F ] (μ G) → [ F ] X
mapCata |Id| G φ < x > = φ (mapCata G G φ x)
mapCata (|K| A) G φ x = x
mapCata (F |+| F₁) G φ (inl x) = inl (mapCata F G φ x)
mapCata (F |+| F₁) G φ (inr x) = inr (mapCata F₁ G φ x)
mapCata (F |*| F₁) G φ (x , x₁) =
  mapCata F G φ x , mapCata F₁ G φ x₁

⟨|_|⟩ : ∀ {F : Functor} {A : Set} → ([ F ] A → A) → μ F → A
⟨|_|⟩ {F} φ < x > = φ (mapCata F F φ x)

Foldr

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr f acc  = ⟨| φ |⟩ where
  φ = [ const acc || uncurry f ]

Foldr = id

foldr=id' : ∀ {A} → (L : List A) → foldr cons nil L ≡ id L
foldr=id' < inl _ > = refl
foldr=id' < inr (x , xs) > with foldr=id xs
foldr=id' < inr (x , < x₁ >) > | z =
  cong (λ r → < inr (x , r) >) z

Thank you!