Tue 24 Aug 2021 07:30 - 07:45 at ICFP Talks - Session 2
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.
Mon 23 AugDisplayed time zone: Seoul change
19:00 - 20:45 | Session 2Research Papers at ICFP Talks +12h
| ||
19:00 15mTalk | Contextual Modal Types for Algebraic Effects and Handlers Research Papers DOI Media Attached | ||
19:15 15mTalk | Calculating Dependently-Typed Compilers (Functional Pearl) Research Papers DOI Media Attached | ||
19:30 15mTalk | Reasoning about Effect Interaction by Fusion Research Papers DOI Pre-print Media Attached | ||
19:45 15mTalk | Compositional Optimizations for CertiCoq Research Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI Media Attached | ||
20:00 15mTalk | Generalized Evidence Passing for Effect Handlers Research Papers DOI Media Attached | ||
20:15 15mTalk | Deriving Efficient Program Transformations from Rewrite Rules Research Papers DOI Media Attached | ||
20:30 15mTalk | Algebras for Weighted Search Research Papers DOI Media Attached |
Tue 24 AugDisplayed time zone: Seoul change
07:00 - 08:45 | |||
07:00 15mTalk | Contextual Modal Types for Algebraic Effects and Handlers Research Papers DOI Media Attached | ||
07:15 15mTalk | Calculating Dependently-Typed Compilers (Functional Pearl) Research Papers DOI Media Attached | ||
07:30 15mTalk | Reasoning about Effect Interaction by Fusion Research Papers DOI Pre-print Media Attached | ||
07:45 15mTalk | Compositional Optimizations for CertiCoq Research Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI Media Attached | ||
08:00 15mTalk | Generalized Evidence Passing for Effect Handlers Research Papers DOI Media Attached | ||
08:15 15mTalk | Deriving Efficient Program Transformations from Rewrite Rules Research Papers DOI Media Attached | ||
08:30 15mTalk | Algebras for Weighted Search Research Papers DOI Media Attached |