Reasoning about effect interaction by fusion
File(s)3473578.pdf (379.86 KB)
Published version
Author(s)
Yang, Zhixuan
Wu, Nicolas
Type
Journal Article
Abstract
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.
Date Issued
2021-08
Date Acceptance
2021-06-19
Citation
Proceedings of the ACM on Programming Languages, 2021, 5, pp.1-29
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
29
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
5
Copyright Statement
© 2021 Copyright held by the owner/author(s).
This work is licensed under a Creative Commons Attribution 4.0 International License.
This work is licensed under a Creative Commons Attribution 4.0 International License.
License URL
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Identifier
https://dl.acm.org/doi/10.1145/3473578
Grant Number
EP/S028129/1
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Haskell
fusion
modular handlers
CPS transformation
HANDLERS
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Haskell
fusion
modular handlers
CPS transformation
HANDLERS
Publication Status
Published
Article Number
73
Date Publish Online
2021-08