Relens to Lens

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

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

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

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）：

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

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

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的操作了：

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 xLens p1 -- = 1.0
set xLens 10 p2 -- = Point 3.0 10.0

-- 对l1的 终点 的 横坐标 进行get和set
get (endLens >. xLens) l1 -- 3
set (endLens >. xLens) 10 l1 -- ...

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

-- 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的组合模式了：

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作一个变换：

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

总结一下：

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作用的结果：

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 representation：

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的参数的位置调整一下，并提供其中缀形式：

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的第一种形式，没有区别：

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 xLens p1 -- = 1.0
set yLens 10 p2 -- = Point 3.0 10.0

-- 对l1的 终点 的 横坐标 进行get和set
view (endLens . xLens) l1 -- 3
set (endLens . xLens) 10 l1 -- ...

稍微可以复杂点：

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

两者形式的等价性

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

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之间的等价：

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之间的等价：

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 $

（这里用 $A \stackrel{\mathcal{C}}{\longrightarrow} B$ 表示 $\mathrm{Hom}_\mathcal{C}(A, B)$ ）

要证明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\{ 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}$时，我们就可以得到

$ \psi:A \stackrel{\mathbf{Set}}{\longrightarrow} \mathrm{Store}_{S,T}B \cong \mathrm{Store}_{A,B}\stackrel{\mathbf{Set}^\mathcal{C}}{\longrightarrow} \mathrm{Store}_{S,T} $

也就是a -> (s, t -> b)等价于forall x. (a, b->x) -> (s, t->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

## 两者的区别

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

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的概念，它在第一个参数上逆变，第二个参数上协变

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。

那我们是否有：

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

我们尝试证明：

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：

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 b = Yoneda ((a -> b) -> f b)， Yoneda f是一个Strong

…

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

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

-- xLens :: Lens' Point Double
-- xLens = dimap (positionX . snd) (\(x, p) -> p { positionX = x }) . first'

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

Store的题外话

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

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

启发我的是猫老师

@CrLF0710 的这篇文章

CrLF0710：在Rust里访问所有者的数据

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

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

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

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

用Rust表达就是：

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
    }
}

那么文章就到这里结束了，晚安

Relens to Lens#

Lens要解决的问题#

抽象的getter和setter#

从另外一个角度归纳出lens#

两者形式的等价性#

进一步的抽象#

Store的题外话#

Relens to Lens

Lens要解决的问题

抽象的getter和setter

从另外一个角度归纳出lens

两者形式的等价性

进一步的抽象

Store的题外话