research-article

Open access

Reasoning about effect interaction by fusion

Authors:

Zhixuan Yang,

Nicolas WuAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue ICFP

Article No.: 73, Pages 1 - 29

https://doi.org/10.1145/3473578

Published: 19 August 2021 Publication History

PDF eReader

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.

Supplementary Material

Auxiliary Archive (icfp21main-p61-p-archive.zip)

This contains the appendices to the paper Reasoning about Effect Interaction by Fusion accepted to ICFP 2021. The appendices contain detailed proofs of some of the lemmas and theorems in the paper.

Download
1.42 MB

Auxiliary Presentation Video (icfp21main-p61-p-video.mp4)

This contains the appendices to the paper Reasoning about Effect Interaction by Fusion accepted to ICFP 2021. The appendices contain detailed proofs of some of the lemmas and theorems in the paper.

Download
184.95 MB

MP4 File (3473578.mp4)

Presentation Videos

Download
135.36 MB

References

[1]

Danel Ahman. 2017. Handling Fibred Algebraic Effects. Proc. ACM Program. Lang., 2, POPL (2017), Article 7, Dec., 29 pages. https://doi.org/10.1145/3158095

Abstract

Supplementary Material

References

Cited By

Index Terms

Recommendations

Effect handlers in scope

Effect handlers in scope

An extensible dynamically-typed hierarchy of exceptions

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Funding Sources

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations