Instantly share code, notes, and snippets.

# shouya/f-alg.org Secret

Created September 15, 2020 20:14
Show Gist options
• Save shouya/c59f6dd270e58403b4eee898835367a3 to your computer and use it in GitHub Desktop.

# F-algebra

Given a endofunctor F: C -> C, an algebra is a pair (a, α) where a: Ob(C) and α: F a -> a. \$a\$ is called the carrier and \$α\$ is called the evaluator.

# F-algebra for programmers

An endofunctor can be though as a data structure with a type parameter F.

`data F a = ...`

Therefore, an algebra is a function:

`a_alg :: F a -> a -- for some a`

Quiz 1. Is `a_alg` a natural transformation? Why? Quiz 2. Give an example of an algebra, point out the functor \$F\$, the carrier \$a\$ and the morphism (F a -> a).

# F-algebra homomorphism

Given two F-algebra (a, α) and (b, β). A f-algebra homomorphism is a map f.

```     alpha
F a -------> a
|            |
| Ff         | f
v            v
F b -------> b
beta
```

# F-algebra homomorphism for programmers

Here’s an example for Haskell. Let \$F\$ be the `Maybe` functor.

```strAlg :: Maybe String -> String
intAlg :: Maybe Int -> Int

f :: String -> Int

-- if for all x :: Maybe String, we have
intAlg (fmap f x) == f (strAlg x)
-- then f is a homomorphism.```

Quiz: is `length` function an f-algebra homomorphism? Show it!

# Category of F-algebras

Given an endofunctor \$F\$, there is a category of F-algebras, where the objects are the f-algebras and the morphisms are f-algebra homomorphisms.

Quiz: what’s the identities on the objects in the category of F-algebras?

# Initial algebra

In some categories of f-algebras, there is a “best” algebra \$(i, in)\$ such that for any algebra \$(a, f)\$, there is a unique homomorphism \$h : i -&gt; a\$.

```      in
F i -------> i
|            |
|            | cata f
v            v
F a -------> a
f
```

The unique morphism from \$i\$ to \$a\$ is called catamorphism.

# Examples of initial algebra

```data F a = Const
data F' a = Identity a
data F'' a = Zero | Succ a  -- aka Maybe
data F''' a = Nil | Cons Int a

-- initial algebras
initF :: Const -> Const
initF = id

initF' :: Void -> Void
initF' = absurd

initF'' :: F'' Int -> Int
initF'' Zero = 0
initF'' Succ a = 1 + a

initF''' :: F''' [Int] -> [Int]
initF''' Nil = []
initF''' Cons x xs = (x:xs)```

# How to find initial algebra

the colimit of \$0 -&gt; F(0) -&gt; F(F(0)) …\$ is the initial algebra of \$F\$.

# Lambek’s theorem

Claim: If \$(i, in)\$ is the initial algebra, then \$a\$ is isomorphic to \$F(a)\$.

Proof:

```      in
F i -------> i
|           |
| F m       | m
v           v
F F i -----> F i
|    F in   |
| F in      | in
v           v
F i -------> i
```

By initiality, `i` has an unique morphism to `i`, therefore `in . m = id_i`.