The preface for this book essentially argues that the software we've built using crude, duct-taped languages (C, Java, Go, etc) that were not based on good (aka mathematically sound) foundations, is truly incredible. Much like how it's a miracle of chance that many gothic structures are still standing (built with intuition, without engineering principles), it's incredulous that we sent people to the moon with null pointer errors. Bartosz argues that we will soon approach the limits of imperative, side-effectful programming, its software becoming too complex to modify in one place without breaking something in another (or too bureaucratic and boring to hang onto the few minds that have this power). My opinion is that generative AI is extending the life of imperative code projects, but only for a little while; sooner or later, a house of cards must come falling down.

This book sets out to give a brief but rigorous understanding of category theory that you can take with you to reasoning about everyday programs. I'm not sure that it's as terse and compact as it could be to be the most practical recommendation for functional programming, but it's a start.

10 Natural transformations

We have categories C,D with a functor F from C to D.
F maps
1. objects in C to objects in D
2. morphisms in C to morphisms in D

Suppose we have two functors F, G between C,D. A natural transformation is a collection of mappings between the respective images of C under F and G. A natural transformation alpha is a collection of mappings, defined for each object a in C:
alpha_a :: F a -> G a

For any morphism f :: a -> b in C, we have F f and G f, of type
F f :: F a -> F b
G f :: G a -> G b

A natural transformation alpha must satisfy the naturality condition, which informally says that it doesn't matter whether we go from F a to G b via F f or G g.
Formally, the naturality condition means for all objects a,b in C, then taking their respective components alpha_a and alpha_b in alpha, then for all f :: a -> b in C:
G f . alpha_a = alpha_b . F f
where (brackets showing intermediate type)
G f . alpha_a :: F a (-> G a) -> G b
alpha_b . F f :: F a (-> F b) -> G b

In programming, where we use the category of types:
- objects are types
- morphisms are functions between types
And subsequently, functors have both:
- type constructors that map types to types (endofunctor)
- fmap, which maps morphisms to morphisms

Contravariant functors reverse the order of function composition in the target category.

(->) a is a functor (specifically, covariant functor) because
let F b = (->) a b
fmap :: (x -> y) -> F x -> F y
fmap :: (x -> y) -> (a -> x) -> (a -> y)
fmap x_to_y a_to_x = x_to_y . a_to_x -- notice that x_to_y is is applied after the functor

F a is contravariant if can define
contramap :: (x -> y) -> F y -> F x
contramap x_to_y f_y = f_y . x_to_y -- notice that x_to_y is is applied before the functor

let F a = a -> r
contramap :: (x -> y) -> (y -> a) -> (x -> a)
contramap x_to_y y_to_a = y_to_a . x_to_y

---


10.6 Challenges
1. Prove the naturality condition from Maybe to List.

Let F = Maybe and G = List. We want to show, for any f :: a -> b:
G f . alpha_a = alpha_b . F f
(fmap_G f) . alpha_a = alpha_b . (fmap_F f)

alpha_a :: Maybe a -> List a
5. alpha_a Nothing = []
6. alpha_a (Just a) = [a]

-- Because parametrically polymorphic functions are defined with an implicit forall a in their type constraints, alpha_b is the same as alpha_a
alpha_b :: Maybe b -> List b
alpha_b = alpha_a 

Let's call alpha = alpha_a = alpha_b.

So we want to show:
(fmap_G f) . alpha = alpha . (fmap_F f)

fmap_G :: (a -> b) -> List a -> List b
1. fmap_G f [] = []
2. fmap_G f (x:xs) = (f x) : (fmap_G f xs)

fmap_F :: (a -> b) -> Maybe a -> Maybe b
3. fmap_F f Nothing = Nothing
4. fmap_F f (Just a) = Just (f a)

fmap_G f . alpha $ Nothing
= fmap_G f (alpha Nothing) -- function associativity
= fmap_G f ([])            -- 5
= []                       -- 1

alpha . fmap_F f $ Nothing
= alpha (Nothing) -- 3
= []              -- 5

fmap_G f . alpha $ Just a
= fmap_G f (alpha (Just a))
= fmap_G f [a]             -- 6
= [f a]                    -- 2

alpha . fmap_F f $ Just a
= alpha (Just (f a)) -- 4
= [f a]              -- 6

2. Two different natural transformations between Reader () and List.

newtype Reader e a = Reader (e -> a) -- we will just write e -> a in place of Reader (e -> a), and write R a in place of Reader () a

alpha :: R a -> List a
alpha _ = []

beta :: R a -> List a
beta f = [f ()]

gamma :: R a -> List a
gamma f = [f (), f ()]

There are (countably) infinitely many lists of ().
[]
[()]
[(), ()]
...

The Yoneda lemma later hints that each of the possible natural transformations from (e -> a) to F a corresponds to the members of F e.

3. Two different nat trans between Reader Bool and Maybe.
Reader Bool a = Bool -> a

alpha :: (Bool -> a) -> Maybe a
alpha _ = Nothing

beta :: (Bool -> a) -> Maybe a
beta f = Just (f False)

gamma :: (Bool -> a) -> Maybe a
gamma f = Just (f True)

Maybe Bool has three values: Nothing, Just False and Just True, which correspond to alpha, beta, gamma.

These are all the possible natural transformations, but shouldn't be anywhere near the number possible functions of this type. By cardinality calculations:
|(Bool -> a) -> Maybe a|
= |Maybe a| ^ |Bool -> a|
= |Maybe a| ^ |a| ^ |Bool|
= (1 + |a|) ^ (2*|a|)
For a = Bool, that gives us (3)^4 = 81 possible values.
If we fix a = Bool, there are four possible Bool -> Bool functions: id, not, true (const True), false (const False)

That's because if Bool is instantiated in the type signature, the function bodies have access to interrogation on f's values. For example:

delta :: (Bool -> Bool) -> Maybe Bool
delta f =
	if f False == True and f True == False -- aka f == not
	then Just False
	else Nothing

Holy shit! This is a direct explanation of how writing polymorphic functions truly reduces the number of possible functions (and therefore errors) by orders of magnitude.

But how can we use the cardinality calculation on parametrically polymorphic functions? Why, that will be the purpose of the Yoneda lemma!

|forall a. (Bool -> a) -> Maybe a|
= |Maybe e| ^ 1 where e = Bool
= (1 + 2) ^ 1