Control.Lens.Setter 在仿函数中包装类型不是多余的吗?

Isn't it redundant for Control.Lens.Setter to wrap types in functors?

我在看Control.Lens介绍video
这让我想知道为什么 Setter 类型需要将东西包装在仿函数中。
它(大致)定义如下:

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

假设我有一个名为 Point 的数据,其定义如下:

data Point = Point { _x :: Int, _y :: Int } deriving Show

然后我可以这样写自己的xlens

type MySetter s t a b = (a -> b) -> s -> t
xlens :: MySetter Point Point Int Int
xlens f p = p { _x = f (_x p) }

我可以这样使用它:

p = Point 100 200
xlens (+1) p -- Results in Point { _x = 101, _y = 200 }

通过使用Control.Lens,实现同样的效果:

over x (+1) p

以下代表:

x :: Functor f => (Int -> f Int) -> Point -> f Point
over :: Setter Point Point Int Int -> (Int -> Int) -> Point -> Point

所以我的问题是,既然可以用更简单的方式实现相同的效果,为什么 Control.Lens 将东西包装在仿函数中?它对我来说看起来是多余的,因为我的 xlensControl.Lensover x 一样。

郑重声明,我也可以用同样的方式连接我的镜头:

data Atom = Atom { _element :: String, _pos :: Point } deriving Show
poslens :: MySetter Atom Atom Point Point
poslens f a = a { _pos = f (_pos a) }

a = Atom "Oxygen" p
(poslens . xlens) :: (Int -> Int) -> Atom -> Atom
(poslens . xlens) (+1) a -- Results in Atom "Oxygen" (Point 101 200)

从某种意义上说,lens 将 setter 包装在仿函数-returns 中的原因是它们 太强大了 否则。

事实上,当使用setter时,函子无论如何都会被实例化为Identity,这与您建议的签名完全一样。但是,setter 的实现不能利用这个事实。有了你的签名,我可以写出类似

的东西
zlens :: MySetter Point Point Int Int
zlens _f p = p  -- no z here!

嗯,这对于基于 Functor 的签名是不可能的,因为 zlens 需要在函子上进行普遍量化,它不知道如何将结果注入 f 包装纸。获得仿函数类型结果的唯一方法是首先将 setter-函数应用于正确类型的字段!

所以,这只是一个很好的自由定理

更实际地说,我们需要 兼容性 的仿函数包装器。虽然您可以在没有此包装的情况下定义 setters,但这对于 getter 是不可能的,因为它们使用 Const 而不是 Identity,并且需要在此类型构造函数的第一个参数中添加了多态性。通过为 all 镜头风格(仅具有不同的 class 约束)要求这样的包装器,我们可以对所有这些使用相同的组合器,但类型系统总是会崩溃功能细化到实际适用于该情况的任何功能。


想想看,保底其实不是很强...我还是可以用一些fmap (const old)作弊来颠覆的,但是这当然不是现实中可能错误发生的事情。

这是一个很好的问题,需要进行一些拆解。

我想马上纠正你的一点:lens 包中的 Setter 的类型在最新版本中是

type Setter s t a b = (a -> Identity b) -> s -> Identity t

看不到 Functor……还没有。

但这并不会使您的问题无效。为什么类型不是简单的

type Setter s t a b = (a -> b) -> s -> t

为此我们首先要谈谈 Lens

镜头

A Lens 是一种允许我们执行 getter 和 setter 操作的类型。这两个组合形成了一个漂亮的功能参考。

Lens 类型的简单选择是:

type Getter s a = s -> a
type Setter s t a b = (a -> b) -> s -> t
type Lens s t a b = (Getter s a, Setter s t a b)

然而,这种类型令人非常不满意。

  • 无法与.组合,这可能是lens包的最大卖点。
  • 构建大量元组,稍后才将它们分开,这在内存效率上相当低下。
  • 大问题:采用 getters(如 view)和 setters(如 over)的函数不能采用镜头,因为它们的类型非常不同.

如果最后一个问题没有解决,为什么还要费心去写一个库呢?我们不希望用户不得不不断地思考他们在光学的 UML 层次结构中的位置,每次向上或向下移动时调整他们的函数调用。

现在的问题是:有没有一种类型我们可以为 Lens 写下来,这样它 自动 既是 Getter 又是Setter?为此,我们必须转换 GetterSetter.

的类型

Getter

  • 首先注意s -> a等价于forall r. (a -> r) -> s -> r。这种向连续传球风格的转变远非显而易见。您可能会这样理解这种转变:"A function of type s -> a is a promise that given any s you can hand me an a. But that should be equivalent to the promise that given a function that maps a to r you can hand me a function that maps s to r also." 也许吧?也许不吧。这里可能涉及信仰的飞跃。

  • 现在定义newtype Const r a = Const r deriving Functor。请注意 Const r a 在数学上和运行时与 r 相同。

  • 现在注意type Getter s a = forall r. (a -> r) -> s -> r可以改写为type Getter s t a b = forall r. (a -> Const r b) -> s -> Const r t。尽管我们为自己引入了新的类型变量和精神痛苦,但这种类型在数学上仍然与我们开始时的相同 (s -> a).

Setter

  • 定义 newtype Identity a = Identity a。请注意 Identity a 在数学上和运行时与 a 相同。

  • 现在请注意 type Setter s t a b = (a -> Identity b) -> s -> Identity t 仍然与我们开始时使用的类型相同。

一起

有了这份文书工作,我们能否将 setter 和 getter 统一为一个 Lens 类型?

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

嗯,这是Haskell,我们可以将IdentityConst的选择抽象为一个量化变量。正如 the lens wiki saysConstIdentity 的共同点是每个都是 Functor。然后我们选择它作为这些类型的统一点:

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

(选择Functor还有其他原因,比如用自由定理来证明泛函引用定律。但是我们会在这里挥手一点时间。)那forall f 就像 forall r。上面 - 它让类型的消费者选择如何填写变量。填写一个 Identity,你会得到一个 setter。填写一个Const a,你会得到一个getter。正是通过沿途选择细小而谨慎的转变,我们才能够到达这一点。

注意事项

请务必注意,此推导 不是 lens 包的原始动机。作为 Derivation wiki page states explains, you can start from the interesting behavior of (.) with certain functions and tease out optics from there. But I think this path we carved out is a little better at explaining the question you posed, which was a big question I had starting out too. I also want to refer you to lens over tea,它提供了 另一个 推导。

我认为这些多重推导是一件好事,也是 lens 设计是否健康的一种试纸。我们能够从不同的角度得出相同的优雅解决方案,这意味着这种抽象是稳健的,并且得到不同直觉和数学的良好支持。

最近lens我也撒了一点关于Setter的类型。其实是

type Setter s t a b = forall f. Settable f => (a -> f b) -> s -> t b

这是另一个在光学类型中抽象出高阶类型以提供图书馆用户更好体验的例子。几乎总是 f 将被实例化为 Identity,因为存在 instance Settable Identity。但是,有时您可能希望将 setter 传递给 backwards 函数,该函数将 f 固定为 Backwards Identity。我们大概可以把这段归类为"more information about lens than you probably wanted to know."