有状态计算中的的透镜结构

可在www.sciencedirect.com在线获取理论计算机科学电子笔记319（2015）403-421www.elsevier.com/locate/entcs有效计算的有状态运行程序Tarmo Uustalu1塔林理工大学控制论研究所，Akadeemia tee 21，12618 Tallinn，爱沙尼亚摘要一个集合需要什么样的结构，才能使给定计算概念中的计算以这个集合作为状态集合有状态地运行？对于有状态地运行非确定性计算，需要解析器结构;对于交互式I/O计算，需要“响应者-侦听器”结构;为了能够服务于有状态计算，集合必须携带透镜结构。 我们表明，一般来说，是一个有状态的运行计算的单子对应于一个Lawvere理论（定义为一个集在给定的单子和这个集合的状态单子之间配备有单子态射）与成为理论的共模型相同，即，对应的余单子的余代数。我们得出了一些这种观察的例子，并将跑步者与处理者进行了关键词：事件，单子，Lawvere理论，余模型，状态单子，处理程序1引言本文是关于基于Moggi给定一个单子（T，η，μ），X中一个值的计算是T X的一个元素。计算是用来计算值的，所以我们认为希望提取这些值来运行计算是很自然的。理想情况下，我们可能希望有一个多态函数θ：<$X。T X→X用于从计算中提取值，但这通常要求太多（尽管这是可能的，例如，作者monads）。然而，如果允许我们依赖于某些输入，我们通常可以产生一个值-将其视为从具有适当结构的集合C中例如，如果我们有一个有限的非确定性计算，在这个意义上，一个二进制的良基叶树，一个比特流可以用来识别一个叶子。由于在运行两个计算的序列应该与组成两个运行相同的意义上，运行应该合理地是组合的，因此运行不仅应该是组合的，而且应该是第1tarmo@cs.ioc.eehttp://dx.doi.org/10.1016/j.entcs.2015.12.0241571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。404T. Uustalu/电子笔记理论计算机科学319（2015）403∀→依赖于初始状态，但也返回最终状态（可以作为另一次运行的初始状态）。在不确定性和比特流的情况下，最终状态可以是作为初始状态提供的比特流的剩余部分。所以一般来说，我们可能想寻找一个多态函数θ：X。 T XT C X其中（T C，η C，μ C）是C作为状态集的状态单子。我们想要的复合性意味着θ不仅是一个自然变换，而且是一个单子态射。在本文中，我们回答了一个问题，当一个集合C可以被用来运行计算在一个单子（T，η，μ）状态，假设单子对应于一个Lawvere理论。答案是：C必须携带一个Lawvere理论的共模型（即，对应的comonad的余代数我们拼出了这种普遍性的一些实例，非确定性，交互式I/O和有这是一个简单的练习，但我们发现，结果很有启发性。例如，对于某些版本的非确定性，运行者只能恢复给定计算中的一部分信息;其他版本的非确定性只允许微不足道的运行者，不透露任何关于计算的信息。所以有些变化非决定论本质上比其他的更具操作性运行程序与处理程序有些类似，但一个更大的区别是运行程序在值集上是多态的。例如，处理允许从一个特定值集上的非确定性计算（一个二进制良基叶树）中提取一个值 (If对我们来说，不确定性计算是一个非空的值列表，这个操作必须是关联的。跑步不允许这样的事情。在我们看来，处理程序和运行程序的语用学是不同的：处理程序是一种编程语言构造，而运行程序是编译方案。本文的结构如下。在第二节中，我们回顾了我们需要的关于Lawvere理论、模型和共模型的一些基本事实。在第3节中，我们证明了对应于Lawvere理论的单子的有状态算子是与该理论的余模（对应的余单子的余代数）的双射。我们还比较了这一观察到的一个事实单子态射延续单子不同类型的跑步者。在第四节中，我们给出了非确定性、交互式I/O和有状态计算的实例。在结束之前，在第5节中，我们将跑步者与训练者进行比较。2Lawvere理论、模型、共模型我们首先回顾关于无限Lawvere理论和模型的最基本的定义和事实（对于适当的阐述，请参见，例如，[6]）以及电源可数Lawvere理论和正则基数κ的κ元Lawvere理论的定义类似。Lawvere理论一个（无穷）Lawvere理论是由一个小范畴L和一个函子L：Fop→L给出的，这个函子是对象上的恒等式，并且严格保持Fop的有限积。T. Uustalu/电子笔记理论计算机科学319（2015）403405O（Ⅲ）（Ⅲ）（Ⅲ）（）（）（）（）（）o∈O1，任何运算OP：I→O都可以用O个运算OP：这里F是有限基数范畴，即，这是有限集合范畴的骨架。它是一个严格monoidal范畴wrt。有限余积，实际上它是单对象范畴上的自由的这样的范畴。一个理论可以（非唯一地）通过一个陈述来具体化，即，由L（运算）的映射OPj：Ij→Oj的某个子集，所有其他映射都可以从它定义，以及L（方程）的交换图LHSk=RHSk的某个子集，所有其他交换图都可以从它得出。请注意，我们总是可以只做点I→1的运算作为O=1、0 =0，0=模型o∈OOPo）。（二）理论（L，L）的模型由函子−：L→Set给出，它保持L的有限乘积（非严格）。为了给出（L，L）的模型，它必须指定一个集合，A= 1因为，对于ny个其他对象Y，我们有Y=y∈Y1<$=y∈Y1=1<$Y3连同功能opj= Λ−1OPj：Oj×（1<$Ij）→ 1因为，对于任何其他映射f，f则由函性和有限积的保持唯一确定。此外，任何具有函数op j：O j×（A <$I j）→A的集合A定义一个模型，只要方程lhs k= rhs k对导出函数lhs k，rhs k成立。理论与单子一个理论定义了一个唯一的单子，它的代数本质上与它的模型相同。对应于理论（L，L）的单子是自由单子的商。底层的仿函数是TX=T0X/T0X其中，T0X是由下式归纳定义的集合：X：Xvarx：T0Xo：Oj f：T0XIjopj（o，f）：T0X(so 用更简洁的符号表示，T0X = μZ X + j O j×（Z <$I j））和<$X2我们根据表示的运算来写L的映射，F的映射，L的乘积双函子，我们记为+（sic！）与F的余积和L的合成的符号一致。注意，F的映射在L中的方向是相反的，所以在F中o：1 → O，但在L中o：O → 1，等等。[3]为了避免在例子中显式使用×的对称性，我们将使用两个指数函子<$1和<$2;把− <$Y看作Y×−的右伴随，把Y<$−看作−×Y的右伴随。406T. Uustalu/电子笔记理论计算机科学319（2015）403是T0X上的二元关系，归纳定义为：i：Ii.fiopj（o，f）<$Xopj（o，fJ）lhsk（o，f）<$Xrhsk（o，f）单位η是var，乘法μ递归地定义为μ（vart）=t，μ（opj（o，f））= opj（o，λi. μ（f i））。（T，η，μ）的代数本质上是相同的。模del（A，（o pj：O j×（AIj）→A）j）和代数（A，α：TA→A）通过yα（v arx） =x和α（o pj（o，f））=o pj（o，λi）可互定义递归. α（fi））和byopj（o，f） =α（opj（o，λi. var（f i）。对应于一个理论的单子是无穷的。任何单子都以这种方式对应于至多一个理论科莫德尔斯我们现在准备讨论Power理论（L，L：Fop→L）的一个余模型由一个保持Lop的有限余积的函子−：Lop→Set给出（回想一下，一个模型是来自L的保持其有限积的函子）。为了给出一个共模型，它可以指定一个集合，C=1000000因为X=x∈X1=x∈X1=1×X，连同函数opj=OPj：1×Oj→1×Ij其中我们经常将opj拆分为n_opnj，opsj_op（其中n和s是“next”和“show”的助记符）。同样，任何具有函数opj：C×O j→C×I j的集合C定义一个余模，条件是方程lhs k= rhs k对导出函数lhs k，rhs k成立。理论与共同体除了定义一个代数与模型相同的（无穷的）单子之外，一个理论还定义一个具有如下性质的共单子：该理论的余模型与该共单子的余代数相同。对应于理论（L，L）的余单子是余自由余单子的子余单子。底层函子定义为：DX = D0X|OKX其中D0X是一个余感定义为4的d：D0Xvard：Xd：D0X o：Ojopnj（d，o）：D0Xd：D0X o：Ojopsj（d，o）：Ij[4]我们以基于析构函数的方式编写共归纳定义（与证明助手中常用的基于构造函数的风格相反），因为这更流畅。T. Uustalu/电子笔记理论计算机科学319（2015）403407（因此，用一个更紧凑的符号表示，D0X=νZ。X×j（Oj<$Z×Ij））和okX是D0X上的谓词，共归纳地定义为okX dokX（opnj（d，o））okX dlhsnk（d，o）=rhsnk（d，o）okX dlhssk（d，o）=rhssk（d，o）计数ε是var。余乘δ的上递归定义为var（δ d）=d，opnj（δ d，o）= δ（opnj（d，o）），opsj（δ d，o）= opsj（d，o）。一个余模（C ，opj：C × O j→ C × I j） j）与一个余代数（C，γ：C→DC）可共递归地互定义为var（γ c）= c，opnj（γ c，o）= γ（opnj（c，o）），opsj（γ c，o）= opsj（c，o），以及opnj（c，o）= var（opnj（γc，o）），opsj（c，o）= opsj（γ c，o）。与上述形式的理论相对应的comonad一般是非无穷的。此外，一个comonad可以对应许多理论。(E.g.、所有具有至少一个零元运算（OP：0→O，O/= 0）的理论都有初始comonad（DX= 0）作为相应的comonad。3有状态的跑步者= comodels我们准备证明本文所围绕的定理。我们证明了一个有状态的runner和一个comodel是一样的命题3.1给定一个Lawvere理论（L，L），设（T，η，μ）是对应于该理论的单子。给定一个集合C，设（TC，η C，μ C）是C的状态单子。在从（T，η，μ）到（TC，ηC，μ C）的单子态射和C上的余模之间存在双射（即， （D，ε，δ）对应于（L，L）的余代数。证据令Lawvere理论（L，L）由运算OPj：Ij→Oj和方程LHSk=RHSk给出.相应的单子（T，η，μ）然后如前一节所述构造。给定一个余模（opj：C × O j→ C × Ij）j，给出单子态射θ：<$X. T X →（C×X）C由t上的递归定义：T0X，θ X（var x）= λc。 （c，x）θ X（opj（o，f））= λc. θ X（f（opsj（c，o））（opnj（c，o））为了使这个定义合法，θX必须将T0X中与θ X相关的计算发送到TC X中的相等计算。这是通过归纳证明的证明t<$XtJ从lhsnk=rhsnk和lhssk=rhssk。单子态射的单位保持律平凡地成立。乘法保持律是一个“替换引理”，它是在t：T0（T0X）.在相反的方向上，给定一个单子态射θ，我们定义余模（opj）j为：o pj（c，o）=θIj（opj（o，λi. vari）c408T. Uustalu/电子笔记理论计算机科学319（2015）403等式lhsnk=rhsnk和lhssk=rhssk遵循θX在T0X中发送与θ X相关的计算到TC X中的相等计算。从一个余模到一个单子态射再返回的往返是直接的-恒等式。另一个往返是由于θ的自然性而产生的恒等式。Q我们将此定理与以下众所周知的定理进行比较（参见，例如，[5]关于连续运行。命题3.2给定一个单子（T，η，μ）和一个集合A。设（TA，η A，μ A）是A的连续单子. 从（T，η，μ）到（TA，η A，μ A）的单子态射θ是A上具有（T，η，μ）-代数结构α的双射.证据 给定一个代数结构α：TA → A，单子态射θ：<$X. T X →（A<$X）<$A定义为θ X t = λf。α（T f t）;单子态射的定律遵循代数的定律。在相反的方向上，给定一个单子态射θ，对应的代数结构α定义为αt=θA tidA;代数的定律遵循单子态射的定律。从一个代数到一个单子态射再返回的往返是直接的恒等式.另一个往返是恒等式的证明依赖于θ的自然性。Q请注意，在第一个定理中，我们用一个Lawvere理论来联系一个单子和一个共单子（然而Lawvere理论是由单子决定的）。第二个定理可以在不涉及Lawvere理论的情况下陈述一个更重要的区别是。给定任何单子，对于任何值集X，我们可以找到一个具有延续（A，θ）的游程，使得θX是单子的，即，在给定的单子中，关于给定值集X上的计算的所有它在延续单子中的对应物。实际上，对于任何X，调用自由代数（TX，μX），我们有θX t ηX=t。在有状态运行的情况下，要实现θX是单声道的要困难得多。正如我们很快将看到的，很容易构造这样的例子，其中没有状态集C足以恢复给定值集X上的计算。这两个定理都可以加强到范畴的同构;我们在这里跳过细节4实例4.1非决定论让我们看看上面的命题在各种有限非决定论单子以及非决定论单子的例子中的作用。T. Uustalu/电子笔记理论计算机科学319（2015）403409、ch¸一σ一加一1有限非决定论首先，我们考虑由下面的运算和下面的一些方程给出的理论一加一ch（c）（1 +1）+1ch+11+（1 +1）1+ch1+1ch（d）1+ 1σ+一加一ch（e）1中国1+1ch1Ccchcz1c1C每个这样的理论的模型由一个集合A给出，该集合A具有以下函数并满足以下方程中的正确方程A×A（c）（A×A）×A <$A×（A×A）A×ch<$A×A(d) A×Aσ×A ×A(e) 一ΔΔA×Achch×Acch奇奇CAA×A曲克ZC C我们看到，这些理论的模型正是我们所期望的：没有任何方程，我们得到岩浆，与（c）半群，与（c），（d）交换半群，与（c），（d），（e）半格，与（d）单独交换岩浆。相应的单子是二元叶树单子（游离岩浆，TX=μZ. X + Z×Z），非空列表（自由半群），非空有限多集（自由交换半群），非空有限集（自由半格），二元无序叶树（自由交换岩浆）。他们都是第一个单子的继承者。它们都在一定的粒度水平上对非决定论进行建模;使用哪个单子取决于我们到底想跟踪什么作为非决定论的结果（实际上也取决于我们是否想能够解决非决定论，我们很快就会看到）。这些单子的理论观点告诉我们，单个操作ch对于编程有限不确定函数是完全的。共模型（非确定性计算的运行器）是一个集合C，其函数满足下列方程：C+、Cch（c）（C+C）+C，C+（C+C）、ch+CC+chC+、Cch+的(d) C+C，C+、Cch(e) C， C+、CchCC+C，chCC C最小化地重新表述，一个余模型是一个集合C，函数ch=CHCHN，CHSCHN：C→C×2满足适当的方程。对于没有方程的理论，它只不过是一个最精细的非确定性概念的解析器（调度器），它记住了二元选择的顺序，二元选择中的选项顺序等。给定一个不确定的计算，在这种情况下是二进制叶子标记树，它可以选择一条从根到某个叶子的路径等式（e）迫使chn x=x。等式（c）要求chs（chn x）=chs x和chn（chn x）=chn x，当chn是恒等式时，它们是平凡的。因此，非确定性版本的重新求解器，其中二元选择的顺序被认为是无关紧要的，并且两个相等选项之间的二元选择被认为与根本没有选择相同（因此计算是非空的无平方值列表，即，列出chch一一410T. Uustalu/电子笔记理论计算机科学319（2015）403∼∼∼¸Cz这是一个总是在不改变状态的情况下做出选择的机器，因此，给定一个叶树（与其他叶子树一起标识为同一个非空列表），它从根向下走，总是向左或总是向右，最终到达最左边或最右边的叶子（列表的第一个或最后一个位置）。请注意，其他叶子（列表的内部位置）对于runner来说是不可访问的-它们不是足够“可访问”的。5在包含方程（d）的任何理论的余模型中，必须不是（chs x）=chsx，当C =0时，这是一个问题，就像秩序一样，选择中的选项被认为是无关紧要的，解决非决定论是不可能的，除了无趣的退化情况。无方程理论的共同点是状态流和比特流，D X=νZ 。 X× （ 2×Z ） 。 对 于 一 个 或 多 个 特 定 理 论 的 comonads 是 sub bcomonads。特别地，只包含（c）的理论的共名为DX = X×（2 ×X），包含（c）和（e）的理论的共名为DX = X×2。包含（d）的理论的comonads有DX = 0。失效有限不确定性让我们考虑用下面的运算和可能的下面的等式来扩展所考虑的理论0死1C（a）0 + 1死亡+11+c1CH1（b）第（1）款1+模具1 + 0 1 + 1CH1C现在，模型是支持满足以下方程的以下函数的集合A：1死C(a)1 ×A模具×A切(b) A×1A×dieA ×AchzCAA×A A AA模型有尖岩浆、幺半群、带底交换半格、交换尖岩浆。单子是零-二元叶单子树（游离岩浆，TX_（？）X+1 +Z×Z）及其区别-列表的单子（自由幺半群），有限多集（自由交换幺半群），有限集（有底的自由交换半格），零-二元无序叶树（自由尖交换岩浆）。它们都是非决定主义概念的典范，其中也一个余模型是一个集合C，其函数满足以下期望的函数：5T3的这两个元素相等：t0=ch（ch（var0，var 1），var2）和t1=ch（var0，ch（var1，var 2））。但t0=μt′0且t1=μ t′1对于t′0=ch（var（ch（var 0，var 1）），var（var 2））和t′1=T（T3）中的ch（var（var0），var（ch（var1，var2）。t′0和t′1都是ch（var（.. . ），var（.. . ））.一个能够从t 0中提取值1的运行者，必须首先向左处理t′0，但随后它必须对t′1做 同 样 的 事 情 ，在这种情况下，它不能从t 1中提取值1，它等于t0。T. Uustalu/电子笔记理论计算机科学319（2015）403411O以下等式：0（a）0 +C（b）第（1）款C，+dieC+C、、、C+0，，死C模具+C chC+C，chCC这是直接的，没有有趣的余模型：即使在没有方程的情况下，余模型的载体也必须是空的所有的comonads都是恒定的0（D Xλ=0）。这是不可能的（除了一个统一的退化情况不可能的初始状态）来解决可能失败的不确定性计算。观察到，同样的情况发生在任何理论与一个或多个零操作-迭代（OP：0→O，其中OT0/ = 0。偏袒0）或，在单子方面，与任何单子这样最后，我们也可以跳过CH，考虑只有模而没有方程的理论这个理论的模型是点集。单子是集合的可能单子有一个附加的点，自由点集，TX=1+X），通常用于建模。 我们了解到一个并不令人惊讶的事实，即死亡是唯一需要的操作用于编程部分函数。我们已经知道没有有趣的共模型。4.2交互式输入/输出我们继续考虑其他类型的例子。 开始时，拿两套，O，并考虑非常简单的理论，其中有以下两个操作，没有方程：I1得到安置1cc一个模型是一个集合A，AI得到C一放CAAO单子是自由单子，定义为T X = μZ。X+（Z<$I）+O×Z。我们认识到，在它的单子交互式输入/输出与I和O的输入和输出字母。一个余模型是一个具有两个函数的集合CC×，I得到CC，放C×O它是交互式输入/输出的运行器，一台可以提供输入和消费输出的机器，改变其状态。共分子是共自由共分子，定义为DX= νZ。X×（Z×I）×（O<$Z）。412T. Uustalu/电子笔记理论计算机科学319（2015）403、一一、、 、只有交互输入的情况被O= 0的特殊情况所覆盖，在这种情况下，我们也可以放弃put操作，因为它是强制的，并且没有信息。允许交互式输出仅对应于删除GET操作。这与I= 0的情况不同（从空字母表输入，导致），以及从情况I= 1（输入从单例字母表）。 但是通过P=O（O上的自由幺半群），它是下一节考虑的写的一个实例。4.3状态计算我们继续进行状态计算。我们首先看只读和只写，然后继续读和写（由状态单子建模）。我们通过分析阅读和一般更新（由我们称之为更新单子的模型）来完成。阅读我们从阅读开始取一组S（状态）。我们来看看这个理论：S1！公司简介S×SΔSLKP1CLKP1CLKP×S1LKPCSLKP 101c×S模型是一个集合A，一个人LKPA1A！阿贾克斯LKPAS×SAΔASLKPAczcC（AS）SlkpSAS李鹏通过一般构造，该理论的单子由TX=T0X/T0X，其中T0X和T 0X通过电感定义X：Xvarx：T0X（所以T0X = μ Z。X+（Z<$S））和f：T0XXSlkpf：T0X一群人。f sXf ′slkpf <$Xlkp f ′c <$Xlkp（λs. c）lkp（λs′. lkp（λs. f s s′））<$Xlkp（λs. （f s s）很容易证明TX中的每个元素都可以用规范形式lkp（λs）表示。 var（f s））对于唯一的f：X ∈ S。 由此可见，单子也可以不加限制地定义为T X = X<$S和ηx= λs。x，μf = λs。fs s。这是S作为状态集的reader monad一个共模型是一个集合C，C×SLKPC×1，C×！C×SLKPC×（S×S），C×ΔC×，SLKPC C（C×S）×S，lkp×SC×S，lkp CT. Uustalu/电子笔记理论计算机科学319（2015）403413CUP一CUPAP×PC或者等同地，C，S，C，C，，lkpnS，，LKPSLKPNCLKPSCCLKPNLKPNC，lkpnCLKPSC，lkpnC在后一描述中，第一等式明确地要求lkpn=idC，使得lkpn是多余的，第二个和第三个是多余的，所以我们只剩下一个函数lkps：C→S，没有方程。 因此，用于读取的跑步机相当于一台机器，很乐意用外部状态（从集合S中提取）来服务查找请求，然后在相同的内部状态（从集合C中提取）中继续-因此下次它将再次提供相同的外部状态。由此可见，comonad可以定义为DX=X×S和ε（x，s）=x，δ（x，s）=（（x，s），s）.这是常数S函子上的余自由余子。写作为了写作，我们取一个（更新的）幺半群（P，o，），并考虑以下理论：1 1 向上D 1updupp 1UPduppUPDC人民民主联盟CCUPD×PcP1P1×P这个理论的一个模型是一个集合A，一UPD一个cUPD一AzAoA101UPD一UPDAcupdP（AA一个布拉奇或者，可选择地，以未加咖喱的形式，P×AUPD1×Ao×AP×AUPD（P×P）×A×AP×AUPDcvcCP×（P×A）P×updP×A民主 进步联盟这正是（P，o，n）的左作用的含义。一般的构造告诉我们，相应的单子由下式给出：TX=T0X/ΔX其中T0X和ΔX由yX：Xvarx：T0X(soT0X = μZ。X + P×Z）和p：Pc：T0Xupd（p，c）：T0XcXc′upd（p，c）<$Xupd（p，c′） cXupd（o，c） upd（p，upd（p′，c））<$Xupd（p<$p′，c）一P）PARP一414T. Uustalu/电子笔记理论计算机科学319（2015）403我们可以看到，对于唯一的对（p，x）：P×X，T X的每个元素都可以转换为upd（p，varx）的形式。因此，单子也可以被定义为T. Uustalu/电子笔记理论计算机科学319（2015）403415S1S×S1×SS×S一公司简介公司简介由TX=P×X和ηx=（o，x），μ（p，（pJ，x））=（p<$pJ，x）.这是我们熟悉的（P，o，n）的作者单子，作为更新的幺半群。写作理论的一个commodel（写作计算的一个runner）是一个集合，C与C C，updC×P C，UPDC×P、、UPDC×oUPDC× CC×PC×1C×P，upd×P（C×P）×P，C×（P×P）也就是说，么半群的右作用我们把它看作是一台机器，它监听更新并改变它的状态。comonad的构造是取DX = D0X|其中D0X和ok X共归纳地定义为c：D0Xvarc：Xc：D0Xp：Pupd（c，p）：D0X(soD0X = νZ X×（P<$Z））和okXcokX（upd（c，p））okXcc=upd（c，o）okXcupd（upd（c，p），p′）=upd（c，p<$p′）这里的情况是，关于DX的元素[ ]可以学习的所有内容（即，D 0 X的ok元素）被概括在函数λp中。 var（upd（[]，p））：PX. 这是观察DX的元素的一种普遍方法，因为对于任何集合Y，任何函数f：DX→Y都可表示为λc。g（λp. var（upd（c，p），对于唯一g：（P<$X）→Y.因此，comonad更简洁地定义为DX = P <$X，εv =vo，δv = λp。λpJ.v（p<$pJ）.阅读与阅读我们现在可以继续阅读并进入状态。给定一个状态集S，读和写的理论由两个运算LKP和UPDS11 upd1updSSLKP-1UPDLKP1CUPDCSLKP1CUPD c×sndUPD×ScΔcUPD×S模型是具有函数lkp和upd的集合A，使得一个人LKP一UPD一u pd 阿贾克斯LKPUPD一UPD阿贾克斯ACc一一个人cAcupdS（A布拉奇、SS）S416T. Uustalu/电子笔记理论计算机科学319（2015）403 、ASlkpAupASupdAΔ（AS）S公司简介T. Uustalu/电子笔记理论计算机科学319（2015）403417、一、、或者，可选择地，以未加咖喱的形式，一个人LKPS×AUPD（S×A）SupdSASLKP（S×S）×A和×AS×AUPDCcAACAS× C（S×A）S×updS×A民主进步联盟S×（A<$S）S×lkp<$S×Aupd<$AΔ×（AS）cupd（S×S）×（A<$S）<$S×（S×（A<$S）） <$S×A相应的单子是TX=T0X/X，其中T0X和X由下式归纳定义：X：Xvarx：T0Xf：T0XXSlkpf：T0Xs：S c：T0Xupd（s，c）：T0X(soT0X = μZ。X+（Z<$S）+S×Z），一群人。fsXf ′slkpfX lkpf′cXc′upd（s，c）Xupd（s，c′）c<$Xlkp（λs. upd（s，c））upd（s，upd（s′，c））<$Xupd（s′，c）upd（s，lkp f）<$Xupd（s，fs）由于TX中的每个元素都可以唯一地表示为正规形，lkp（λs. u pd（gs，v ar（hs）），对于某些g，h∈：（S×X）<$S，我们有tTX<$=（S×X）<$S，其中ηx = λs. （s，x），μf = λs. let（sJ，g）←fsing sJ-状态monad为S.一个余模型是一个集合C连同函数lkp和upd，使得公司简介C，updC×S C，UPDC×S、、LKPUPDLKPUPDC×sndC C×SCC×S，upd×S（C×S）×S，C×（S×S）C×S，lkpupd×SC，updC×SC×Δ（C×S）×S，C×或者，拆分lkp=lkpn，lkps，C（S×S）C SCC，updC×S C，UPDC×S、、、、 、、LKPNLKPSUPD（立法局议员、立法局议员）UPDC×snd公司简介CC×S，upd×S（C×S）×S，C×（S×S）一418T. Uustalu/电子笔记理论计算机科学319（2015）403、、C，lkpnC，updUPDC×SS，lkpsC，updsndC×S这里，第一和第三等式一起给出lkpn=idC，使得lkpn冗余。第一个方程于是简化为upd_id_C，lkps_id=id_C，第三个方程变成重言式。我们看到有状态计算的运行者是一台机器T. Uustalu/电子笔记理论计算机科学319（2015）403419×⇒9、一一∼×响应查找（不改变其状态）并监听重写。[6]这种结构在双向变换[4]中被称为C和S之间的透镜7。8公式为DX = D0X|ok X其中D0X和ok X合归纳定义为c：D0Xvarc：Xc：D0Xlkpsc：Sc：D0X s：Supd（c，s）：D0X(soD0X = νZ X×S×（S<$Z））和okXcokX（upd（c，s））okXcc=upd（c，lkpsc）okXcupd（upd（c，s），s′）=upd（c，s′）okXclkps（upd（c，s））=s关于DX的元素[ ]的所有已知信息都可以总结为普适观测（lkps []，λs。 var（upd（[]，s））：S ×（S <$X）. 因此，comonad也可以定义为DX = S（SX）和ε（s，v）= vs和δ（s，v）=（s，λsJ. （sJ，v））。这个comonad被称为costate（或数组）comonad [13，9]。阅读和一般写作让我们也考虑一下阅读和一般写作（而不仅仅是写作）的结合。给定一个（状态）集合S，一个（更新）幺半群（P，o，n）和一个右动作↓：S×P→S（描述状态更新的应用），我们对以下运算和方程给出S1！公司简介S×SΔSLKP1CLKP1CLKP×S1LKPcSLKP 101c1 1 向上DCUP×S1UPdPUPDC人民民主联盟CcUPD×PcP1P1×PP×PSLKP1上dP1×PCLKP×P1×SUPD×SP×S（snd，↓S×P一个具有函数lkp和upd的集合A的模型，使得一个人LKPA1A！阿贾克斯LKPAS×SAΔSALKPAczcC（AS）SlkpSAS李鹏6.计算的状态集为S;运行者的状态集为C。最后的共模型有C=S，lkps=idS和upd=snd，但它不是唯一的共模型。 然而，对于任何共模型，C=SC′，对于某个集合C′。跑者状态的C′投影不能被查找，不能被计算覆盖。[7]更准确地说，双向变换项应该是8在这种情况下，S称为视图状态集，C称为源状态集。420T. Uustalu/电子笔记理论计算机科学319（2015）4039这不是最简单的介绍，而是最简单的介绍。最小的一个有相同的操作，但三个（更多涉及）方程。T. Uustalu/电子笔记理论计算机科学319（2015）403421⇐、S∼、、 、、、CUPCUPAP×PA Au pd AUPD一个cAOzCA101UPD一cupdP（A一个布 拉奇ASlkpAupAPupdlkp（AP）SAP×A（snd，↓AS×P其中UPD和涉及它的方程也可以写成未加括号的形式。单子是TX=T0X/X，其中T0X和X由yX：Xvarx：T0Xf：T0XXSlkpf：T0Xp：Pc：T0Xupd（p，c）：T0X（所以T0X = μ Z。X+（Z<$S） +P×Z）和d一群人。fsXf ′slkpfX lkpf′cXc′upd（p，c）<$Xupd（p，c′）c <$Xlkp（λs. c）lkp（λs′. lkp（λs. f s s′））<$Xlkp（λs. （f s s）c<$Xupd（o，c）upd（p，upd（p′，c））<$Xupd（p <$p′，c）upd（p，lkp f）<$Xlkp（λs. upd（p，f（s ↓ p）由于这些方程允许我们以规范形式lkp（λs）唯一地表示TX中的任何元素。upd（gs，var（hs），对于某些g，h∈：（P×X）<$S，我们得到TX=（P×X）<$S，其中η Xx = λs。 （o，x）μ Xf = λs。 令（p，g）<$fs;（p′，x）<$g（s ↓p）在（p <$p′，x）中我们称这个单子为S，（P，o，n），↓[2]的更新单子更新单子正是读者单子和作者单子的相容组合它们之间的分配律是右作用的双射余模型是具有函数lkp和upd的集合C，使得C×SLKPC×1，C×！S×CLKPC×（S×S），C×ΔC×SLKPC C（C×S）×S，lkp×SC×S，lkp CC C，updC×P C，UPDC×P、、UPDC×oUPDC× CC×PC×1C×P，upd×P（C×P）×P，C×（P×P）C×S，upd×SLKPCUPDC×Plkp×P（C×P）×S，C×（P×S），（snd，↓C×（S×P），（C×cPS）×分解lkp=lkpn，lkps，我们看到第一个方程只是说lkpn=idC，使lkpn冗余。这使得第二个方程重言式，并简化了第五个方程，S，lkpsC，u pdP）PARP、422T. Uustalu/电子笔记理论计算机科学319（2015）403C×Plkps×PS，↓CS×P