Imperial College London
Portrait Picture

DrNicolasWu

Faculty of Engineering, Department of Computing

Reader in Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8189n.wu Website

 
 
//

Location

 

374Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Yang:2021:10.1145/3473578,
author = {Yang, Z and Wu, N},
doi = {10.1145/3473578},
journal = {Proceedings of the ACM on Programming Languages},
pages = {1--29},
title = {Reasoning about effect interaction by fusion},
url = {http://dx.doi.org/10.1145/3473578},
volume = {5},
year = {2021}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - Effect handlers can be composed by applying them sequentially, each handling some operations and leaving other operations uninterpreted in the syntax tree. However, the semantics of composed handlers can be subtle—it is well known that different orders of composing handlers can lead to drastically different semantics. Determining the correct order of composition is a non-trivial task. To alleviate this problem, this paper presents a systematic way of deriving sufficient conditions on handlers for their composite to correctly handle combinations, such as the sum and the tensor, of the effect theories separately handled. These conditions are solely characterised by the clauses for relevant operations of the handlers, and are derived by fusing two handlers into one using a form of fold/build fusion and continuation-passing style transformation. As case studies, the technique is applied to commutative and distributive interaction of handlers to obtain a series of results about the interaction of common handlers: (a) equations respected by each handler are preserved after handler composition; (b) handling mutable state before any handler gives rise to a semantics in which state operations are commutative with any operations from the latter handler; (c) handling the writer effect and mutable state in either order gives rise to a correct handler of the commutative combination of these two theories.
AU  - Yang,Z
AU  - Wu,N
DO  - 10.1145/3473578
EP  - 29
PY  - 2021///
SN  - 2475-1421
SP  - 1
TI  - Reasoning about effect interaction by fusion
T2  - Proceedings of the ACM on Programming Languages
UR  - http://dx.doi.org/10.1145/3473578
UR  - https://dl.acm.org/doi/10.1145/3473578
UR  - http://hdl.handle.net/10044/1/90698
VL  - 5
ER  -
Download