Relens to Lens

之前也写过一篇lens的文章，学了新知识之后，现在看起来觉得不满意，于是打算重新再写一篇。

Lens的设计十分的精妙，是数学指导编程的一个非常典型的案例。

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的第二个端点的横坐标：

xxxxxxxxxx
l1 {segmentEnd = (segmentEnd l1) {positionX = 10}}
-- 如果没有部分修改record的语法，这样的工作会更麻烦，只能用模式匹配一项项填

如果数据结构更加复杂的时候，代码就会变得更冗长。但如果用lens，刚刚的表达式就可以重写为：

xxxxxxxxxx
l1 & endLens . xLens .~ 10

其中(endLens . xLens)就是一个透镜组，先访问end，再访问x，.~就是set。那么之前需要用语法特殊解决的问题，就可以靠lens的组合来解决（解决一个带field语法的语言没有的问题）。

• remark1: lens本质上是提供了a是b“内部”组件的一个证明，或者说提供了b到a的一个访问路径。

• remark2: lens对于record或者struct来说，相当于一个field path。

抽象的getter和setter

对数据的操作，无非是get和set。get是从父组件拿到某个子组件；set在函数式语言的语境下是将修改了某个子组件的父组件复制一份，也就是所谓的写时复制（Copy on Write）：

xxxxxxxxxx
-- a是b的“内部”
get :: b -> a
set :: b -> a -> b

将其组合起来就得到了Lens的第一种形式：

x
newtype Lens b a = Lens { getLens :: b -> (a, a->b) }
​
-- Lens的组合
infixr 9 >.
(>.) :: Lens c b -> Lens b a -> Lens c a
(Lens c2b) >. (Lens b2a) = Lens $ \c -> 
    let (bc, b) = c2b c in
    let (ab, a) = b2a b in 
    (bc . ab, a)

假如现在有一个b到a的lens，我们就可以对b的a进行get或set的操作了：

xxxxxxxxxx
set (endLens >. xLens) 10 l1 -- ...
set :: Lens b a -> a -> b -> b
set lens = flip $ snd . (getLens lens) 
​
get :: Lens b a -> b -> a
get lens = fst . (getLens lens) 
​
-- 从Point到其横纵坐标的Lens，类似可以写出endLens，这些代码可以用模板来生成。
xLens, yLens :: Lens Point Double
xLens = Lens (\p -> (\x -> p { positionX = x }, positionX p))
yLens = Lens (\p -> (\y -> p { positionY = y }, positionY p))
​
-- 对p1的get和set
get xGS p1 -- = 1.0
set yGS p2 10 -- = Point 3.0 10.0
​
-- 对l1的 终点 的 横坐标 进行get和set
get (endLens >. xLens) l1 -- 3
set (endLens >. xLens) l1 10 -- ...

如果不限制set之后得到类型前后一致，我们还可以得到第一种形式的Lens的完全形式：

x
newtype Lens s t a b = Lens { getLens :: s -> (a, b -> t)) }
-- a是s的“内部”，将a替换为b之后得到t
newtype Lens s t a b = Lens { getLens :: s -> (a, b -> t) }
-- getter :: s -> a
-- setter :: s -> b -> t

其余代码的实现方式不改变。

remark: Lens是Costate Comonad的Coalgebra。

从另外一个角度归纳出lens

其实平常我们就已经在用一些get和set的组合模式了：

x
fmap     :: (a -> b) -> (f a -> f b)     -- f a的setter：将f a中的a修改为b，得到f b
traverse :: (a -> f b) -> t a -> f (t b) -- 将t a中的a修改为f b，得到f (t b)
modify   :: (a -> b) -> (s -> t)         -- 上面的一般情况：将s中的a修改为b，得到t
​
fold :: t m -> m -- 从t m中得到m
get  :: b -> a   -- 从b中得到a

统一一下形式，对get和fold作一个变换：

x
fold' :: (m -> r) -> (t m -> r)
get'  :: (a -> r) -> (b -> r) -- get' id b -> a

总结一下：

xxxxxxxxxx
fold :: (Foldable t, Monoid m) => Getter (t m) m
type Setter s t a b  = (a -> b) -> (s -> t)
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
type Getter s a = forall r. (a -> r) -> (b -> r)
​
modify   :: Setter s t a b
fmap     :: Setter (f a) (f b) a b
get      :: Getter s a
fold     :: (Foldable t, Monoid m) => Getter (t m) m
traverse :: Traversable t => Traversal (t a) (t b) a b

观察到，这时将Getter中的r看作常函子Const r作用的结果；将Setter中的a和t看作是单位函子Identity作用的结果：

xxxxxxxxxx
type Setter s t a b    =           (a -> Identity b) -> (s -> Identity t)
type Getter s a        = forall r. (a -> Const r b) -> (b -> Const r a)
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

这时就可以归纳出一个统一性非常强的形式，这将作为Lens的第二种形式，称为van Laarhoven form：

x
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
type Lens' b a = Lens b b a a
-- Lens的组合就是函数的组合(.)
​
-- 对f的细化我们就可以得到Setter, Getter, Traversal
-- f取Identify
type Setter s t a b = (a -> Identity b) -> (s -> Identity t) 
-- f取可应用函子
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
-- f取反变函子，常函子同时是一个反变函子和函子
type Getter s a = forall f. (Contravariant f, Functor f) => (a -> f a) -> s -> f s
-- f取反变函子，同时为可应用函子
type Fold s a = forall f. (Contravariant f, Applicative f) => (a -> f a) -> s -> f s
​
set      :: Setter s t a b         -> b -> (s -> t)
get      :: Getter s a             -> s -> a
modify   :: Setter s t a b         -> (a -> b) -> (s -> t)
fmap     :: Setter (f a) (f b) a b -> (a -> b) -> (f a -> f b)
traverse :: Traversable t => Traversal (t a) (t b) a b
mapped   :: Functor f     => Setter (f a) (f b) a b
folded   :: Foldable t    => Fold (t a) a

在习惯上，我们称modify为over，get称为view并将set的参数的位置调整一下，并提供其中缀形式：

x
set  :: Setter s t a b -> s -> b -> t
view :: Getter s a     -> s -> a
over :: Setter s t a b -> (a -> b) -> (s -> t)
​
infixl 8 ^.
(^.) = flip view
​
infixr 4 %~
(%~) = over
​
infixr 4 .~
(.~) = set
​
infixl 1 & 
x & f = f x

应用起来和lens的第一种形式，没有区别：

x
xLens, yLens :: Lens' Point Double
xLens f p = fmap (\x -> p { positionX = x }) $ f (positionX p)
yLens f p = fmap (\x -> p { positionY = y }) $ f (positionY p)
​
-- 对p1的get和set
view xGS p1 -- = 1.0
set yGS p2 10 -- = Point 3.0 10.0
​
-- 对l1的 终点 的 横坐标 进行get和set
view (endLens . xLens) l1 -- 3
set (endLens . xLens) l1 10 -- ...

稍微可以复杂点：

x
over (_1.mapped._2.mapped) toUpper ([(42, "hello")],"world")
-- ([(42, "HELLO")],"world")

两者形式的等价性

那么Lens的这两种形式是否等价呢？我们比较两者形式：

x
type Lens1 a b s t = s -> (a, b -> t)
type Lens2 a b s t = forall f. Functor f => (a -> f b) -> s -> f t
--                   s -> forall f. Functor f => (a -> f b) -> f t

除去相同的部分s->，证明两者等价相当于证明(a, b -> t)和forall f. Functor f => (a -> f b) -> f t之间的等价：

x
phi :: (a, b -> t) -> (forall f. Functor f => (a -> f b) -> f t)
phi (a, g) = \f -> fmap g (f a)
​
psi :: (forall f. (a -> f b) -> f t) -> (a, b -> t)
psi h = h (\a -> (a, id))
​
-- 容易验证
psi . phi = id
phi . psi = id

我们还能证明([a], [b] -> t)和forall f. Applicative f => (a -> f b) -> f t之间的等价：

xxxxxxxxxx
phi :: ([a], [b] -> t) -> (forall f. Applicative f => (a -> f b) -> f t)
phi (as, g) = \f -> fmap g (traverse f as)
​
psi :: (forall f. (a -> f b) -> f t) -> ([a], [b] -> t)
psi h = h (\a -> ([a], id))
​
-- 容易验证
psi . phi = id
phi . psi = id

其实这两个证明是可以从米田引理中导出来的。

米田引理：对于局部小范畴$\mathcal{C}$中的对象$A$，以及函子$F: \mathcal{C} \rightarrow \mathbf{Set}$，函子$\left(A \stackrel{\mathcal{C}}{\longrightarrow} -\right)$到$F$的自然变换与$F\,A$之间一一对应：

$$\psi: \left(A \stackrel{\mathcal{C}}{\longrightarrow} -\right) \stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} F \cong F\,A$$

要证明Lens两种形式的等价，我们需要先证明一个引理：

引理1：记函子$\mathrm{Store}_{A,B} X = A \times (B \stackrel{\mathcal{C}}{\longrightarrow} X)$，有$\psi:A \stackrel{\mathbf{Set}}{\longrightarrow} F\,B \cong \mathrm{Store}_{A,B}\stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} F$

proof:

$$\begin{align} \psi:A \stackrel{\mathbf{Set}}{\longrightarrow} F\,B & &\\ & \cong \{ yoneda\} \\ & A \stackrel{\mathbf{Set}}{\longrightarrow} \left(\left(B \stackrel{\mathcal{C}}{\longrightarrow} -\right) \stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} F\right) \\ & \cong \\ & \left(A \stackrel{\mathbf{Set}}{\longrightarrow} \left(B \stackrel{\mathcal{C}}{\longrightarrow} -\right) \right)\stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} F \\ & \cong \{ uncurry\}\\ & \left(A \times \left(B \stackrel{\mathcal{C}}{\longrightarrow} -\right) \right)\stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} F\\ & \cong \\ &\mathbf{Store}_{A,B}\stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} F \end{align}$$

那么两者Lens之间的等价相当于证明：

定理1：$\mathrm{Store}_{A,B} C \cong \left(A \stackrel{\mathbf{Set}}{\longrightarrow} -\,B\right) \stackrel{\mathbf{Set}^{\mathbf{Set}^\mathcal{C}}}{\longrightarrow} -\,C$

proof:

$$\begin{align} \psi:\left(A \stackrel{\mathbf{Set}}{\longrightarrow} -\,B\right) \stackrel{\mathbf{Set}^{\mathbf{Set}^\mathcal{C}}}{\longrightarrow} -\,C &\\ & \cong \{lemma_1\}\\ & \left(\mathrm{Store}_{A,B}\stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} -\right) \stackrel{\mathbf{Set}^{\mathbf{Set}^\mathcal{C}}}{\longrightarrow} -\,C \\ & \cong \{yoneda\} \\ & \mathrm{Store}_{A,B} C \end{align}$$

 

即$\psi:\mathrm{Store}_{A,B} C \cong \forall F: Functor. (A \rightarrow F\,B)\rightarrow F\,C$。同样的我们还能证明$\psi:\mathrm{Store}_{[A],[B]} C \cong \forall F: Applicative. (A \rightarrow F\,B)\rightarrow F\,C$。

其实引理1我们还可以导出第三种形式的Lens，当我们取$F = \mathrm{Store}_{S, T}$时，我们就可以得到

也就是a -> (s, t -> b)等价于forall x. (a, b->x) -> (s, t->x).

x
type Lens s t a b = forall x. (s, t->x) -> (a, b->x)

remark: Lens就是Costate Comonad之间的自然变换！

从米田嵌入的角度来看——米田嵌入就是一个函子$\mathrm{y}: \mathcal{C} \rightarrow \mathbf{Set}^{\mathcal{C}^\mathrm{op}}$，将范畴$\mathcal{C}$“嵌入”到一个函子范畴$\mathbf{Set}^{\mathcal{C}^\mathrm{op}}$中，用函子和自然变换表示$\mathcal{C}$中的对象和态射，米田引理就表示为$\psi: \mathrm{y}\,A \stackrel{\mathbf{Set}^{\mathcal{C}^\mathrm{op}}}{\longrightarrow} F \cong F\,A$——

• 形式1的lens将getter和setter嵌入到函子范畴中，就得到了形式3的lens
• 将形式3的lens又嵌入到了其函子范畴中，就得到了形式2的lens
• 最终用函子的函子的自然变换表示原来的getter和setter

两者的区别

那么说完了两者的等价性，那么这两种形式之间有什么又有什么区别呢。

x
type Lens1 s t a b = s -> (a, b -> t)
type Lens2 s t a b  = forall f. Functor f => (a -> f b) -> s -> f t

感性地来说，函子范畴地性质会比原来的范畴有更好地性质，能完成原来不可行地构造（比如说求一些极限之类的）。而在使用上，大概有两点区别：

• 第二种形式的Lens的组合是函数组合，实现上比第一种形式要简单，性能会比第一种要好
• 对形式2的自由变量f的范围进行限制的话，就可以得到Lens的不同“子功能”，就如第三节得到的几种形式。然后就可以分模块针对不同的功能实现不同的操作，这在工程上也是十分有益的。

对自由变量f的范围的不同的限制，这就有了现在lens库中不同模块之间的UML图：

remark: traverse就不能用第一种形式的Lens来表达。

进一步的抽象

在进一步抽象之前，还得引入Profunctor的概念，它在第一个参数上逆变，第二个参数上协变

x
class Profunctor p where
    dimap :: (b -> a) -> (c -> d) -> p a c -> p b d
    dimap f g = lmap f . rmap g
    
    lmap :: (b -> a) -> p a c -> p b c
    lmap f = dimap f id
    
    rmap :: (c -> d) -> p a c -> p a d
    rmap f = dimap id f

(->)就是最典型的Profuncto。在第二种形式的Lens中，(- -> f -)也是一个Profunctor。在第三种形式中$\mathrm{Store}_{-_2, -_1}X$也是Profunctor。

那我们是否有：

x
type Lens s t a b = forall p. Profunctor p. p a b -> p s t

我们尝试证明：

x
phi :: (s -> (a, b -> t)) -> (forall p. Profunctor p. p a b -> p s t)
phi lens = \pab -> lmap (fst . lens) (\(b, s) -> snd (lens s) b) (_ pab)
​
psi :: (forall p. Profunctor p. p a b -> p s t) -> (s -> (a, b -> t))
psi h = h (\a -> (a, id))
-- (- -> (a, -))是profunctor
​
-- 需要满足
phi . psi = id
psi . phi = id

洞_中的的类型是p a b -> p (a, s) (b, s)，Profunctor还缺了这么一个函数使得和第一种形式的Lens等价。补充之后，我们就得到了Strong Profunctor：

xxxxxxxxxx
class Profunctor p => Strong p where
    first' :: p a b -> p (a, c) (b, c) -- 逆变位到协变位可以引入一个id
    first' = dimap swap swap . second'
    
    second' :: p a b -> p (c, a) (c, b)
    second' = dimap swap swap . first'

• (->)当然是Strong
• newtype Star f a b = Star (a -> f b)，Star f是一个Strong
• newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)， Yoneda f是一个Strong

...

于是我们就得到了第四种形式的Lens：

x
type Lens s t a b = forall p. Strong p. p a b -> p s t

不过我们通常还是使用第二种形式的Lens。可能是因为懒得去实现Strong相关的typeclass了吧

Store的题外话

我们通常笑话Haskell为了解决不存在的问题（访问record深层数据）而发明了Lens。那是不是Lens对于本身带有field语法的语言就没有什么卵用呢？以前我是这么觉得的，甚至觉得js上的Lens库是多此一举。

但最近我在Rust中找到这个问题的一部分答案，当然并不是把Lens搬到Rust上，而是发现Lens的一部分——Store在Rust中存在着它的价值。（在Haskell中我一直想不到这玩意儿究竟有什么用）

启发我的是猫老师的这篇文章

在Rust里访问所有者的数据 - 知乎 (zhihu.com)

我这里只是简单复述一下里面的观点。

在日常编程中，很可能会遇到一种情况：子组件引用父组件的其它部分进行操作。那么在c/cpp或者其它语言中，这就会造成自引用。在rust中，这样的代码是无法通过borrow check的，这时候有几种可能的操作：

• 用裸指针代替引用，然后将父组件Pin起来
• 用索引代替引用，然后用于索引父组件中的某个Vec

那么还有一种方法就是用Store表示对子组件的引用。t是s的子组件，用Store s t = (s, s -> t)来表示对t的引用，持有Store s t作为t的引用的同时，仍然可以访问到父组件s的引用。

用Rust表达就是：

x
struct Store<'a, S: ?Sized, T: ?Sized> {
    stored: &'a S,
    accessor: fn(&S) -> &T,
}
​
impl<'a, S: ?Sized, T: ?Sized> Deref for Store<'a, S, T> {
    type Target = T;
    fn deref(&self) -> &Self::Target {
        (self.accessor)(self.stored)
    }
}
​
impl<'a, S: ?Sized, T: ?Sized> Store<'a, S, T> {
    fn pos(&self) -> &'a S {
        self.stored
    }
}
​
// 实现子组件上的方法
impl Store<'_, Container, Item> {
    fn foo(&self) {
        //...self.pos().xxx + self.yyy
    }
}