Category Theory II 8.2: Catamorphisms and Anamorphisms

[soufianemgInk]

I just understood the magic and seriously had to thank you once again. I don't know how I could have managed to understand CT without your book and lectures.

[fremtilfortiden]

This is a mind opening lecture. We all know about the algebra (of evaluation). But in category theory follows the dual: Coalgebra; the algebra that we were never taught. Namely, the algebra of generation.

[BestTheGuy]

He reminds me of Professor Snape. I also think they're both doing magic :Ь

[timh.]

So, I'd like to point out that if you can make a natural transformation (X -> a) => (F X -> a), you can also produce the unique (Fix F -> a). This is what first-year math students know as the principle of mathematical induction (assuming P(x) holds, prove P(F x) holds). The reason we introduce an arbitrary variable X is to keep the algorithm from trying to induce on a type while it's already inducing on it. The reason we get to assume P(X) holds for arbirary X is truly because we're mapping the initial algebra to some other algebra, and so there is a unique morphism, we just might not have its definition yet.

The reason I point this out is because we don't always want to recurse first. Consider an evaluator for a functional language: the conditional expression should only evaluate one of the two branches (technically a total pure language doesn't care because there are no side effects and every function is defined on its entire domain, but we lose a lot of expressivity this way). If we tried to write an interpreter as a catamorphism, we would end up evaluating both branches and throwing away one of the results. That's very wasteful. If instead we can do some pre-processing, recursively eval, and then combine, we get much better performance. I believe this is the idea behind holomorphisms, but I could be mistaken. On top of this, we can get Lisp-like quoting semantics in a homoiconic language by deciding to not recurse on the quote constructor. And for the 'call' evaluator, we can check whether the parameters (or indeed *which* parameters) should be evaluated before calling the function.

Then if you can define an F-algebra (or perhaps a colagebra?) corresponding to your computer's assembly language, you can write a compiler as a single function! huzzah!

[DmitryKurilo]

In case someone prefer working examples (as I do), here is how it works (catamorphisms and anamorphism from this and previous lecture). It works on my phone, so you definitely can compile and run it. :)
But maybe it's a good idea to try to create it yourself first.
{-# LANGUAGE DeriveFunctor #-}
module Main where

import System.IO

type Algebra f a = f a -> a

type Coalgebra f a = a -> f a

newtype Fix f = Fix (f (Fix f))

unFix :: Fix f -> f (Fix f)
unFix (Fix x) = x

cata :: Functor f => (Algebra f a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix

ana :: Functor f => (Coalgebra f a) -> a -> Fix f
ana coa = Fix . fmap (ana coa) . coa

-- Example 1. Fibonacci
data NatF a = ZeroF | SuccF a deriving (Functor)

type Nat = Fix NatF

intToNat :: Integer -> Nat
intToNat 0 = Fix ZeroF
intToNat n = Fix . SuccF . intToNat $ (n-1)

fib :: Algebra NatF (Integer, Integer)
fib ZeroF = (0, 1)
fib (SuccF (m, n)) = (n, m + n)

-- Example 2. Sum
data ListF e a = NulF | ConsF e a deriving (Functor)

type List a = Fix (ListF a)

listToList :: [a] -> List a
listToList [] = Fix NulF
listToList (x:xs) = Fix . ConsF x $ listToList xs

sumAlg :: Algebra (ListF Int) Int
sumAlg NulF = 0
sumAlg (ConsF e a) = e + a

-- Example 3. Primes
data StreamF e a = StreamF e a deriving (Functor)

era :: Coalgebra (StreamF Int) [Int]
era (p:ns) = StreamF p (filter (nodiv p) ns)

nodiv p x = x `mod` p /= 0

primes :: Fix (StreamF Int)
primes = ana era [2..]

streamToList :: Fix (StreamF e) -> [e]
streamToList (Fix (StreamF e a)) = e:streamToList a

main = do
print . fst . cata fib . intToNat $ 10000
print . cata sumAlg . listToList $
print ((streamToList primes) !! 1000)

[DanielMinshewTheInternet]

Has anyone tried editing out that fan noise in the background?

[hujason]

that's a very nice demystification of recursion schemes!

[lorenzolamas-ui]

so, this guy Lambek, goes on and produces his Lemma and then he doesn't go "Fellas" *mic drop* "point, match and set", "cut, wrap it up, that's it" or "I'm the big cheese, y'all are just powder"?

[iamwxz]

how do I get the fixed point of a functor? how do I know List e is the fixed point of ListF e?

[cooperating.systems]

(I am just starting to watch the next course on Lenses, and these seem very coalgebraic to me... )