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

BM Category Theory : Motivation and Philosophy

Object-Oriented  has 2 weaknesses for Concurrency and Parallel programming : 

  1. Hidden Mutating States; 
  2. Data Sharing.

Category Theory (CT): a higher abstraction of all different Math structures : Set , Logic, Computing math, Algebra… =>

\boxed {\text {CT reveals the way how our brain works by analysing, reasoning about structures !}}

Our brain works by:  1) Abstraction 2) Composition 3) Identity (to identify)

What is a Category ? 
1) Abstraction:

  •  Objects
  • Morphism (Arrow)

2) Composition: Associative 
3) Identity


  • Small  Category with “Set” as object. 
  • Large Category without Set as object.
  • Morphism is a Set : “Hom” Set.

Example in Programming

  • Object : Types Set
  • Morphism : Function “Sin” converts degree to R: \sin \frac {\pi}{2} = 1

Note: We just look at the Category “Types Set” from external Macroview, “forget ” what it contains, we only know the “composition” (Arrows) between the Category “Type Set”, also “forget” what these Arrows (sin,cosin, tgt, etc) actually are, we only study these arrows’ behavior (Associativity).

2.1 : Function of Set, Morphism of Category

Set: A function is 

  • Surjective (greek: epic / epimorphism 满射),
  • Injective (greek : monic / monomorphism 单射)

Category:  [Surjective]

g 。f = h 。f
=> g = h (Right Cancellation )

2.2 Monomorphism 

f 。g = f 。h
=> g = h
(Left cancellation)

\boxed { \text {Epimorphism + Monomorphism =? Isomorphism }}

NOT Necessary !! Reason ( click here): 

In Haskell, 2 foundation Types: Void, Unit

Void = False
Unit ( ) = True

Functions : absurd, unit
absurd :: Void -> a (a = anything)
unit :: a -> ()

[to be continued 3.1 ….]

代 数拓扑 Algebraic Topology (Part 1/3)

Excellent Advanced Math Lecture Series (Part 1 to 3) by 齊震宇老師

(2012.09.10) Part I:

History: 1900 H. Poincaré invented Topology from Euler Characteristic (V -E + R = 2)

Motivation of Algebraic Topology : Find Invariants [1]of various topological spaces (in higher dimension). 求拓扑空间的“不变量” eg.

  • Vector Space (to + – , × ÷ by multiplier Field scalars);
  • Ring (to + x) in co-homology
  • etc.

then apply algebra (Linear Algebra, Matrices) with computer to compute these invariants  (homology, co-homology, etc).

A topological space can be formed by a “Big Data” Point Set, e.g. genes, tumors, drugs, images, graphics, etc. By finding (co)- / homology – hence the intuitive Chinese term (上) /同调 [2] – is to find “holes” in the Big Data in the 10,000 (e.g.) dimensional space the hidden information (co-relationship, patterns, etc).
Note: [1] Analogy of an”Invariant” in Population: eg. “Age” is an invariant can be added in the “Population Space” as the average age of the citizens.

Side Reading (Very Clear) : Invariant and the Fundamental Group Primer

Note [2]: Homology 同调 = same “tune”.

南朝 刘宋 谢灵运山水诗:
同调 = Homology
(希腊 homo = 同, -logy = 知识 / 调)

– “Reading an ancient text  allows us to think “in tune” (or resonant) with the ancient author.”

[温习] Category Theory Foundation – 3 important concepts:

  • Categories
  • Functors
  • Natural Transformation

[Skip if you are familiar with Category Theory Basics: Video 16:30 mins to 66:00 mins.]

[主题] Singular Homology Groups 奇异同调群  (See excellent writeup in Wikipedia) (Video 66:20 mins to end)

  1. Singular Simplices 奇异 单纯
  2. Singular Chain Groups 奇异 链 群
  3. Boundary Operation 边界
  4. Singular Chain Complex 奇异 单纯复形

Part 1/3 Video (Whole) :

Category Theory in Computing Languages

​Is there any connection between category theory and the way computer languages work? by Thorsten Altenkirch 

Yes, lots.

Just one example: a function with 2 inputs from A and B and results from C would have the type A x B -> C but in functional languages like Haskell we are using A -> (B -> C), i.e. a function that returns a function. This “currying” is exactly a the categorical definition of a cartesian closed category as one where Hom(AxB,C) is isomorphic to Hom(A,B -> C) and in this false you can replace Hom(X,Y) with X -> Y.

It is well known that effects in functional programming can be modelled by monads which is a concept from category theory. Nowadays a weaker structure called applicative functors has become very popular – needless to say also a concept from Category Theory.

Not all languages are functional (yet) but even non-functional languages can be understood using concepts from category theory.

See also: 

Free Categories, Free MonoIds, Monads = MonoId+Endofunctor

Monad Diagram