共代数更新透镜：一种用于双向变换的数学结构

可在www.sciencedirect.com在线获取理论计算机科学电子笔记308（2014）25-48www.elsevier.com/locate/entcs共代数更新透镜丹尼尔·阿曼计算机科学基础实验室，爱丁堡大学，10 Crichton Street，Edinburgh EH89LE，英国Tarmo Uustalu2塔林理工大学控制论研究所，Akadeemia tee 21，12618塔林，爱沙尼亚摘要透镜是在双向变换的上下文中使用的数学结构在本文中，我们引入更新镜头作为普通（非对称）镜头的改进，其中我们区分视图和更新。除了视图集之外，还有一个更新幺半群和幺半群对视图集的操作。 从视图中分离更新允许以其他方式更改源，而不仅仅是将视图合并到源中。 我们还考虑了一个更精细的依赖类型版本 更新镜头。我们用双代数和余代数给出了更新透镜的一些特征，包括O'Connor的余代数和Johnson，Rosebrugh和Wood的普通透镜的代数特征。我们认为转换的意见和更新，张量积的更新镜头和更新镜头的组成。关键词：透镜，余单子，单子，余代数，代数，双代数，分配律，提升，幺半群作用，有向容器1介绍在双向变换的背景下研究透镜。透镜是两个集合上的一个结构，调节作用于它们的行为。考虑确保数据库的两个副本，一个在服务器上，一个在客户端计算机上，无论数据库在客户端如何更改，都保持一致在文献中已经考虑了透镜的许多不同变化。在福斯特等人的开创性工作中。[8]，定义了X集和S集之间的透镜作为一对映射lkp：X→S和upd：X×S→X，服从适当的1d. ed.ac.uk2tarmo@cs.ioc.eehttp://dx.doi.org/10.1016/j.entcs.2014.10.0031571-0661/© 2014 Elsevier B. V.保留所有权利。26D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25往返法在这里，X被认为是一组源，S被认为是一组视图。O’Connor [ Johnson，Rosebrugh和Wood [14]以及Gibbons和Johnson [10]将透镜刻画为集合/S上某个单子的代数。透镜的其他变体包括例如商透镜[9]、对称透镜[12]、（对称）编辑透镜[11]和（不对称）增量透镜[6]。在本文中，我们定义了普通（非对称）透镜的一种变体，我们称之为更新透镜（这个名字是由它们的实际动机所决定的，并且与我们之前关于更新单子的相关工作[3]的术语一致简而言之，更新镜头不同于普通的基于状态的镜头，因为它们区分视图和更新。除了视图集合S之外，还有一个更新幺半群（P，o，n）和一个关于S的动作（P，o，n）。因此，更新映射变成upd：X×P→X，允许其他方式更改源代码，而不仅仅是将视图合并到源代码中。还有一个依赖类型的版本，其中每个视图s：S都有自己的一组更新P s。本文从余单子/函子之间的分配律、余单子的相容合成、余单子/函子到余代数范畴的提升、单子/函子在余单子/函子上的分配律、余自由单子、伴随单子和余单子等标准事实出发，给出了更新透镜在双代数、代数和余代数上的一些刻画.[7、5、4、20、21]。我们研究了视图和更新的转换，更新透镜的张量在附录中，我们还讨论了一个专门的，可初始化的更新镜头。在相关的工作中，与我们最接近的是霍夫曼、皮尔斯和瓦格纳[11]关于（对称）编辑镜头的工作。他们分析对称透镜，并认识到编辑（在我们的术语更新中）通常带有自然的monoidal结构，因此最好使用monoids建模。作为对称设置的结果，编辑透镜由两个幺半群组成，其中upd操作由幺半群同态的适当变化给出。一个不同的相关工作是Diskin、Xiong和Czarnecki [6]以及Johnson和Rosebrugh [15]关于（不对称）三角形透镜的工作。后一组作者还介绍了一个三角形透镜的子类，称为c-透镜，定义更简洁。这两组作者都在研究向源和视图的集合添加更多的结构，将它们视为自反图（或等价的类别）。节点表示源或视图，箭头表示它们之间的增量（在我们的术语更新中）。lkp和upd操作依赖于函性来保证增量的正确和可组合的转换为了可读性，我们为Set（以及建立在Set上的范畴）开发了所有的数学，但是对于我们所做的几乎所有事情，它都可以被任何具有有限乘积的范畴或任何笛卡尔闭范畴所取代。D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）252732普通镜片普通镜片：定义给定一个（视图）集合S，S的普通（非对称）透镜是（源）集合X，并映射lkp：X→S（查看源）和upd：X×S→X（更新一个源）满足条件x=upd（x，lkpx）upd（upd（x，s），sJ）=upd（x，sJ）lkp（upd（x，s））=s也就是说，使以下三个图X伊普？阿利茨？阿利希德（X×S）×SJ.J.公司简介UPDX×SUPD XLKPX×SUPDXX×SUPDJCXzcJS两个普通透镜（X，lkp，upd），（XJ，lkpJ，updJ）之间的映射是映射h：X→XJ（源的转换）满足lkpx=lkpJ（h x）h（upd（x，s））=updJ（h x，s）也就是说，XlkpJchXJJCLKP′X×Sup dJch×S XJ×SJcup d′S SXhXJS的普通透镜和它们之间的映射形成透镜S的类别。运行示例：编辑书店数据库考虑建立一个小型书店的数据库。我们将使用一个非常简单的数据库，仅由一个表组成，包含有关身份的信息（例如，书名和作者姓名，或ISBN），商店里每本书的价格和数量。我们让书，价格，数量代表这些数据的允许值集。我们让源集合X（数据库状态集合）为X=B书.B→价格×数量每一个这样的数据库状态都包含一组当前在数据库中的书籍B，以及B中每一本书的价格和数量的分配。可以给出用于上述源集合X的视图集合S通过sndupd×S28D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25S=Bbook.B→价格3我们使用字母X表示源集合，S表示视图集合，名称lkp表示get，upd表示put。 这可能一开始会让人感到困惑，但与更新单子代数的助记符一致[3]。D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2529--这组视图可以用来定义编辑图书价格的普通镜头，如下所示。我们定义lkp：X→S，只需丢弃每本书的量场，即lkp（B，v）=（B，fstv）我们通过删除数据库中的所有书籍来定义upd：X×S→X，不在给定视图中，编辑价格并保留数据库和视图中所有书籍的数量，并添加仅在视图中数量为0的所有书籍。详细地说，upd的定义是：upd（（B，v），（BJ，vJ））=（BJ，λb. 如果b∈B则（vJb，snd（v b））else（vJb，0））观察到，对于这个书店数据库，为了满足第三普通透镜定律，传递给upd的视图参数必须包含所有我们想要留下的书数据库更新后。此外，由于我们不能限制哪些书籍可以编辑，我们必须允许镜头能够添加新的书籍到源代码中，具有一些默认数量，这里为0。我们认为，这种被迫的选择是普通镜头的一个真正的缺点，并解决它在本文的其余部分通过发展更新镜头的理论普通镜头：一些替代描述Johnson等人[14]指出，S的透镜范畴与Set/S上下列单子（T1，η1，μ1）的代数范畴相同：T1（X，lkp）=（X×S，snd）η1X，lkpx=（x，lkpx）μ1（（x，s），SJ）=（x，SJ）实际上，（T1，η1，μ1）的代数是Set/S中的映射upd：（X×S，snd）→（X，lkp），即，一个映射upd：X×S→X满足lkp（upd（x，s））=s，它还必须满足（T1，η1，μ1）的代数结构的条件.后者正好等于x=upd（x，lkpx）和upd（upd（x，s），sJ）=upd（x，sJ）。O’ConnorDX=S×（S→X）ε（s，v）=vsδ（s，v）=（s，λsJ. （sJ，v））明确地说，（D，ε，δ）的余代数是集合X和映射作用：X→S×（S→X）满足x=let（s，v）←actxinvs让（s，v）← act x in（s，λsJ. act（v sJ））= let（s，v）← act x in（s，λsJ.（sJ，v））30D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25×J↓↓⊕同构赋予集合X上的透镜结构（lkp，upd）X上的（D，ε，δ）-余代数结构act=。由于Power和Shkaravska4的进一步刻画，仅仅是范畴的等价，而不是同构。S的镜片类别等同于Set。对于一个集合R，我们将由X = S定义的透镜（X，lkp，upd）联系起来R、lkp（s，r）=s，upd（（s，r），SJ）=（SJ，r）。在相反的方向上，透镜（X，lkp，upd）被发送到集合R ={x：X|lkpx = s0}其中s0是S. s 0的选择只造成同构的不同：对于任何s，s：S，函数λx。upd（x，sJ）：{x：X|lkpx = s} → {x：X|lkpx = SJ}是第一和第三透镜条件的同构。(In在S= 0的特殊情况下，我们取R= 0。）直观地说，X被分解成两部分：S，既可以查看也可以更新，R，既不能查看也不能更新。普通镜片的组成与其将S（视图集合）视为固定集合，我们可以让它变化。 然后我们可以定义两个集合X和Y之间的（普通）透镜是满足三个普通透镜定律的一对映射lkp：X→Y和upd：X×Y→X对于任何集合X，都有恒等透镜（id{X}，fst）。给定两个透镜（lkp，upd）：X→Y和（lkpJ，updJ）：Y→Z，我们将它们的组合定义为（lkpJJ，updJJ）：X→Z，其中lkpJJx=lkpJ（lkpx）和updJJ（x，z）=upd（x，updJ（lkpx，z））。它们之间的集合和透镜形成一个类别。3更新镜片在本文中，我们感兴趣的是普通镜头的更细粒度的变化，我们称之为更新镜头。更新镜头：定义我们定义了一个由集合S（视图），（更新）幺半群（P，o，n）和幺半群在集合上的作用（描述对任何给定视图应用任何给定更新的结果）给出的行为5动作（S，（P，o，n），↓）的更新镜头是（源的）集合X，并且映射lkp：X→S（查看源）和upd：X×P→X（更新源）满足条件x=upd（x，o）upd（upd（x，p），pJ）=upd（x，p<$pJ）lkp（upd（x，p））=lkpx↓p4J. Power，O.Shkaravska，Arrays with garbage，Slides from a talk at the Estonian Computer ScienceTheory Days at Viinistu，Oct. 2005，http://cs.ioc.ee/www.example.com~tarmo/tday-viinistu/shkaravska-slides.pdf.在文献中，对（S，）通常被称为a（P，o，）-设置。 我们偶尔会用到这个术语也D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2531也就是说，Xρ JCX×1（X×P）×PX×PX×PUPD XX×ocJUPDX×PX两个更新透镜（X，lkp，upd）之间的映射（X，J，lkp，J，upd，J）是h：X→XJ（源的转换），满足lkpx=lkpJ（h x）h（upd（x，p））=updJ（h x，p）地图也就是说，XlkpJchX JcJlkp′X×Pup dJch×P XJ×PJcup d′S SXhX J为一个动作（S，（P，o，），↓）更新镜头，它们之间的映射形成一个类别Ulen（S，（P，o，n），↓）.运行示例：编辑书店数据库现在我们重新回到第2节中的书店例子。我们首先回想一下，使用普通书店的镜头来编辑特定书籍的价格有些不方便。特别是，我们不能简单地列出我们想要编辑价格的书籍，但也必须列出所有其他书籍。造成这种不便的主要原因是在lkp和upd中都使用了一组视图S。在这里，我们将说明如何将更新与视图解耦，以帮助我们在不同的更新策略中重用同一组视图我们像以前一样保持源集合X、视图集合S和查看地图lkp，但是让（P，o，n），↓，upd根据我们想要对数据库做什么而变化。对于第一个例子，我们重新编辑图书价格，将P设为P=（图书×价格）。任何更新ps：P都将被视为一系列单本书的价格幺半群结构（o，）是自由幺半群的结构（其中o= []且=++），而↓和upd定义如下。（B，v）↓[] =（B，v）（B，v）↓（（b，p）：：ps）=（B，λbJ. 如果bJ= b则p，否则v bJ）↓ psupd（（B，v），[]）=（B，v）upd（（B，v），（b，p）：：ps）= upd（（B，λbJ. if bJ= b then（p，snd（vupd×PαJcX×（ P×P）UPDlkp×PLKPX×XMCJ人民民主联盟X×PXJCJC↓ ¸S× PSJC32D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25bJ））else v bJ），ps）D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2533∗(With这个定义，如果我们要修改的某本书不在数据库中，它将不会被添加到数据库中由于更新镜头带来的额外自由，我们可以同样很好地修改图书价格相对于数据库中的价格。为此，我们可以将P定义为（图书×变化）（让我们同意价格只能是非负数，但变化也可以是负数）。幺半群结构（P，o，n）如上所述，但对↓和upd的定义进行了相应的调整（B，v）↓[] =（B，v）（B，v）↓（（b，c）：：ps）=（B，λbJ. if bJ= b then max（0，v bJ+ c））else vbJ）↓ psupd（（B，v），[]）=（B，v）upd（（B，v），（b，c）：：ps）=upd（（B，λbJ. 如果bJ= b则（max（0，fst（v bJ）+c），snd（v bJ））else v bJ），ps）作为额外的处理，我们还可以使用相同的视图集S来执行书籍的删除和添加。我们选择P为（（书×价格×数量）+书），其中第一个被加数代表增加一本书，第二个被加数代表删除一本书。幺半群结构（P，o，n）又是自由幺半群的结构。（B，v）↓[] =（B，v）（B，v）↓（inl（b，p，q）：：ps）=（B {b}，λbJ. 如果bJ= b则p，否则v bJ）↓ps（B，v）↓（inr b：：ps）=（B\{b}，v|B\{b}）↓psupd（（B，v），[]）=（B，v）upd（（B，v），inl（b，p，q）：：ps）= upd（（B ∈ {b}，λbJ. if bJ= b then（p，q）else v bJ），ps）upd（（B，v），inrb：：ps）= upd（（B\{b}，v|（b）、（ps）当然，如果需要，我们也可以将条目的添加和删除与条目的修改结合起来。请注意，当改变一本书的价格时，或者当添加一本新书时，当负变化的绝对值分别大于书的价格时，我们必须引入额外的默认行为。如果这本书已经在数据库中。这是必要的，因为每次更新都必须始终适用。我们将在第7节中通过引入更新镜头的依赖类型版本来解决这一缺陷。将透镜更新为函子和单子（S，（P，o，n），↓）的透镜范畴允许几种可供选择的特征化。我们现在将依次考虑这些问题。最终的见解是，更新透镜是一个适当的共单的余代数。我们将通过中间特征化的几个小步骤到达那里，这些中间特征化也具有独立的价值。我们只使用关于单子、余单子、分配律、提升、余自由余单子、伴随单子和余单子的标准事实。这些在文献中分散出现，一些参考文献包括[7，5，4，20，21]。34D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25↓我们首先注意到，从集合X到S的映射lkp只不过是由F0X=S定义的函子F0在X上的余代数结构。 （P，o，n）在X上的作用upd恰好是单子（T1，η1，μ1）在X上的代数结构，定义如下：T1X=X×Pη1x=（x，o）μ1（（x，p），pJ）=（x，p<$pJ）最后，（P，o，n）在S上的作用↓：S×P→S恰是函子F0上单子（T1，η1，μ1）的分配律.因此，（S，（P，o，n），↓）的更新透镜（X，lkp，upd）只不过是函子F0和单子（T1，η1，μ1）的↓ 集合X的三元组，映射lkp：X→S与（T1，η1，μ1）的代数结构upd：X×P→X在条件X×PupdXlkpSlkp×PJc公司简介同样，更新透镜映射是双代数映射。因此，更新镜头的类别与（0）函子F0和单子（T1，η1，μ1）的↓-双代数范畴因此，这一类别也可以描述为：（（0让我们拼出（（该↓-提升F0↓F0到（P，o，u）的集合定义为yF0↓（X，u p d）=（S，↓）.F0↓的余代数是因此由一个（P，o，n）-集（X，upd）给出，它有一个从lkp到（S，↓）的映射。 因此，是（P，o，n）-Set/（S，↓）.（0”）：F0的c-代数的范畴是Set / S. f（T1，η1，μ1）的e↓-提升（T1↓，η1↓，μ↓1）定义为：T1↓（X，lkp）=（X × P，λ（x，p）. lkp x ↓ p）（T1↓，η1↓，μ↓1）的代数是Set /S的对象（X，lkp），其映射是（X×P，λ（x，p））的up pd. lkpx↓p）满足单子代数的条件。D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2535将透镜更新为共单子和单子的双代数设（D0，ε0，δ0）是函子F0上的余自由余子，由下式显式给出：D0X=S×Xε0（s，x）=xδ0（s，x）=（s，（s，x））F0的余代数范畴（即，范畴Set/S）同构于（D0，ε0，δ0）的余代数范畴，其对象由集合X和映射dlkp：X→S×X给出，满足dlkp XS×XdlkpXS×XJCSNDdlkpCJc/J·阿夫斯特，同上XS×XS×dlkpS×（S×X）同构将（D0，ε0，δ0）-余代数结构dlkp=dlkp，idlkp：X→S×X赋给集合X上的任何F0-余代数结构lkp：X → S.此外，（T1，η1，μ1）在F0上的分配律↓导出了（T1，η1，μ1）在（D0，ε0，δ0）上的分配律λ，由下式明确给出：λ：（S×X）×P→S×（X×P）λ（（s，x），p）=（s↓p，（x，p））因此，更新透镜范畴，即F0的↓-双代数范畴且（T1，η1，μ1）同构于(1) （D0，ε0，δ0）和（T1，η1，μ1）的λ明确地说，这一范畴的对象是集合X的三元组，（D0，ε0，δ0）-余代数结构dlkp：X→S×X和（T1，η1，μ1）-代数结构upd：X×P→X，满足人民民主联盟X×PXS×Xdlkp×PcJ=lkp，id、S×upd（S×X）×Pλ<$S×（X×P）这一类别也可以描述为：（（T1，η1，μ1）的代数范畴;0 0 0（1（D0，ε0，δ0）的余代数范畴。1 1 1将透镜更新为函子和余子的余代数对我们可以用不同的余单子代替单子（T1，η1，μ1），而不是用余单子代替函子36D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25F0。这就是我们现在要做的D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2537‡‡‡→=‡‡考虑下面的comonad（D1，ε1，δ1）：D1X=P→Xε1v=voδ1v = λp。λpJ.v（p<$pJ）函子D1是函子T1的右伴随.此外，余单子（D1，ε1，δ1）是单子（T1，η 1，μ 1）在[ 7 ]意义下的相应因此，（T1，η1，μ1）的代数范畴同构于（D1，ε1，δ1）的余代数范畴.证明了（D1，ε1，δ1）的余代数是具有映射cup：X→（P→X）满足杯XP→XJco→X杯XP→XJc→X→X杯cJJcP×杯P×P→XCJXP→XP→（P→X）同构将（D1，ε1，δ1）-余代数结构cupd=curupd：X→（P→X）赋予集合X上的（T1，η1，μ1）-代数结构upd：X×P进一步地，（T1，η1，μ1）在F0上的分配律↓导出了F0在（D1，ε1，δ1）上的分配律，即=cur ↓.由此得出F0和（T1，η1，μ1）的↓-双代数范畴同构于(2) F0和（D1，ε1，δ1）的余代数的-匹配对范畴解释一下，这个范畴的对象由集合X，maplkp：X→S和（D1，ε1，δ1）的余代数结构cupd：X→（P→X）满足S，LKP杯XPX库尔乌普德cJP→lkpSP→S这一类别也可以描述为：（将透镜更新为两个余子的余代数对我们现在把前两段的内容结合起来。我们用（D0，ε0，δ0）代替F0，用（D1，ε1，δ1）代替（T1，η1，μ1（T1，η1，μ1）在（D0，ε0，δ0）上的分配律λ和F0在（D1，ε1，δ1）上的分配律都给出了（D0，ε0，δ0）在（D1，ε1，δ1）上的分配律θθ：S×（P→X）→（P→S×X）θ（s，v）= λp。（s ↓ p，v p）138D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25→更新镜头的类别，即，函子的↓-双代数范畴F0和单子（T1，η1，μ1），因此同构于(3)（D0，ε0，δ0）和（D1，ε1，δ1）的余代数的θ-匹配对范畴设X是一个集合，（D0，ε0，δ0）-余代数结构dlkp：X→S×X和（D1，ε1，δ1）-余代数结构cupd：X→（P→X）满足S×XS×cupdcJ，dlkp=lkp，id杯X=curup d X→XPdlkpJCS×（P→X）θ<$P→S×X同一类别也可以描述为（000（D0，ε0，δ0）到（D1，ε1，δ1）的余代数范畴.将透镜更新为comonad的余代数我们有两个余项（D0，ε0，δ0）和（D1，ε1，δ1），前者对后者有一个分配律θ。这给出了相容的复合comonad（D，ε，δ）：DX=（D0·D1）X=S×（P→X）ε（s，v）=voδ（s，v）=（s，λp. （s ↓ p，λpJ.v（p <$pJ）更新镜头的类别，即，（D0，ε0，δ0）和（D1，ε1，δ1）的余代数的θ-匹配对同构于(4) （D，ε，δ）-余代数范畴证明了一个（D，ε，δ）-余代数是一个集合X，其映射作用X→S×（P→X）满足x=let（s，v）←actxinvo让（s，v）←act x in（s，λp. act（v p））= let（s，v）←act x in（s，λp. （s ↓ p，λpJ.v（p <$pJ）也就是说，X法S×（P→X）εCJX行为Jc作用量S×（P→X）cJδS×（P→act）XS×（P→X）<$S×（P→S×（P→X））同构对应于集合Xa（D，ε，δ）上的更新透镜结构（lkp，upd）-余代数结构act=cur lkp，curupd <$.D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2539沿着（0）-（1）-（3）-（4）和（0）-（2）-（3）-（4）两条路线，我们得到了（S，（P，o，n），↓）的最新透镜本质上与余代数相同40D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25（D，ε，δ）。 代数特征（0[14]对于集合S的普通透镜，并且共代数特征（4）与O 'Connor的[ 18 ]类似更新透镜的许多其他替代表征没有普通透镜的对应物。我们没有机会在这里详细讨论这个问题，但是更新（S，（P，o，n），↓）的镜头，即，余单子（D，ε，δ）的余代数，余模相同的（一般大的）Lawvere理论，该理论由我们在别处[3]称为（S，（P，o，δ），↓）的更新单子的代数建模。这个单子（T，η，μ）定义为：T X=S→P×Xηx= λs。 （o，x）μf = λs。let（p，g）<$fsin let（pJ，x）<$g（s↓p）in（p<$pJ，x）更新镜片：等同表征这里有一个不同的刻画，它只是范畴的等价，而不是同构。我们首先观察到，任何行为（S，（P，o，n），↓）定义一个范畴S，（P，o，n），↓ n，其中对象是S的元素s和s，SJ之间的映射：S是P的元素p，使得s↓p=SJ。 s上的恒等式是o，p和pJ的合成是ppJ.范畴Ulens（S，（P，o，），↓）等价于函子范畴[UlensS，（P，o，），↓Ulens，Set]。一 个函子R：R_S，（P，o，n），↓ R_s → Set被映射到由X = R_s：S定义的最新透镜（X，lkp，upd）。Rs，lkp（s，r）= s和upd（（s，r），p）=（s↓p，Rpr）。在相反方向上，更新透镜（X，lkp，upd）被映射到由Rs ={x：X|lkp x = s}，Rp x = upd（x，p）。把普通镜头变成更新镜头给定一个行为（S，（P，o，n），↓），S的任何普通透镜（X，lkp：X→S，upd：X×S→X）通过updJ（x，p）=upd（X，lkpx↓p）定义了（S，（P，o，n），↓）的更新透镜（X，lkp，updJ：X× P→X并且，对于S，两个普通透镜之间的任何映射h也是对于（S，（P，o，n），↓）的相应更新透镜之间的映射。 这就给出了一个从Lens S到Ulens（S，（P，o，），↓）的函子。这个函子是 它定义为τ（s，v）=（s，λp。v（s↓p））。两个余代数之间的任何态射给出了对应余代数范畴之间的4视图转换和更新到目前为止，我们已经看到更新透镜映射h：（X，lkp，upd）→（XJ，lkpJ，updJ）模拟了从源集合X到源集合XJ的转换，对于固定动作（S，（P，o，n），↓）。D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2541（Ⅲ）（Ⅲ）ULensTot=（Ⅲ）尤伦斯JJJJJ菲内斯 一 态射<$t，q）=τ之间 的 科莫纳德 （P，o，n），↓）和在本节中，我们讨论了对于一个固定的源集合X，行为之间的映射如何引起视图集和更新集之间的转换。动作（S，（P，o，n），↓）和（SJ，（PJ，oJ，nJ），↓J）之间的映射（t，q）由函数（视图的转换）t：S→SJ和么半群同态（更新的转换）q：（PJ，OJ，J）→（P，o，j），使得t（s↓q p）=ts↓Jp（注意么半群同态的反向方向在文献中，例如，[17]，通常需要q：（P，o，n）→（PJ，oJ，nJ）和t（s↓p）=ts↓Jq p，但这不是这里所需要的行为构成一个类别行为。我们说，由动作（S，（P，o，n），↓），（SJ，（PJ，oJ，nj），↓J）之间的态射（t，q）引起的视图和更新的转换是函子ULens（t，q）：ULens（S，（P，o，n），↓）→ULens（SJ，（PJ，oJ，nJ），↓J）定义为ULens（t，q）（X，lkp，upd）=（X，t<$lkp，upd <$（X×q））Ulen（t，q）h=h我们注意到Ulen是从Act到CAT的函子。从函子Ulens，我们可以通过使用Grothendieck构造来构建所有更新镜头的总类别UlensTot（参见，例如， [13，§1.10]），即，详细地，ULensTot的对象是动作（S，（P，o，n），↓）以及用于该动作的最新镜头（X，lkp，updUlens（S，（P，o，），↓）的对象。 两个对象（（S，（P，o，n），↓），（X，lkp，upd））和（（SJ，（P J，oJ，nJ），↓J）之间的映射，（XJ，lkpJ，updJ））是一个动作映射（t，q）：（S，（P，o，n），↓）→（SJ，（PJ，oJ，nJ），↓J）配对其中映射h：ULens（t，q）（X，lkp，upd）→（XJ，lkpJ，updJ）为（SJ，（PJ，oJ，J），↓J）的更新透镜。共单余代数到共单余代数映射的视图和更新的转换正如每个动作（S，（P，o，），↓）定义一个共单子S，（P，o，），↓=（D，ε，δ）一样，两个动作（S，（P，o，），↓）和（SJ，（PJ，oJ，J），↓J）之间的每个态射（T，Q）de-S，（P，o，n），↓.明确地说，这种自然转变的定义是：τ：τ {X}。（S×（P→X））→SJ×（PJ→X）τ（s，v）=（t s，v<$q）- 形成从Act到Comonads（Set）的函子。42D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25如前所述，两个余单子（D，ε，δ）和（DJ，εJ，δJ）之间的态射τ确定了对应余代数范畴之间的函子，将（D，ε，δ）-余代数（X，act）发送到（DJ，εJ，δJ）-余代数（X，τ {X}-余act）。D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）2543（2）（Ⅲ）（Ⅲ）而范畴Ulens（S，（P，o，n），↓）同构于Coal- gebras范畴 的 的科莫纳德S，（P，o，），↓，的函子ULens（t，q）：ULens（S，（P，o，n），↓）→ULens（SJ，（PJ，oJ，nJ），↓J）同构于由同单态射t，q导出的Sj，（P，o，n），↓和SJ，（PJ，oJ，nJ），↓j的余代数范畴之间的函子.总而言之，我们有下面的图可以交换到同构：Act<$−）Comonads（Set）科尔格zs，猫5张量更新镜头有时我们可能想将多个更新镜头收集到一个更新镜头结构中。我们展示了如何可以做到这一点与张量积的所有更新镜头的类别。我们将单位行为I定义为行为（1，（1，！，！））。对于任意两个作用（S0，（P0，o0，0），↓0）和（S1，（P1，o1，1），↓1），我们定义它们的张量积为：（S0，（P1，o1，1），↓1）（S1，（P1，o1，1），↓1）=（S0×S1，（P0×P1，o，1），↓）哪里o=（o0，o1）（p0，p1）<$（pJ0，pJ1）=（p0<$0pJ0，p1<$1pJ1）（s0，s1）↓（p0，p1）=（s0↓0p0，s1↓1p1）I和D把Act变成一个monoidal范畴。现在对于行为I，我们有单位透镜J=（1，！）。并且对于两个更新透镜（X0，lkp0，upd0）和 （X1，lkp1，upd1） 为 分别作用于（S0，（P0，o0，0），↓0）（S1，（P1，o1，1），↓1），有张量更新透镜（X0，lkp0，upd0）<$（X1，lkp1，upd1）=（X0×X1，lkp，upd）对于作用（S0，（P0，o0，0），↓0）<$（S1，（P1，o1，1），↓1），lkp（x0，x1）=（lkp0x0，lkp1x1）upd（x0，x1）（p0，p1）=（upd0（x0，p0），upd1（x1，p1））有了这一点，我们已经表明，ULens是一个宽松的monoidal函子从Act到CAT（wrt。Act上的（I，）monoidal结构和CAT上的乘积monoidal结构），其中monoidality见证人是ULens44D. Ahman，T.Uustalu/理论计算机科学电子笔记308（2014）25J：1→UlensI：ULens（S0，（P0，o0，→Ulen（（S0，（P0，o0，0），↓0）（S1，（P1，o1，1），↓1））