### Fold-Fusion Strikes Back

Since I'm determined not to touch Agda after I get up in order to prepare for the midterms, I'm currently reluctant to fall asleep XD. Below I proved some simple facts about fold in Agda, but I haven't written any practical examples yet.

First we define function composition. The operator precedence "30" is arbitrarily chosen, which luckily seems to work.

infixl 30 _○_ _○_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C) (f ○ g) x = f (g x)

Now we prove the Fold-Fusion Theorem. (By chain reasoning, of course. XD)

foldr-fusion : {α β γ : Set} -> {f : α -> β -> β} {e : β} {h : β -> γ} {g : α -> γ -> γ}-> ((x : α)(y : β) -> h (f x y) ≡ g x (h y)) -> ∀ (\xs -> (h ○ (foldr f e)) xs ≡ foldr g (h e) xs) foldr-fusion _ [] = refl foldr-fusion {_}{_}{_} {f}{e}{h}{g} fuse (x :: xs) = chain> (h ○ foldr f e) (x :: xs) === h (foldr f e (x :: xs)) by refl === h (f x (foldr f e xs)) by cong h refl === g x (h (foldr f e xs)) by fuse x (foldr f e xs) === g x ((h ○ foldr f e) xs) by cong (g x) refl === g x (foldr g (h e) xs) by cong (g x) (foldr-fusion fuse xs) === foldr g (h e) (x :: xs) by refl

This is the first time I formally prove the Fold-Fusion Theorem. XD

Define the identity fold and prove that it is indeed an identity.

id-foldr : {A : Set} -> List A -> List A id-foldr = foldr _::_ [] id-foldr-id : {A : Set}{xs : List A} -> id-foldr xs ≡ xs id-foldr-id {_}{[]} = refl id-foldr-id {_}{x :: xs} = chain> id-foldr (x :: xs) === foldr _::_ [] (x :: xs) by refl === x :: foldr _::_ [] xs by refl === x :: xs by cong (_::_ x) id-foldr-id

Then we prove that for any function `f`

, `f`

is the same as `f ○ id-foldr`

.

compose-id : {A B : Set}(f : List A -> B)(xs : List A) -> f xs ≡ (f ○ id-foldr) xs compose-id f xs = chain> f xs === f (id-foldr xs) by cong f (sym id-foldr-id) === (f ○ id-foldr) xs by refl

Finally we prove that `map f`

is a fold by Fold-Fusion Theorem: first add an `id-foldr`

to the right of `map f`

and then apply fold-fusion.

map-as-foldr : {A B : Set}{f : A -> B}{xs : List A} -> map f xs ≡ foldr (\y ys -> f y :: ys) [] xs map-as-foldr {A}{_}{f}{xs} = chain> map f xs === (map f ○ id-foldr) xs by compose-id (map f) xs === foldr (\y ys -> f y :: ys) [] xs by foldr-fusion fuse-cond xs where fuse-cond : (x : A)(xs : List A) -> (map f) (x :: xs) ≡ (\y ys -> f y :: ys) x (map f xs) fuse-cond x xs = refl

--

Chain reasoning is marvelous! XD

Labels: Agda, Programming

<< 回到主頁