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”

https://bartoszmilewski.com/2013/05/15/understanding-yoneda/

adjoint functor in nLab

Yoneda lemma in nLab

维基百科: Hom functor
https://www.zhihu.com/question/23324349/answer/54242934

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s