In the preceding post, we did a rudimentary survey of the principal elements comprising the apparatus of category theory. Henceforth, we shall direct our gaze towards the intricate constituents conjured by these foundational elements, plunging further into the intricate labyrinth of interwoven components in the machinery of category theory.
Higher category theory deals with the generalization of parts that make up machinery. In this realm, we erect structures in a context where, between objects, we have not only mere morphisms but k-morphisms, which are maps between (k - 1) of those morphisms where \(k \in \mathbb{N}\).
Horizonal Composition, if \(F_1, G_1 : A \to B\), \(F_2, G_2 : B \to C\) and \(\alpha : F_1 \Rightarrow G_1\), \(\beta : F_2 \Rightarrow G_2\) then \(\beta \circ \alpha : (F_2 \circ F_1) \Rightarrow (G_2 \circ G_1)\),
Vertical Composition, if \(F, G, H : A \to B\) and \(\alpha : F \Rightarrow G\), \(\beta : G \Rightarrow H\) then,
In any category \(\mathbb{C}\) the following diagram is called the product diagram, where \(A, B, \pi_1, \pi_2, X, f, g \in\mathbb{C}\),
This diagram must satisfy the following universal property: if we have a similar diagram, then there exists a unique morphism \(h: X \to A \times B\) such that,
In almost every programming languages, you’ll find products implemented as pairs, with their distinct types and two constructors much like \(\pi_1\) and $π_2", granting access to the pair’s first and second elements, respectively.
example :: (Int, String)
example = (111, "Apples")
number = fst example
string = snd example
An adjunction is a weaker notion of equivalence defined above in the sense that it does not impose the natural isomorphism between composition of functors and identity. Instead, it imposes the existence of the following isomorphism: for \(c\in\mathbb{C}\) and \(d\in\mathbb{D}\),
\(hom_{\mathbb{d}} (fc, d) \cong hom_{\mathbb{c}} (c, gd)\)
Here, \(F\) is called the left adjoint of functor \(G\) written as \(F \dashv G\) if whenever for \(c \in \mathbb{C}\) and \(d \in \mathbb{D}\) all the maps from \(Fc \to d\) are the same as maps from \(c \to Gd\). This structure with two functors and the above isomorphism is called an adjunction.
In the category of sets (\(\textbf{Set}\)) all the objects can be combined by forming their Cartesian product. Which is just another object in \(\textbf{Set}\): \(A \times B\) which is the set of all ordered pairs \((x, y)\) such that \(x \in A\) and \(y \in B\). This construction is the same as products described earlier.
We can also express another set or object as \(B^A\) in that it is the same as \(hom_{\textbf{Set}}(A, B)\) i.e. it has all the functions between \(A\) and \(B\).
Now, let’s fix the set \(B\) we get from the following functors:
\(\_ \times b : \textbf{Set} \to \textbf{Set}\) \((\_)^b : \textbf{Set} \to \textbf{Set}\)
If one thinks of types as sets, then the morphism \(\lambda.g : \_ \to (\_)^B\) represents the function that takes in a value from some arbitrary type and returns the function type. Moreover, if we are given this \(\lambda g\) then we can easily get \(g: \_ \times B \to C\) and vice versa,
From, \(g: \_ \times B \to C\)
We can define a \(g’ : \_ \to C^B\) as \((g’(a))(b) = g (a,b)\) where \(a \in \_\) and \(b\in B\).
Similarly from, \(f: \_ \to C^B\)
We can define a \(f’: \_ \times B \to C\) as \(f’(a, b) = (f(a))(b)\) where \(a \in \_\) and \(b\in B\).
This method of obtaining a function (with one argument) that returns another function (which takes two arguments) is called currying, and its reverse is called uncurry.
curry :: ((a, b) -> t) -> a -> b -> t
curry f a b = f (a, b)
uncurry :: (t1 -> t2 -> t3) -> (t1, t2) -> t3
uncurry g (a, b) = g a b
Similarly, one can show that there is a canonical bijection here that programmers can understand intuitively, i.e.,
\(hom_{\textbf{Set}} (A \times B, C) \cong hom_{\textbf{Set}} (A, C^B)\)
Since we now have two functors and an isomorphism, we’ve got ourselves an adjunction here for every set \(B\).
This example requires some jargon,
Now, let \((A, \leq)\) and \((B, \leq)\) be two partially ordered sets, and then the (monotone) Galois connection between these posets consists of two monotone functions: \(f : A \to B\) and \(g : B \to A\), such that for all \(a \in A\) and \(b \in B\),
\(f(a) \leq b\) if and only if \(a \leq g(b)\)
From the lens of category theory, one can say that a Galois connection is nothing but an adjoint \(f \dashv g\) equipped with the essential property that an upper or lower adjoint of a Galois connection uniquely determines the other:
A monad on some category \(\mathbb{C}\) is a triple \((T,\eta,\mu)\) which consists of,
such that the following diagrams in the functor category \(\mathbb{C}^{\mathbb{C}}\) commute, i.e. to say for all \(c \in \mathbb{C}\) the following diagrams commute when functors are applied to \(c\) (\(Tc\)) and when components of natural transformations (\(\eta_c\), \(\mu_c\)) are considered, then these diagrams commute in \(\mathbb{C}\),
Associativity Square:
Unit Triangles:
One may also say that a monad is a generalization of monoid.
In this world, programs denote the morphisms between objects \(A\) and \(TB\) where \(A\) is the object of values of type \(A\) and \(TB\) is the object of computations of type \(B\). These programs are functions that are generated through a maze of computations.
For the existence of a monad in such a category, these programs must form a kliesli category.
A kliesli triple over \(\mathbb{C}\) is the triple \((T, \eta, \_^\star)\) where,
The equations for kliesli triples form a category, i.e. the kliesli category (\(\mathbb{C}_T\)) such that given a kliesli triple \((T, \eta, \_^\star)\) , \(\mathbb{C}_T\) is defined as,
class Monad where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
Monad of partiality, \(TA = A + {\bot}\) where \(\bot\) denotes divergent computation is expressed in Haskell as the algebraic data type `Maybe`,
instance Monad Maybe where
return a = Just a
m >>= f = case m of
Just x -> f x
Nothing -> Nothing
divide :: Maybe Int -> Maybe Int -> Maybe Int
divide a b = a >>= \m -> b >>= \n -> if n == 0 then Nothing else return (a `div` b)
Monad for side effects: A side effect is a form of computation where the computation changes state. It can be changing stuff inside variables or raising an exception. We can express such a notion by \(TA = (A \times S)^S\) where \(S\) is a set of states.
instance Monad (State s) where
return a = State (\s -> (s, a))
State m >>= f = State (\s -> let (s', a) = m s
State m' = f a
in m' s')
readState :: State s s
readState = State (\s -> (s, s))
writeState :: s -> State (s, ())
writeState s = State (\s -> (s, ()))
-- Example
increment :: State Int ()
increment = readState >>= \s -> writeState (s + 1)
The above material comes from my notes made while reading, watching,