对于Control.Lens.Setter来说,将类型包装在functors中是否是冗余的?

22

我正在观看介绍Control.Lens视频
这让我想知道为什么需要在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)
2个回答

21
这是一个非常好的问题,需要进行一些详细的解释。
首先,我想温柔地纠正您一个错误:最近版本中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

Lens

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包的最佳卖点。
  • 构建大量元组,只为稍后将它们分解,这样会浪费很多内存。
  • 最重要的问题:接受getter(例如view)和setter(例如over)的函数无法使用镜头,因为它们的类型非常不同。

如果不能解决上述问题,那么写库还有什么意义呢?我们不希望用户必须经常考虑光学学科的UML层次结构,每次移动上下文时都要调整函数调用。

那么目前的问题是:我们能否写出一个类型为Lens的类型,使其自动成为GetterSetter?为此,我们必须转换GetterSetter的类型。

Getter

  • 首先注意,s -> a等效于forall r. (a -> r) -> s -> r。这种转换为续定式样式远非明显。您可能能够将此转换直观地理解为:“类型为s -> a的函数承诺,给定任何s,您都可以向我提供a。但是,这应该等同于一个承诺,即给定将a映射到r的函数,您也可以向我提供将s映射到r的函数。”也许?也许不是。这里可能涉及一种信仰跳跃。

  • 现在定义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 aa是相同的。

  • 现在请注意,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的选择抽象为一个量化变量。正如lens wiki所说,所有ConstIdentity共同之处在于它们都是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` 包最初的动机。正如 推导维基页面 所解释的那样,你可以从 `.` 和某些函数的有趣行为开始,然后推出光学元素。但是我认为我们创造的这条路径更好地解释了你提出的问题,这也是我一开始遇到的一个大问题。我还想向你介绍 茶话会上的光学元素,它提供了另外一个推导。

我认为这些多个推导是一件好事,也是检测 `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。我们可以将此段落归类为“关于lens的更多信息,您可能并不想知道”。

6
在某种意义上,lens将setter包装在函数返回中的原因是,否则它们将会太强大了。
实际上,当使用setter时,该函数将被实例化为Identity,这与您提议的签名完全相同。但是,setter的实现不能利用这一点。使用您的签名,我可以编写类似以下内容的代码:
zlens :: MySetter Point Point Int Int
zlens _f p = p  -- no z here!

这就是使用Functor签名时不可能的,因为zlens需要普遍量化functor,它不能知道如何将结果注入f包装器。获取functor类型的唯一方法是首先将setter函数应用于正确类型的字段!
所以,这只是一个好的自由定理。
更实际地说,我们需要functor包装器来保持兼容性。虽然您可以在没有此包装器的情况下定义setters,但对于getters而言则不可能,因为这些使用Const而不是Identity,并且需要该类型构造函数的第一个参数中的添加多态性。通过要求所有镜头风味(仅具有不同的类约束)都需要这样的包装器,我们可以为它们使用相同的组合器,但类型系统将始终将功能折叠到实际适用于情况的任何功能上。
†思考一下,保证实际上并不强...我仍然可以用一些fmap(const old)欺骗手法来破坏它,但这肯定不是一个可能发生错误的事情。

你能否详细解释一下为什么将类型包装在一个函子中会防止这种情况发生?即使类型被包装,我仍然可以做完全相同的事情:zlens f p = fmap (const p) $ f 0 -- zlens :: Lens' Point Int - qwe
@qwe 因此我的脚注。但是至少,使用包装器时,您必须将提供的函数应用于正确类型的某个值。 - leftaroundabout
那么我还不确定它是必要的。可能与单子和副作用计算有关? - qwe
1
如果你创建了一个类型转换Setter,我认为你无法通过欺骗来绕过它。但当然,并非总是可用。 - dfeuer

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接