TY - JOUR

T1 - Not by equations alone

T2 - Reasoning with extensible effects

AU - Kiselyov, Oleg

AU - Mu, Shin Cheng

AU - Sabry, Amr

N1 - Publisher Copyright:
© The Author(s), 2021. Published by Cambridge University Press

PY - 2021

Y1 - 2021

N2 - The challenge of reasoning about programs with (multiple) effects such as mutation, jumps, or IO dates back to the inception of program semantics in the works of Strachey and Landin. Using monads to represent individual effects and the associated equational laws to reason about them proved exceptionally effective. Even then it is not always clear what laws are to be associated with a monad-for a good reason, as we show for non-determinism. Combining expressions using different effects brings challenges not just for monads, which do not compose, but also for equational reasoning: the interaction of effects may invalidate their individual laws, as well as induce emerging properties that are not apparent in the semantics of individual effects. Overall, the problems are judging the adequacy of a law; determining if or when a law continues to hold upon addition of new effects; and obtaining and easily verifying emergent laws. We present a solution relying on the framework of (algebraic, extensible) effects, which already proved itself for writing programs with multiple effects. Equipped with a fairly conventional denotational semantics, this framework turns useful, as we demonstrate, also for reasoning about and optimizing programs with multiple interacting effects. Unlike the conventional approach, equational laws are not imposed on programs/effect handlers, but induced from them: our starting point hence is a program (model), whose denotational semantics, besides being used directly, suggests and justifies equational laws and clarifies side conditions. The main technical result is the introduction of the notion of equivalence modulo handlers (“modulo observation”) or a particular combination of handlers-and proving it to be a congruence. It is hence usable for reasoning in any context, not just evaluation contexts-provided particular conditions are met. Concretely, we describe several realistic handlers for non-determinism and elucidate their laws (some of which hold in the presence of any other effect). We demonstrate appropriate equational laws of non-determinism in the presence of global state, which have been a challenge to state and prove before.

AB - The challenge of reasoning about programs with (multiple) effects such as mutation, jumps, or IO dates back to the inception of program semantics in the works of Strachey and Landin. Using monads to represent individual effects and the associated equational laws to reason about them proved exceptionally effective. Even then it is not always clear what laws are to be associated with a monad-for a good reason, as we show for non-determinism. Combining expressions using different effects brings challenges not just for monads, which do not compose, but also for equational reasoning: the interaction of effects may invalidate their individual laws, as well as induce emerging properties that are not apparent in the semantics of individual effects. Overall, the problems are judging the adequacy of a law; determining if or when a law continues to hold upon addition of new effects; and obtaining and easily verifying emergent laws. We present a solution relying on the framework of (algebraic, extensible) effects, which already proved itself for writing programs with multiple effects. Equipped with a fairly conventional denotational semantics, this framework turns useful, as we demonstrate, also for reasoning about and optimizing programs with multiple interacting effects. Unlike the conventional approach, equational laws are not imposed on programs/effect handlers, but induced from them: our starting point hence is a program (model), whose denotational semantics, besides being used directly, suggests and justifies equational laws and clarifies side conditions. The main technical result is the introduction of the notion of equivalence modulo handlers (“modulo observation”) or a particular combination of handlers-and proving it to be a congruence. It is hence usable for reasoning in any context, not just evaluation contexts-provided particular conditions are met. Concretely, we describe several realistic handlers for non-determinism and elucidate their laws (some of which hold in the presence of any other effect). We demonstrate appropriate equational laws of non-determinism in the presence of global state, which have been a challenge to state and prove before.

UR - http://www.scopus.com/inward/record.url?scp=85100311056&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85100311056&partnerID=8YFLogxK

U2 - 10.1017/S0956796820000271

DO - 10.1017/S0956796820000271

M3 - Article

AN - SCOPUS:85100311056

JO - Journal of Functional Programming

JF - Journal of Functional Programming

SN - 0956-7968

M1 - e2

ER -