镜头法则：他们想告诉我什么？

Question

我看过各种版本的镜头法则。不确定它们是否都是等效的，所以为了明确起见，我将使用 StackOverflow 上的版本来对抗标签 Lenses [Edward Kmett ~ 5 年前]

（我问是因为我想要更多地处理双向编程。）

使用a作为结构，b作为结构中的组件/值：

1. get (set b a) = b

好的。你得到的就是你付出的。对于任何自称为数据结构/容器的东西来说似乎都是必不可少的。我可能有一个小问题：最初的a 来自哪里？我可以直接去get a吗？这意味着什么？

1. get (set b' (set b a)) = b'

？我相信这是为了告诉我：你得到的是你最后放的东西（而你之前放的任何东西都永远丢失了）。但实际上并没有这么说。它不（例如）排除镜头是堆栈内-a - 即get 的行为类似于pop。所以如果我再做一次get，它可能会返回之前的b。 IOW 它需要说：一旦你已经set b' (whatever-a)，get 将永远返回b' ad infinitum。

This is law 有时写成以下形式：set b' (set b a) = set b' a。但我根本不喜欢这样，这让我想到：

1. set (get a) a = a

把你已经拥有的东西放在一边没有任何作用。 （这似乎是一件几乎没有意思的事情：它不是遵循第 1 条吗？）但是对结构的相等性测试正在打破抽象。我们（作为结构的客户）并不关心结构在内部是如何组织的。我们的接口是根据方法get、set。放置您已经拥有的东西可能会改变我们所关心的结构的价值——只要 get 返回我们放置的值。

如果set (get a) a 的值/内容有什么重要的，那不能用get/set 来表达吗？如果不能，我们为什么要关心？

---

所有这些定律都是用一个镜头来描述的。因此，如果结构只是一个“插槽”，他们会坚持下去——这似乎是很多机器，也就是“变量”。

似乎缺少的是如何组合不同的镜头来处理更复杂的结构。这样的结构允许每个镜头正交工作。我相信有范拉霍文定律：

-- I need two lenses, so I'll use get', set' as well as get, set get' (set b (set' b' a)) = b'

我不需要这样的法律吗？请解释一下。

Answer 1

如果你是带着对双向编程的期望来的，我并不奇怪你会感到困惑，AntC。

FAQ 页面资源 [1] 引用了 Pierce 和 Voigtländer（他们都制定了类似的法律）；但实际上他们正在使用完全不同的语义。例如 Pierce 等人 2005 年的论文：

镜头的get 组件与视图定义完全对应。为了支持组合方法，我们认为视图状态是一个完整的数据库（而不是像许多视图处理中的单个关系）。

所以这些是数据库意义上的“视图”（这导致了光学术语的双关语）。总是有一个“基本”模式定义（数据结构），镜头可以转换视图。 Pierce 和 Voigtländer 都在尝试管理数据结构的“大小和形状”，以保持它们之间的转换。那么难怪他们会认为“基地”是内容的主要持有者，而镜头只是透视的机制。

有了函数引用，就没有这样的困难了。镜头专注于单个数据结构中的“插槽”。并且结构被视为抽象。

如果功能引用方法想要根据“插槽”制定法律，并专门处理 Pierce 所谓的遗忘镜头，它必须采用外部结构部分的语义镜头。 Voigtländer 等人 2012 年的论文使用 res（残差）函数处理了什么；或之前关于数据库视图的工作 [Bancilhon & Spyratos 1981] 称为“补充”。

O.P. 中引用的法律中的set 函数是遗忘，因为它忽略了“插槽”的当前内容并覆盖它。镜头不一定是这样的。最近的治疗使用upd 函数（带有附加参数f 用于更新以应用于当前值）。注意

get (upd f a) = f (get a).
get (set b a) = b = get (upd (const b) a).   (Law 1)

除了并非所有镜头upd 操作都遵守这些等价性。例如，一个镜头的巧妙技巧是gets 来自日期的day 插槽；但其upd (+ 1) 会增加整个日期。 getDay (updDay (+ 1) (Date {year = 2017, month = 2, day = 28}) ) 返回 1，而不是 29。

针对O.P.中的具体问题

1. “slight q”：初始a来自create函数[Voigtländer] 还有一堆create/get 法律。
   • 或者已经在“基础”架构中 [Pierce]。
2. @Amadan 的回答是正确的。 get 和 set 是纯函数。
   • get 必须返回最后的 set，根据法则 1。所以法则 2 似乎毫无意义。
3. 对于 Pierce 和 Voigtländer 来说很重要，因为他们认为“基础”至关重要。
   • 对于函数引用（如果数据结构应该是抽象的），
   • 陈述这条法则是在打破抽象。
   • 它也没有在结构中说明其他镜头的行为， 如果set 改变值——这肯定是 Lens 用户想要理解的。
   • 所以又显得毫无意义。
   • 请注意，无论是 Pierce 还是 Voigtländer 的方法都不会期望超过一个 Lens。

---

如果两个 Lenses 专注于结构中的独立插槽，则这两个都成立：

-- continuing to use get'/set' as well as get/set
 ∀ b b' . get' (set b (set' b' a)) = b'     -- law for set' inside set
 ∀ b' b . get (set' b' (set b a)) = b       -- law for set inside set'

如果两个镜头干涉/重叠，则这两个公式都不成立（通常对于 set、set' 域中的所有值）。

因此，从上面的getDay/updDayfocussing 内部getDate/setDate 中采取“最糟糕”但仍然合理的情况： 法则 1 适用于getDate/setDate；但是updDay 的行为不像set 的一个版本。 法则 2 和 3 成立（但似乎毫无意义）。

没有任何规律可以让我们有效地描述它们之间的相互作用。 我想我们能做的最好的事情就是分离聚焦在同一结构内的镜头 分为相互干扰/不相互干扰的分组。

总的来说，我认为镜头法则对于理解现在使用的镜头没有太大帮助。

[1]https://github.com/ekmett/lens/wiki/FAQ#lens-resources

Answer 2

我以前没有使用过这种形式，所以它可能会在我的回答中显示出来。

1. 这是一个数学定律。 a 来自哪里并不重要，只要满足相关的数学要求即可。在编程中，您可以在代码中定义它，从文件中加载它，从网络调用中解析它，递归地构建它；随便。

2. 不能这么说。 get 不返回新结构，只返回值；镜头的全部意义在于为不可变、无副作用结构创建一个框架。设a' 为(set b' (set b a))； get a' 每次都会返回b'，因为a' 不能改变，而get 是纯函数；没有地方可以存储状态。您的“get 将始终返回 b' ad infinitum”假定对于纯函数始终为真，无需进一步规定。要实现堆栈，您需要以下两件事之一：要么是可变的、有副作用的（因此 get a == get a 不一定是真的），要么操作函数需要返回新的堆栈 - put 和get。

3. 我没能为此构造一个反例，可能是因为它直觉性很强。这里有一个非常脆弱的反例：让get a (Container b _) = b，set b (Container b c) = Container b (c + 1)，set b (Container b' _) = Container b 0。此外，让a = Container b' 0 和b != b'。第一定律：get (set b a) = get (Container b 0) = b - 好的。第二定律：get (set b' (set b a)) = get (set b' (Container b 0)) = get (Container b' 0) = b' - 好的。但是，set (get a) a = set (get (Container b' 0)) (Container b' 0) = set b' (Container b') = Container b' 1 != a - 不行。因此，它不遵循第一定律。没有这个，你不能测试两个结构的相等性，而是需要迭代每个访问器来证明这两个结构是相等的（作为一个 JavaScript 程序员，让我告诉你：没有对象标识函数真的很尴尬）。

4. 确实如此。想象一下：set b a = Container b，get (Container b) = b。第一定律：get (set b a) = get (Container b) = b - 好的。第二定律：get (set b' (set b a)) = get (set b' (Container b)) = get (Container b') = b' - OK；第三定律：让a == Container b：set (get a) a = set (get (Container b)) a = set b a = Container b = a - OK。所有三个定律都对这个非常简单（而且有点明显错误）的定义感到满意。现在让我们添加set' b a = Container' b、get' (Container' b) = b)，看看会发生什么：get' (set b (set' b' a)) = get' (set b (Container' b')) = get' (Container b)... 这无法评估。哎呀。或者，想象一下：set b a = Container b 0、get (Container b _) = b、set' b a = Container b 1、get' (Container b _) = b。在这种情况下，get' (set b (set' b' a)) = get' (set b (Container b' 1)) = get' (Container b 0) = b - 不行。该定律保证set' 设置的值将保留在结构中，即使我们应用set（在此示例中绝对不是这种情况）。