First Lens to Lenses

前言

Haskell中有一个很强大的库，叫做Lens。

在Haskell中，只提供了「模式匹配」的语法来访问/修改数据结构。于是处理深层的数据就成为了老大难的问题。

比如在这样的数据结构里：

data Point = Point 
    { positionX :: Double
    , positionY :: Double
    } deriving (Show, Eq)

data Segment = Segment
    { segmentStart :: Point
    , segmentEnd :: Point
    } deriving (Show, Eq)

p1 = Point 1 2
p2 = Point 3 4
l1 = Segment p1 p2

我们要修改l1的第二个端点的横坐标：

l1 {segmentEnd = (segmentEnd l1) {positionX = 10}}

如果数据结构更加复杂的时候，代码就会变得更冗长。

这时候Lens库就出场了,刚刚那段代码等价于：

l1 & endLens . xLens .~ 10

其中endLens . xLens就是一个透镜组，先访问end，再访问x，.~就是set。很composable有木有。

但是我们打开Hackage想要看看Lens究竟是啥的时候，第一眼就被lens的类型吓到了：

type Lens s t a b = forall f. Functor f. (a -> f b) -> (s -> f t)

这是啥！？

当我们打开某乎，搜索关键字，想看看各路dalao的解释的时候，又被吓到了：

一个Lens不过就是Coalgebra for the CoState Comonad，这有什么难理解的。

这又是啥！？

不懂不懂！但这不妨碍我们自己去摸索……

从零开始的getter和setter

无论是深层还是浅层，lens做的都是get和set的操作。我们先把getter和setter抽象出来。

数据b到数据a的getter和setter应该具有如下类型：

getter :: b -> a
setter :: b -> a -> b

我们同时需要getter和setter，于是将这两个函数合起来：

newtype GS b a = GS (b -> (a -> b, a))

如果现在有一个GS b a，我就可以对b进行set或者get的操作了：

set :: GS b a -> a -> b -> b
set (GS gs) = flip $ fst . gs 

get :: GS b a -> b -> a
get (GS gs) = snd . gs

对于Point到Double类型，我们可以写下一些GS：

xGS, yGS :: GS Point Double
xGS = GS (\p -> (\x -> p { positionX = x }, positionX p))
yGS = GS (\p -> (\y -> p { positionY = y }, positionY p))

我们可以像Lens一样，对Point进行get和set：

get xGS p1 -- = 1.0
set yGS 10 p2 -- = Point 3.0 10.0

Lens有一个很重要的性质就是可组合性，多个lens可以组合在一起。不知GS能不能做到呢，先写下类型：

(>.) :: GS c b -> GS b a -> GS c a
(>.) = _

（此处省略填坑的步骤）我们可以写出组合GS的代码！

infixr 9 >.
(>.) :: GS c b -> GS b a -> GS c a
(>.) = (GS cbl) (GS bal) = 
    GS $ \c -> 
        let (bc, b) = cbl c in
            let (ab, a) = bal b in 
                (bc . ab, a)

验证一下：

get (endGS >. xGS) l1 -- get x of the end of l1 = 3
set (endLens >. xLens) 10 l1 --...

！好耶，我们的GS也是可以组合的！这就是我们的Lens！那么我们也给它一个Lens的名字吧！

附上：

newtype MyLens b a = MyLens (b -> (a -> b, a))

set :: MyLens b a -> a -> b -> b
set (MyLens lens) = flip $ fst . lens 

view :: MyLens b a -> b -> a
view (MyLens lens) = snd . lens

over :: MyLens b a -> (a->a) -> b -> b
over lens f b = set lens (f (view lens b)) b

compLens :: MyLens c b -> MyLens b a -> MyLens c a
compLens (MyLens cbl) (MyLens bal) = 
    MyLens $ \c -> 
        let (bc, b) = cbl c in
            let (ab, a) = bal b in 
                (bc . ab, a) 

infixr 9 >.
(>.) :: MyLens c b -> MyLens b a -> MyLens c a
(>.) = compLens

infixl 8 ^.
(^.) = flip view

infixr 4 %~
(%~) = over

infixr 4 .~
(.~) = set

infixl 1 & 
x & f = f x

大胆猜想小心求证

可是我们现在得到的是b -> (a -> b, a)和库里的forall f. Functor f. (a -> f b) -> (s -> f t)八竿子打不着啊。难道它们冥冥之中有什么关系！？

我们看一个lens的一个简化版本

type Lens' b a = Lens b b a a --forall f. Functor f. (a -> f a) -> (b -> f b)

调一下参数的位置就有b -> forall f. Functor f. (a -> f a) -> f b，跟b -> (a -> b, a)进行比较，不同的是forall f. Functor f => (a -> f a) -> f b和(a -> b, a)这两部分。

如果这两部分是等价的（isomorphism），不就可以得到MyLens和Lens’也等价了吗！？

于是大胆猜想：forall f. Functor f => (a -> f a) -> f b和(a -> b, a)是等价的

然后小（shi）心（fen）论（cao）证（shuai），（省略填hole的n步），我们写出了：

phi ::(forall f. (a -> f a) -> f b) -> (a -> b, a)
phi h = h (\a -> (id, a))

psi :: (a -> b, a) -> (forall f. Functor f => (a -> f a) -> f b)
psi (g, a)= \f -> fmap g $ f a

psi . phi == id 
phi . psi == id

！好耶我们证明了MyLens和Lens’是等价的！

泛化的版本

但是，Lens库里提供的Lens是这样的：

type Lens s t a b = forall f. Functor f. (a -> f b) -> (s -> f t)

这又是什么意思呢？现在先别管这个，我们继续来看我们自己造的Lens。

现在我们可以写出这样的代码：

_1 :: MyLens (a, b) a
_1 = MyLens (\(a, b) -> (\a' -> (a', b), a))

_2 :: MyLens (a, b) b
_2 = MyLens (\(a, b) -> (\b' -> (a, b'), b))

(1, 2) & _1 .~ 10 -- = (10, 2)
--set _1 10 (1, 2)

((1, "Ho Ho Ho"), 2) & (_1 >. _2) .~ "How bad could it be?" 
-- ((1, "How bad could it be?"), 2)

但是我们暂时写不出：

(1, 2) & _1 .~ '1' --期望得到('1', 2)

这样的代码，会报错：

? Could not deduce (Num Char) arising from the literal ‘1’ from the context: Num b bound by the inferred type of it :: Num b => (Char, b) at <interactive>:2:1-18

这是因为MyLens对getter和setter的抽象，限制了set进去的东西要和get到的东西具有同样的类型，并且set完之后的类型要和set之前一样：

getter :: b -> a
--             ^ here，这是get到的值的类型
setter :: b -> a -> b
--             ^ here，这是set进去的值的类型

我们可以来消除这个限制，将getter和setter抽象为：

getter :: s -> a -- 从s中get到a
setter :: s -> b -> t --把s中的a set为b，s变为t

于是MyLens可以重写为：

newtype MyLens s t a b = MyLens (s -> (b -> t, a))
-- getter :: s -> a
-- setter :: s -> b -> t
-- set, view, over, (>.)等的实现和之前完全一样!

现在我们就可以写出：

(1, 2) & _1 .~ '1' -- ('1', 2)

那么，问题来了，现在这个MyLens的版本是否是和库里的Lens等价呢？其实刚刚已经给出证明了！和化简模式是一致的。

Further more?

到这里，我们已经得到了一个属于自己的Lens。我们也会用它从一些数据结构中的字段，但是Lens远远不是只有这点威力。

首先，MyLens中的getter和setter其实是抽象的，getter :: b -> aa并不一定指的是b中的字段，而就是一个普普通通的函数。比如我设写一个lens，从[a]中get到length，而set并不改变值：

_length :: MyLens [a] [a] Int b
_length = MyLens $ \as -> (const as, length as)

我们根据这个_length可以写出一些代码：

view  _length [1, 2, 3] -- 3
view (_1 >. _length) ([1, 2, 3], "Tora!Tora!Tora!") -- 3 
[1, 2, 3] & _length .~ "123" -- [1, 2, 3]

至此，我们发现MyLens和库中的Lens并没有什么使用上的不同（毕竟是等价的）。而MyLens这么直观，为何库中Lens要采用这种形式呢？我现在是不知道的，但我仍然被库中的Lens所折服：

(a -> f b) -> (s -> f t)形式优美，跟CPS变换有很深的联系。
通过取不同的函子，能达到不同层次的抽象，实现不同的行为。（而MyLens就做不了很多其它抽象了。比如说Lens库中的Traversal，不过这个其实是我自己写不出行为一致的代码，从而下的断言）

下面开始解答前面的一些问题：

Co-Algebra for Co-State Co-Monad?

回到前文提到，ekmett大神说过：

一个Lens不过就是Coalgebra for the CoState Comonad，这有什么难理解的。

我们也验证一下这句abstract nonsense

首先CoState Comonad就是Haskell中的Store

data Store s a = Store (s->a) s

也就是(s->a, s)。它是一个Comonad，自然也就是一个Endofunctor

然后CoAlgebra for Endofunctor f就是一个a，和一个态射

type CoAlgebra f a = a -> f a

最后Coalgebra for the CoState Comonad就是

CoAlgebra (Store s) a   
-- ->   
a -> Store s a  
 -- ~   a ->(s->a, s)

这玩意儿就是咱们定义的MyLens的初始版本。

哦！这句话原来是这个意思（我怎么还是啥都没学到）

（其实还是costate comonad 之间的自然变换）

Yoneda lemma？

Yoneda lemma说的是，对象A和函子F满足：

$ Nat(Hom(A,-), F) \cong F\ A $

在Haskell中，在*范畴，可以具体写出：

type Yoneda f a = Functor f => forall b. (a -> b) -> f b
-- 与
Functor f => f a
-- 等价

我们观察到forall f. Functor f => (a -> f a) -> f b和形式1是很像的，那有没有可能两种Lens的等价关系可以由Yoneda lemma导出呢？

直觉是对的，但是这里要绕点弯子：

首先Yoneda lemma是对所有的范畴都成立的，我们可以看一下在自函子范畴的形式是怎么样的（伪代码）：

-- eta :: (*->*) —> * -> *, 函子的函子
type Yoneda eta f = Functor f => 
    forall g. Functor g => 
        forall t. (f t -> g t) --f到g的自然变换，也就是函子间的态射，Nat(f, g)
        -> forall t. eta g t

-— Nat(Nat(f,-), eta) 
-- 与
eta f
-- 等价

现在给一个不严谨的证明：

将eta g t = g b，f t = (a, a->t)代入在自函子范畴上的Yoneda lemma，得到

forall g. Functor g => 
    forall t. ((a, a->t) -> g t) 
    -> g b
-- 与
(a, a->b)
-- 等价

（很接近了！）

对形式1中forall t. ((a, a->t) -> g t)进行curry化，得到a -> forall t. (a->t) -> g t。

对forall t. (a->t) -> g t应用*范畴下的Yoneda lemma，替换成g a。

于是形式1等价于

forall g. Functor g => (a -> g a) -> g b

于是就得到了：

forall g. Functor g => (a -> g a) -> f b和(a -> b, a)是等价的！

（目的达成！功德圆满！）

后记

终于能拿两三天来瞅瞅Lens库，着实被Lens库的优美所震撼！然后又按图索骥，自己鼓捣出上面这些东西，真的挺满足的。说是填hole，但其实都是在草稿纸上推的。。。然后灵光一闪填一个函子进去，然后就ok了。不过过程中我是想用idris来证明那些等价关系的，最后发现idris写出来的东西很冗长，于是就算了，毕竟也没用上dt。

然后就是我对MyLens是否能实现相同的Traversal的功能，产生了疑问，直觉告诉我这是不行的。把Traversel看作弱化了的Lens（Functor条件加强了），两者就不等价了，就无法从Traversal推出MyLens了。

关于标题双关：

Lens to Lenses就是从自己写的Lens再看库里的Lens
第一个Lens作动词，想表达focus的意思（生掰），就是关注Lens（及背后的一些东西）

最后望各路大神指正（溜了

前言#

从零开始的getter和setter#

大胆猜想 小心求证#

泛化的版本#

Further more?#

Co-Algebra for Co-State Co-Monad?#

Yoneda lemma？#

后记#

前言