Category Theory – Purest of pure mathematical disciplines may also be a cornerstone of applied solutions in computational science

There exists in almost all Universities a clear division between pure and applied mathematics. A friendly (and sometimes not so friendly) rivalry exists between both sides of the divide, with separate conferences, separate journals and in many cases even a whole separate language. Category Theory was seen as such an abstract area of research that even pure mathematicians started to refer to it as “abstract nonsense“, and until the mid 1980’s almost all category theorists occupied a place hidden somewhere up above the ‘cloud level’ in the highest reaches of the peaks that defined “pure” maths.

By the mid 1990’s and then by the turn of the millenium, a whole world of computer programmers were learning basic category theory as part of their induction into functional programming. The best known product of these efforts is the Haskell language, but even in the past 7 or 8 yrs, workshops on category theory for computer programmers of all types have flourished and proliferated. It is almost as if there are two separate communities masquerading as one – mathematical category theory and computer programming category theory – and never the twain would meet. Or so it seemed, until now.


Alejandro Serrano: Category Theory Through Functional Programming

(Part 1/3) – λC 2017

What is Category ?


Morphism (Arrows )

Rule1: Associative

Rule 2: Identity

A <– C –> B

Product of Categories : A x B


Sum of Categories: A + B


(Either a b)


Reverse all arrows.


Functor F: C-> D

Mapping of all objects (A, B) in categories C,D

Mapping of arrows f
f : A -> B
Ff : FA -> FB (preservation)
F Id = Id
F (f。g) = Ff。Fg


Constant C -> F
FC = k
Ff = Id

Arrow Functor F: C -> D

For any object A in C,

F A = D -> A
(Functional Type is also Type)

Functors compose !

Category of categories:

Objects: categories

Arrows : Functors

Haskell Category (Hask) is always Endo-Functor, ie Category Hask to itself.

Mapping of arrows.

Mapping of Objects = predefined

(Part 2/3) – λC 2017

(part 3/3) – λC 2017

Category Theory II 9: Lenses

Lens = {get, set}

w = whole tuple, p = a field

get :: w -> p
set :: w -> p -> w

Example: take a pair (tuple)

get1 (x, y) = x

get1 :: (a, b) -> a

set1 (x, y) x’ = (x’,y)

set1 :: (a, b) -> a -> (a,b)

Polymorphic Types: change type of field

set :: w -> p’ -> w’
set1 :: (a, b) -> a’ -> (a’,b)

Lens Laws:

set w (get w) = id 

get (set w p) = p

get (set w p) p’ = set w p’

Combine get & set (co-Algebra):

\boxed {w \to(p, p \to w)}

data Store p w = Store p (p-> w)

fmap g (Store p f ) = Store p (g.f)
g: w-> v
pf : p -> w
g.f : p-> v

Store = functor from w to Store = coalgebra = comonad [W a ->a]

instance Comonad (Store p) where

extract (Store p f) = f p

duplicate  (Store x f) = Store x ( λy -> Store y f)

[Think of p as key, f is the lookup function
f p = retrieve current value]

Comonad & coalgebra – compatible?

(Coalgebra) coalg ::a -> w a
(Comonad) extract :: w a -> a
duplicate :: w a ->w (w a)

coalg w = Store (get w) (set w)

set w (get w) = id [Lens Law]

\boxed {\text {Lens = comonad + coalgebra}}

If Type change (Set = Index Store : a = p, b = p’, t = w)

IStore a b t = IStore a (b ->t)

Object-oriented: eg. school.class.student

<=>”.” = functional programming 

9.2 Lenses 

Type Lense s t a b = forall f . Functor f => (a -> f b) -> s -> f t

s \to \forall f. (a \to f b ) \to f t

s  ->IStore a b t

forall  = polymorphism (?  Natural Transformation)

Yoneda Embedding Lemma

 [C, Set](C (a -> – ), C (b -> – )) ~ C(b, a)

Adjunction: C (Ld,C) ~ D (D,  Rc)

Reference: “Understanding Yoneda”

adjoint functor in nLab

Yoneda lemma in nLab

维基百科: Hom functor

The Yoneda Lemma

Representable Functor F of C ( a, -):

\boxed {(-)^{a} = \text {F} \iff a = \text {log F}}

Video 4.2 Yoneda Lemma

Prove : 

Yoneda Lemma :
\text {F :: C} \to \text {Set}

\boxed {\alpha \text { :: [C, Set] (C (a, -),F) } \simeq \text {F a}}

\alpha : \text {Natural Transformation}
\simeq : \text {(Natural) Isomorphism, "naturally" } \forall ( a, F )

Proof: By “Diagram chasing” below, shows that

: \alpha \text { :: [C, Set] (C (a, -),F) } is indeed a (co-variant) Functor. (Higher-order Function)

Right-side: Functor “F a“. (Data Structure)

\boxed {\forall x, (a \to x) \to \text { F } x \simeq \text { F } a }

Note: When talking about the natural transformations, always mention their component “x”: \alpha_{x}, \beta_{x}

Video 5.1 Yoneda Embedding

Example 1: F = List functor [x]

\boxed {\alpha \text { :: } (a \to x) \to [x] \simeq [a] }

Example 2: F = C (b, -)

\boxed {\alpha \text { :: [C, Set] (C (a, -), C (b, -) ) } \simeq \text {C (b, a)}}

Note: check a , b is in co-variant or contra-variant position.

Example 3: F = Id

\boxed {\alpha \text { :: } (a \to x) \to x \simeq a }

Right-hand-side: a (data structure)

Left-hand-side : “(a -> x) “is a function called “handler” (or “continuation“) which takes the argument “a” to provide it as output : “(a -> x ) -> x“.

eg. handler to database query, over internet…(technique used in Compiler)

Co-Yoneda Lemma : (Contra-variant a , F)

\boxed {\alpha \text { :: [C, Set] (C(-, a),F) } \simeq \text {F a}}

Yoneda Embedding: Full and Faithful
\alpha \text { :: [C, Set] (C (a, -), C (b, -) ) } \simeq \text {C (b, a)}

Note: Instead of proving a , b are isomorphic, sometimes it is easier to prove the functors C(a, -) & C(b, -) are isomorphic.[Proof Trivial: functors preserve composition and identity]

ApplicationCo-Yoneda Lemma : (Contra-variant a , F)
\boxed {\text {[C, Set] (C(- , a), C(- , b) } \simeq \text {C(a ,b)}}

Pre-order Category \boxed {a \leq b}

\forall x, \text {C(x , a)} \to \text {C(x , b)} \simeq \text {C(a , b)}

C(x , a) = x \leq a = \{\varnothing, 1 \}
C(x , b) = x \leq b =\{\varnothing, 1 \}

3 possibilities: (“1” = singleton)
id_{\varnothing} :: \varnothing \to \varnothing
absurd :: \varnothing \to 1
id_{1} :: 1 \to 1
Note: 1 \to \varnothing impossible (function must have an image)


Right-Hand Side: a \leq b

Left-Hand Side: \forall x,( x \leq a \implies x \leq b) \implies a \leq b

Yoneda Embedding (Lagatta)

BM Category Theory II 1.1: Declarative vs Imperative Approach

Excellent lecture using Physics and IT to illustrate the 2 totally different approaches in Programming:

  1. Imperative (or Procedural) – micro-steps or Local 微观世界 [eg. C / C++, Java, Python…]
  2. Declarative (or Functional) – Macro-view or Global 大千世界 [eg. Lisp / Clojure, Scala, F#, Haskell…]

In Math

  1. Analysis (Calculus) 
  2. Algebra (Structures: Group, Ring, Field, Vector Space, Category …)

In Physics:

  1. Newton (Laws of Motion), Maxwell (equations) 
  2. Fermat (*)  (Light travels in least time), Feynman (Quantum Physics).

In IT: Neural Network (AI)  uses both 1 & 2.

More examples…

In Medicine:

  1. Western Medicine: germs/ viruses, anatomy, surgery
  2. Traditional Chinese Medicine (中医): Accupunture, Qi, Yin-Yang.

Note (*): Fermat : My alma mater university in Toulouse (France) named after this 17CE amateur mathematician, who worked in day time as a Chief Judge of Toulouse City, after works spending time in Math and Physcis. He co-invented Analytic Geometry (with Descartes), Probability (with Pascal), also was the “Father of Number Theory” (The Fermat’s ‘Little’ Theorem and The Fermat’s ‘Last’ Theorem). He used Math to prove light travels in straight line (before Newton) due to “Least Time taken” (explained here in this BM video).

Revision :Part 1 Motivation & Philosophy of Category Theory