Intro To Agda

Intro to Agda

by Larry Diehl (larrytheliquid)

induction centric

data Nat : Set where
zero : Nat
suc : Nat -> Nat

one = suc zero
two = suc (suc zero)

unicode centric

data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ

suc₂ : ℕ → ℕ
suc₂ n = suc (suc n)

unicode in emacs

r →
bn ℕ
:: ∷
member ∈
equiv ≡
and ∧
or ∨
neg ¬
ex ∃
all ∀

built-ins

data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

nine = suc₂ 7

standard library

open import Data.Nat

infix & pattern matching

infixl 6 _+_
infixl 7 _*_
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + m * n

emacs goal mode

_+_ : ℕ → ℕ → ℕ
n+m=?

_+_ : ℕ → ℕ → ℕ
n + m = {!!}

_+_ : ℕ → ℕ → ℕ
n + m = { }0
-- ?0 : ℕ

coverage checking

data Day : Set where
Sunday Monday Tuesday : Day
Wednesday Thursday : Day
Friday Saturday : Day

isWeekend : Day → Bool
isWeekend Sunday = true
isWeekend Saturday = true
isWeekend _ = false

termination checking (fail)

isWeekend day = isWeekend day

isWeekend Sunday = true
isWeekend Saturday = isWeekend Sunday
isWeekend _ = false

termination checking (win)

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

_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + m * n

data type polymorphism

data List (A : Set) : Set where
[] : List A
_∷_ : (x : A) (xs : List A) → List A

-- open import Data.List

type-restriction

append : List ℕ → List ℕ → List ℕ
append [] ys = ys
append (x ∷ xs) ys = x ∷ (append xs ys)

parametric polymorphism

append : (A : Set) → List A → List A → List A
append A [] ys = ys
append A (x ∷ xs) ys = x ∷ (append A xs ys)

implicit arguments

append : {A : Set} → List A → List A → List A
append [] ys = ys

-- append = _++_

indexed types

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

bool-vec : Vec Bool 2
bool-vec = _∷_ {1} true
(_∷_ {0} false [])

bool-vec : Vec Bool 2
bool-vec = true ∷ false ∷ []

indexed types

append : {n m : ℕ} {A : Set} → Vec A n →
Vec A m → Vec A (n + m)
append [] ys = ys

coverage checking

head : {A : Set} → Vec A 9 → A
head (x ∷ xs) = x

head : {n : ℕ} {A : Set} → Vec A (suc n) →
A
head (x ∷ xs) = x

head : {n : ℕ} {A : Set} →
Vec A (1 + 1 * n) → A
head (x ∷ xs) = x

records

record Car : Set where
field
    make : Make
    model : Model
    year : ℕ

electricCar : Car
electricCar = record {
    make = Tesla
; model = Roadster
; year = 2010
}

records

record Car : Set where
constructor _,_,_
field
    make : Make
    model : Model
    year : ℕ

electricCar : Car
electricCar = Tesla , Roadster , 2010
carYear : ℕ
carYear = Car.year electricCar

truth & absurdity

record ⊤ : Set where
data ⊥ : Set where

T : Bool → Set
T true = ⊤
T false = ⊥

preconditions

even : ℕ → Bool
even zero = true
even (suc zero) = false
even (suc (suc n)) = even n

evenSquare : (n : ℕ) → {_ : T (even n)} → ℕ
evenSquare n = n * n

preconditions

nonZero : ℕ → Bool
nonZero zero = false
nonZero _ = true

postulate _div_ : ℕ → (n : ℕ) →
{_ : T (nonZero n)} → ℕ

propositional equality

infix 4 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x

testMultiplication : 56 ≡ 8 * 7
testMultiplication = refl

preconditions

lookup : {A : Set}(n : ℕ)(xs : List A)
{_ : T (n < length xs)} → A
lookup n []{()}
lookup zero (x ∷ xs) = x
lookup (suc n) (x ∷ xs) {p} = lookup n xs {p}

testLookup : 2 ≡ lookup 1 (1 ∷ 2 ∷ [])
testLookup = refl

finite sets

data Fin : ℕ → Set where
zero : {n : ℕ} → Fin (suc n)
suc : {n : ℕ} (i : Fin n) → Fin (suc n)

finTest : Fin 3
finTest = zero

finTest₂ : Fin 3
finTest₂ = suc (suc zero)

precondition with indexes

lookup : {A : Set}{n : ℕ} → Fin n → Vec A n → A
lookup zero (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs

testLookup : 2 ≡ lookup (suc zero) (1 ∷ 2 ∷ [])
testLookup = refl

testLookup₂ : 2 ≡ lookup (fromℕ 1) (1 ∷ 2 ∷ [])
testLookup₂ = refl

with

doubleOrNothing :ℕ→ℕ
doubleOrNothing n with even n
doubleOrNothing n | true = n * 2
doubleOrNothing n | false = 0

doubleOrNothing :ℕ→ℕ
doubleOrNothing n with even n
... | true = n * 2
... | false = 0

views

parity : (n : ℕ) → Parity n
parity zero = even zero
parity (suc n) with parity n
parity (suc .(k * 2)) | even k = odd k
parity (suc .(1 + k * 2)) | odd k = even (suc k)

half :ℕ→ℕ
half n with parity n
half .(k * 2) | even k = k
half .(1 + k * 2) | odd k = k

inverse

data Image_∋_ {A B : Set}(f : A → B) :
B → Set where
im : {x : A} → Image f ∋ f x

inv : {A B : Set}(f : A → B)(y : B) →
Image f ∋ y → A
inv f .(f x) (im {x}) = x

inverse

Bool-to-ℕ : Bool → ℕ
Bool-to-ℕ false = 0
Bool-to-ℕ true = 1

testImage : Image Bool-to-ℕ ∋ 0
testImage = im
testImage₂ : Image Bool-to-ℕ ∋ 1
testImage₂ = im

testInv : inv Bool-to-ℕ 0 im ≡ false
testInv = refl
testInv₂ : inv Bool-to-ℕ 1 im ≡ true
testInv₂ = refl

intuitionistic logic

data _∧_ (A B : Set) : Set where
<_,_> : A → B → A ∧ B

fst : {A B : Set} → A ∧ B → A
fst < a , _ > = a
snd : {A B : Set} → A ∧ B → B
snd < _ , b > = b


data _∨_ (A B : Set) : Set where
left : A → A ∨ B
right : B → A ∨ B

case : {A B C : Set} → A ∨ B → (A → C) →
(B → C) → C
case (left a) x _ = x a
case (right b) _ y = y b


record ⊤ : Set where
constructor tt

data ⊥ : Set where

exFalso : {A : Set} → ⊥ → A
exFalso ()

¬ : Set → Set
¬A=A→⊥


_=>_ : (A B : Set) → Set
A => B = A → B

modusPonens : {A B : Set} → A => B → A → B
modusPonens f a = f a

_<=>_ : Set → Set → Set
A <=> B = (A => B) ∧ (B => A)


∀′ : (A : Set)(B : A → Set) → Set
∀′ A B = (a : A) → B a

data ∃ (A : Set)(B : A → Set) : Set where
exists : (a : A) → B a → ∃ A B

witness : {A : Set}{B : A → Set} → ∃ A B → A
witness (exists a _) = a


data Man : Set where
person : Man

isMan : Man → Set
isMan m = ⊤

isMortal : Man → Set
isMortal m = ⊤

socratesIsMortal : {Socrates : Man} →
(∀′ Man isMortal ∧ isMan Socrates) => isMortal Socrates
socratesIsMortal {soc} < lemma , _ > = lemma soc

The End

Agda Wiki
http://is.gd/8YgYM

Dependently Typed Programming in Agda
http://is.gd/8Ygyz

Dependent Types at Work
http://is.gd/8YggR

lemmatheultimate.com

Intro To Agda

More Related Content

What's hot

Similar to Intro To Agda

Recently uploaded

Intro To Agda