algprog/agda/algebra.lagda.md

```agda
open import equality
module algebra where
```

# Algebra of programming

## Preliminaries (Types, Lemmas, Functions)

```agda
  id : ∀ {A : Set} → A → A
  id a = a

  _! : ∀ {A B : Set} → (b : B) → A → B
  (b !) _ = b
```

We will need functional extensionality

```agda
  postulate
    extensionality : ∀ {A B : Set} (f g : A → B) → (∀ (x : A) → f x ≡ g x) → f ≡ g
  
  ext-rev : ∀ {A B : Set} {f g : A → B} → f ≡ g → (∀ (x : A) → f x ≡ g x)
  ext-rev {A} {B} {f} {g} refl x = refl
```

Function composition and some facts about it

```agda
  infixr 9 _∘_
  _∘_ : ∀ {A B C : Set} (g : B → C) (f : A → B) → A → C
  (g ∘ f) x = g (f x)
  {-# INLINE _∘_ #-}

  identityʳ : ∀ {A B : Set} {f : A → B} → f ∘ id ≡ f
  identityʳ {f} = refl

  identityˡ : ∀ {A B : Set} {f : A → B} → id ∘ f ≡ f
  identityˡ {f} = refl

  _⟩∘⟨_ : ∀ {A B C : Set} {g i : B → C} {f h : A → B} → g ≡ i → f ≡ h → g ∘ f ≡ i ∘ h
  refl ⟩∘⟨ refl = refl

  introˡ : ∀ {A B : Set} {f : A → B} {h : B → B} → h ≡ id → f ≡ h ∘ f
  introˡ {f} {h} eq = trans (sym identityˡ) (sym eq ⟩∘⟨ refl)

  introʳ : ∀ {A B : Set} {f : A → B} {h : A → A} → h ≡ id → f ≡ f ∘ h
  introʳ {f} {h} eq = trans (sym identityʳ) (refl ⟩∘⟨ sym eq)
```

## Unit and void type

```agda
  data ⊤ : Set where
    unit : ⊤

  data ⊥ : Set where

  ¡ : ∀ {B : Set} → ⊥ → B
  ¡ ()

  ¡-unique : ∀ {B : Set} → (f : ⊥ → B) → f ≡ ¡
  ¡-unique f = extensionality f ¡ (λ ())
```

## Products

```agda
  infixr 8 _×_
  infixr 7 _×₁_
  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      outl : A
      outr : B
  open _×_

  ×-cong : ∀ {A B : Set} {x y : A} {u v : B} → x ≡ y → u ≡ v → (x , u) ≡ (y , v)
  ×-cong refl refl = refl    

  ⟨_,_⟩ : {A B C : Set} → (A → B) → (A → C) → A → B × C
  ⟨ f , g ⟩ x = (f x) , (g x)
  project₁ : ∀ {A B C : Set} (f : A → B) (g : A → C) → outl ∘ ⟨ f , g ⟩ ≡ f
  project₁ _ _ = refl 
  project₂ : ∀ {A B C : Set} (f : A → B) (g : A → C) → outr ∘ ⟨ f , g ⟩ ≡ g
  project₂ _ _ = refl 

  ⟨⟩-cong : {A B C : Set} → (f g : A → B) → (h i : A → C) → f ≡ g → h ≡ i → ⟨ f , h ⟩ ≡ ⟨ g , i ⟩
  ⟨⟩-cong f g h i refl refl = refl

  ⟨⟩-unique : ∀ {A B C : Set} (f : A → B) (g : A → C) (h : A → B × C) → outl ∘ h ≡ f → outr ∘ h ≡ g → h ≡ ⟨ f , g ⟩
  ⟨⟩-unique f g h refl refl = refl

  _×₁_ : ∀ {A B C D : Set} (f : A → C) (g : B → D) → A × B → C × D
  _×₁_ f g (x , y) = f x , g y
```

Composition as function on products

```agda
  comp : ∀ {A B C : Set} → ((A → B) × (B → C)) → A → C
  comp (f , g) x = g (f x)
```

curry, uncurry, eval

```agda
  curry : ∀ {A B C : Set} → (A × B → C) → (A → B → C)
  curry f a b = f (a , b)

  uncurry : ∀ {A B C : Set} → (A → B → C) → (A × B → C)
  uncurry f (a , b) = f a b

  ev : ∀ {A B : Set} → (A → B) × A → B
  ev (f , a) = f a
```

**HOMEWORK 1**

```agda
  curry-uncurry : ∀ {A B C : Set} → curry ∘ uncurry {A} {B} {C} ≡ id
  curry-uncurry = extensionality (curry ∘ uncurry) id λ _ → refl

  uncurry-curry : ∀ {A B C : Set} → uncurry ∘ curry {A} {B} {C} ≡ id
  uncurry-curry = extensionality (uncurry ∘ curry) id λ _ → refl
```

## Naturals

```agda
  data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ
  {-# BUILTIN NATURAL ℕ #-}

  data 𝔹 : Set where
    true : 𝔹
    false : 𝔹
  {-# BUILTIN BOOL 𝔹 #-}
  
  succ-inj : ∀ {x y : ℕ} → succ x ≡ succ y → x ≡ y
  succ-inj refl = refl

  -- todo rewrite foldn to use ugly cartesian product...
  foldn : ∀ {C : Set} → (C × (C → C)) → ℕ → C
  foldn (c , h) zero = c
  foldn (c , h) (succ n) = h (foldn (c , h) n)

  foldn-id : foldn (zero , succ) ≡ id {ℕ}
  foldn-id = extensionality (foldn (zero , succ)) id helper
    where
      helper : (x : ℕ) → foldn (zero , succ) x ≡ id x
      helper zero = refl
      helper (succ n) rewrite helper n = refl

  foldn-fusion : ∀ {C C' : Set} (c : C) (h : C → C) (k : C → C') (c' : C') (h' : C' → C') → k c ≡ c' → k ∘ h ≡ h' ∘ k → k ∘ foldn (c , h) ≡ foldn (c' , h')
  foldn-fusion {C} {C'} c h k c' h' refl eq = extensionality (k ∘ foldn (c , h)) (foldn (k c , h')) helper
    where
      helper : (x : ℕ) → (k ∘ foldn (c , h)) x ≡ foldn (k c , h') x
      helper zero = refl
      helper (succ x) = begin 
        (k ∘ h) (foldn (c , h) x)  ≡⟨ ext-rev eq (foldn (c , h) x) ⟩ 
        (h' ∘ k) (foldn (c , h) x) ≡⟨ cong h' (helper x) ⟩
        h' (foldn (k c , h') x)  ∎
```

### proving with the fusion law

```agda
  add : ℕ → ℕ → ℕ
  add zero n = n
  add (succ m) n = succ (add m n)

  plus : ℕ → ℕ → ℕ
  plus n = foldn (n , succ)
  plus' : ℕ → ℕ → ℕ
  plus' = foldn (id , (comp ∘ ⟨ id , succ ! ⟩))
  plus-test1 : plus 13 19 ≡ 32
  plus-test1 = refl
  
  + : ℕ × ℕ → ℕ
  + = uncurry (foldn (id , (comp ∘ ⟨ id , succ ! ⟩)))
  +-test1 : + (3 , 5) ≡ 8
  +-test1 = refl
  +-test2 : + (0 , 100) ≡ 100
  +-test2 = refl
  +-test3 : + (100 , 0) ≡ 100
  +-test3 = refl
  
  +0 : ∀ (n : ℕ) → + (n , 0) ≡ n
  +0 zero = refl
  +0 (succ n) rewrite +0 n = refl

  -- TODO define with fusion la
  plus-succˡ : ∀ {m n : ℕ} → succ (plus m n) ≡ plus (succ m) n
  plus-succˡ {m} {zero} = refl
  plus-succˡ {m} {succ n} rewrite plus-succˡ {m} {n} = refl
  plus-comm : ∀ {m n : ℕ} → plus m n ≡ plus n m
  plus-comm {zero} {n} = ext-rev foldn-id n
  plus-comm {succ m} {n} rewrite plus-comm {n} {m} = sym (plus-succˡ {m} {n})

  plus-comm' : ∀ {m n : ℕ} → (plus m) ∘ (plus n) ≡ (plus n) ∘ (plus m)
  plus-comm' {m} {n} = begin 
    (plus m) ∘ (foldn (n , succ)) ≡⟨ commute₁ ⟩ 
    foldn ((plus m n) , succ)     ≡⟨ extensionality (foldn ((plus m n) , succ)) (foldn ((plus n m) , succ)) helper ⟩
    foldn ((plus n m) , succ)     ≡⟨ sym commute₂ ⟩
    (plus n) ∘ (foldn (m , succ)) ∎
    where
      helper : (x : ℕ) → foldn ((plus m n) , succ) x ≡ foldn ((plus n m) , succ) x
      helper x rewrite plus-comm {m} {n} = refl
      commute₁ = foldn-fusion n succ (plus m) (plus m n) succ refl refl
      commute₂ = foldn-fusion m succ (plus n) (plus n m) succ refl refl
```

**HOMEWORK 2**

```agda
  mul : ℕ → ℕ → ℕ
  mul zero n = zero
  mul (succ m) n = plus n (mul m n)
  mul-test1 : mul 0 3 ≡ 0
  mul-test1 = refl
  mul-test2 : mul 3 15 ≡ 45
  mul-test2 = refl

  mult : (m : ℕ) → ℕ → ℕ
  mult m = foldn (zero , (plus m))

  times : (ℕ × ℕ) → ℕ
  times = uncurry times'
    where
      times' : ℕ → ℕ → ℕ
      times' = foldn ((zero !) , (comp ∘ ⟨ curry ⟨ outr , ev ⟩ , + ! ⟩))
  times-test1 : times (1 , 1) ≡ 1
  times-test1 = refl
  times-test2 : times (123 , 15) ≡ 1845
  times-test2 = refl
  times-test3 : times (5 , 0) ≡ 0
  times-test3 = refl
```

**HOMEWORK 3**

```agda
  fac2 : ℕ → ℕ
  fac2 zero = 1
  fac2 (succ n) = times (n , fac2 n)

  fac : ℕ → ℕ
  fac = outr ∘ fac'
    where
      fac' : ℕ → (ℕ × ℕ)
      fac' = foldn ((zero , succ zero) , ⟨ succ ∘ outl , times ∘ (succ ×₁ id) ⟩)
  fac-test1 : fac 5 ≡ 120
  fac-test1 = refl
  fac-test2 : fac 0 ≡ 1
  fac-test2 = refl
```

Proofs from the script

```agda
  distrib : ∀ (m n x : ℕ) → mult m (plus n x) ≡ plus (mult m n) (mult m x)
  distrib m n x = begin 
    mult m (plus n x)                       ≡⟨ refl ⟩ 
    mult m (foldn (n , succ) x)                 ≡⟨ ext-rev commute₁ x ⟩ 
    foldn ((mult m n) , (plus m)) x             ≡⟨ sym (ext-rev commute₂ x) ⟩ 
    plus (mult m n) (foldn (zero , (plus m)) x) ≡⟨ refl ⟩ 
    plus (mult m n) (mult m x)              ∎
    where
      commute₁ : (mult m) ∘ (foldn (n , succ)) ≡ foldn ((mult m n) , (plus m))
      commute₁ = foldn-fusion n succ (mult m) (mult m n) (plus m) kc kh
        where
          kc : mult m n ≡ mult m n
          kc = refl
          kh : mult m ∘ succ ≡ plus m ∘ mult m
          kh = refl
      commute₂ : (plus (mult m n)) ∘ (foldn (zero , (plus m))) ≡ foldn ((mult m n) , (plus m))
      commute₂ = foldn-fusion zero (plus m) (plus (mult m n)) (mult m n) (plus m) kc (kh m n)
        where
          kc : plus (mult m n) zero ≡ mult m n
          kc = refl
          kh : ∀ (m n : ℕ) → (plus (mult m n)) ∘ (plus m) ≡ (plus m) ∘ (plus (mult m n))
          kh zero zero = refl
          kh (succ m) zero = plus-comm'
          kh m (succ n) = plus-comm'

  induction : ∀ (p : ℕ → 𝔹) → p zero ≡ true → (∀ (n : ℕ) → p (succ n) ≡ p n) → p ≡ true !
  induction p IS IH = begin 
    p                          ≡⟨ introʳ foldn-id ⟩ 
    p ∘ foldn (zero , succ)        ≡⟨ commute₁ ⟩ 
    foldn (true , id)              ≡⟨ sym commute₂ ⟩ 
    (true !) ∘ foldn (zero , succ) ≡⟨ identityʳ ⟩
    true !                     ∎
    where
      commute₁ = foldn-fusion zero succ p true id IS (extensionality (p ∘ succ) p IH)
      commute₂ = foldn-fusion zero succ (true !) true id refl refl
```

## Lists

```agda
  data 𝕃 (A : Set) : Set where
    nil : 𝕃 A
    cons : (A × 𝕃 A) → 𝕃 A

  foldr : ∀ {A C : Set} → (C × (A × C → C)) → 𝕃 A → C
  foldr (c , h) nil = c
  foldr (c , h) (cons (x , xs)) = h (x , foldr (c , h) xs)

  foldr-id : ∀ {A : Set} → foldr (nil , cons) ≡ id {𝕃 A}
  foldr-id {A} = extensionality (foldr (nil , cons)) id helper
    where
      helper : ∀ (x : 𝕃 A) → foldr (nil , cons) x ≡ id x
      helper nil = refl
      helper (cons (x , xs)) rewrite helper xs = refl

  foldr-fusion : ∀ {A B B' : Set} (c : B) (h : A × B → B) (k : B → B') (c' : B') (h' : A × B' → B') 
    → k c ≡ c'
    → k ∘ h ≡ h' ∘ (id ×₁ k)
    → k ∘ foldr (c , h) ≡ foldr (c' , h')
  foldr-fusion {A} c h k c' h' kc kh = extensionality (k ∘ foldr (c , h)) (foldr (c' , h')) helper
    where
      helper : ∀ (x : 𝕃 A) → k (foldr (c , h) x) ≡ foldr (c' , h') x
      helper nil = kc
      helper (cons (x , xs)) rewrite ext-rev kh (x , foldr (c , h) xs) | helper xs = refl

  length : ∀ {A : Set} → 𝕃 A → ℕ
  length {A} = foldr (zero , h)
    where
      h : A × ℕ → ℕ
      h = succ ∘ outr

  isempty? : ∀ {A : Set} → 𝕃 A → 𝔹
  isempty? = foldr (true , (false !))

  cat : ∀ {A : Set} → 𝕃 A × 𝕃 A → 𝕃 A
  cat = uncurry (foldr (id , curry (cons ∘ ⟨ outl ∘ outl , ev ∘ (outr ×₁ id) ⟩)))

  sum : 𝕃 ℕ → ℕ
  sum = foldr (0 , +)
```

**HOMEWORK 4**

```agda
  take : ∀ {A : Set} → ℕ → 𝕃 A → 𝕃 A
  take zero = nil !
  take (succ n) = foldr (nil , (cons ∘ (id ×₁ take n)))
```

**HOMEWORK 5**

We show that the `list` function is functorial:

```agda
  list : ∀ {A B : Set} → (A → B) → 𝕃 A → 𝕃 B
  list f = foldr (nil , (cons ∘ (f ×₁ id)))

  list-id : ∀ {A : Set} → list id ≡ id {𝕃 A}
  list-id = foldr-id

  list-homomorphism : ∀ {A B C : Set} (f : A → B) (g : B → C) → (list g) ∘ (list f) ≡ list (g ∘ f)
  list-homomorphism {A} {B} {C} f g = foldr-fusion nil (cons ∘ (f ×₁ id)) (list g) nil (cons ∘ ((g ∘ f) ×₁ id)) refl refl
```

**HOMEWORK 6**

Ackermann function:

```agda
  ack : ℕ × ℕ → ℕ
  ack = uncurry (foldn (succ , h))
    where
      -- https://arxiv.org/pdf/1602.05010.pdf
      -- first look
      h' : (ℕ → ℕ) → ℕ → ℕ
      h' f = foldn (f 1 , f)
      -- pointfree
      h : (ℕ → ℕ) → ℕ → ℕ
      h = curry (ev ∘ ((foldn ∘ ⟨ ev ∘ ⟨ id , 1 ! ⟩ , id ⟩) ×₁ id))

  -- pointwise definition for comparison
  ack' : ℕ → ℕ → ℕ
  ack' 0 = succ
  ack' (succ n) zero = ack' n 1
  ack' (succ n) (succ m) = ack' n (ack' (succ n) m)

  ack-test1 : ack (3 , 3) ≡ ack' 3 3
  ack-test1 = refl
  ack-test2 : ack (0 , 3) ≡ ack' 0 3
  ack-test2 = refl
  ack-test3 : ack (3 , 2) ≡ ack' 3 2
  ack-test3 = refl
  ack-test4 : ack (2 , 2) ≡ ack' 2 2
  ack-test4 = refl
```

**HOMEWORK 7**

Trees:

```agda
  data 𝕋 (A : Set) : Set where
    leaf : A → 𝕋 A
    bin : 𝕋 A × 𝕋 A → 𝕋 A

  foldt : ∀ {A C : Set} → ((A → C) × ((C × C) → C)) → 𝕋 A → C
  foldt (c , h) (leaf a) = c a
  foldt (c , h) (bin (s , t)) = h (foldt (c , h) s , foldt (c , h) t)

  front : ∀ {A : Set} → 𝕋 A → 𝕃 A
  front = foldt ((cons ∘ ⟨ id , nil ! ⟩) , cat)

  foldt-id : ∀ {A : Set} → foldt (leaf , bin) ≡ id {𝕋 A}
  foldt-id {A} = extensionality (foldt (leaf , bin)) id helper
    where
      helper : ∀ (x : 𝕋 A) → foldt (leaf , bin) x ≡ id x
      helper (leaf x) = refl
      helper (bin (x , y)) rewrite helper x | helper y = refl

  foldt-fusion : ∀ {A C C' : Set} (c : A → C) (h : C × C → C) (k : C → C') (c' : A → C') (h' : C' × C' → C') → k ∘ c ≡ c' → k ∘ h ≡ h' ∘ (k ×₁ k) → k ∘ foldt (c , h) ≡ foldt (c' , h')
  foldt-fusion {A} {C} {C'} c h k c' h' kc kh = extensionality (k ∘ foldt (c , h)) (foldt (c' , h')) helper
    where
      helper : ∀ (x : 𝕋 A) → k (foldt (c , h) x) ≡ foldt (c' , h') x
      helper (leaf x) = ext-rev kc x
      helper (bin (s , t)) rewrite ext-rev kh (foldt (c , h) s , foldt (c , h) t) | helper s | helper t = refl

```

**HOMEWORK 8**

```agda
  sumt : 𝕋 ℕ → ℕ
  sumt = foldt (id , +)

  front-sum : sumt ≡ sum ∘ front
  front-sum = sym (foldt-fusion (cons ∘ ⟨ id , nil ! ⟩) cat sum id + (extensionality _ _ triangle) square)
    where
      triangle : ∀ x → (sum ∘ (cons ∘ ⟨ id , nil ! ⟩)) x ≡ id x
      triangle x rewrite +0 x = refl
      square : sum ∘ cat ≡ + ∘ (sum ×₁ sum)
      square = extensionality _ _ helper
        where 
          helper : (x : 𝕃 ℕ × 𝕃 ℕ) → (sum ∘ cat) x ≡ (+ ∘ (sum ×₁ sum)) x
          helper = {!   !}
```

**HOMEWORK 9**

```agda
  data 𝕋' (A : Set) : Set where
    leaf' : A → 𝕋' A
    bin' : A × 𝕋' A × 𝕋' A → 𝕋' A

  foldb : ∀ {A C : Set} → ((A → C) × (A × C × C → C)) → 𝕋' A → C
  foldb (c , h) (leaf' x) = c x
  foldb (c , h) (bin' (x , (s , t))) = h (x , (foldb (c , h) s , foldb (c , h) t))

  foldb-id : ∀ {A : Set} → foldb (leaf' , bin') ≡ id {𝕋' A}
  foldb-id {A} = extensionality (foldb (leaf' , bin')) id helper
    where
      helper : ∀ (x : 𝕋' A) → foldb (leaf' , bin') x ≡ id x
      helper (leaf' x) = refl
      helper (bin' (x , (t , s))) rewrite helper t | helper s = refl

  foldb-fusion : ∀ {A C C' : Set} (c : A → C) (h : A × C × C → C) (k : C → C') (c' : A → C') (h' : A × C' × C' → C') → k ∘ c ≡ c' → k ∘ h ≡ h' ∘ (id ×₁ k ×₁ k) → k ∘ foldb (c , h) ≡ foldb (c' , h')
  foldb-fusion {A} {C} {C'} c h k c' h' kc kh = extensionality _ _ helper 
    where
      helper : ∀ (x : 𝕋' A) → (k ∘ foldb (c , h)) x ≡ foldb (c' , h') x
      helper (leaf' x) = ext-rev kc x
      helper (bin' (x , (s , t))) rewrite ext-rev kh (x , (foldb (c , h) s , foldb (c , h) t)) | helper s | helper t = refl

  size : ∀ {A : Set} → 𝕋' A → ℕ
  size = foldb ((1 !) , (succ ∘ + ∘ outr))

  flatten : ∀ {A : Set} → 𝕋' A → 𝕃 A
  flatten = foldb ((cons ∘ ⟨ id , nil ! ⟩) , (cons ∘ (id ×₁ cat)))

  flatten-size : ∀ {A : Set} → length ∘ flatten ≡ size {A}
  flatten-size {A} = foldb-fusion (cons ∘ ⟨ id , nil ! ⟩) (cons ∘ (id ×₁ cat)) length (1 !) (succ ∘ + ∘ outr) refl square
    where
      square : length ∘ (cons ∘ ((id ×₁ cat))) ≡ (succ ∘ + ∘ outr) ∘ (id ×₁ length ×₁ length)
      square = {!   !}
```