Combining effects: Sum and tensor

被引:115
作者
Hyland, Martin
Plotkin, Gordon
Power, John
机构
[1] Univ Edinburgh, Sch Informat, Lab Fdn Comp Sci, Edinburgh EH9 3JZ, Midlothian, Scotland
[2] Univ Cambridge, Dept Math, Cambridge CB3 0WB, England
基金
英国工程与自然科学研究理事会;
关键词
computational effect; Lawvere theory; modularity; monad;
D O I
10.1016/j.tcs.2006.03.013
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We seek a unified account of modularity for computational effects. We begin by reformulating Moggi's monadic paradigm for modelling computational effects using the notion of enriched Lawvere theory, together with its relationship with strong monads; this emphasises the importance of the operations that produce the effects. Effects qua theories are then combined by appropriate bifunctors on the category of theories. We give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer and an interactive input/output monad transformer. We further give a theory of the commutative combination of effects, their tensor, which yields Moggi's side-effects monad transformer. Finally, we give a theory of operation transformers, for redefining operations when adding new effects; we derive explicit forms for the operation transformers associated to the above monad transformers. (C) 2006 Elsevier B.V. All rights reserved.
引用
收藏
页码:70 / 99
页数:30
相关论文
共 58 条
[21]  
Kelly G. I., 1980, Bull. Austral. Math. Soc., V22, P1
[22]  
Kelly G.M., 1982, Cah. Topol. Geom. Differ. Categ., V23, P3
[23]   ADJUNCTIONS WHOSE COUNITS ARE COEQUALIZERS, AND PRESENTATIONS OF FINITARY ENRICHED MONADS [J].
KELLY, GM ;
POWER, AJ .
JOURNAL OF PURE AND APPLIED ALGEBRA, 1993, 89 (1-2) :163-179
[24]  
Kelly GM., 1982, Basic concepts of enriched category theory
[25]  
King D., 1992, Proceedings. Pacific Telecommunications Council Fourteenth Annual Conference. PTC '92, P134
[26]   Sketches [J].
Kinoshita, Y ;
Power, J ;
Takeyama, M .
JOURNAL OF PURE AND APPLIED ALGEBRA, 1999, 143 (1-3) :275-291
[27]   MONADS ON SYMMETRIC MONOIDAL CLOSED CATEGORIES [J].
KOCK, A .
ARCHIV DER MATHEMATIK, 1970, 21 (01) :1-&
[28]   CONCURRENT PROCESSES AND THEIR SYNTAX [J].
MILNE, G ;
MILNER, R .
JOURNAL OF THE ACM, 1979, 26 (02) :302-321
[29]  
Milner R., 1989, Communication and concurrency
[30]  
Mislove M., 2000, LECT NOTES COMPUTER, V1877, P350, DOI DOI 10.1007/3-540-44618-4