On The Expressive Power Of User-Defined Effects

1m ago
5 Views
0 Downloads
897.32 KB
26 Pages
Transcription

On the Expressive Power of User-Defined Effects:Effect Handlers, Monadic Reflection, Delimited ControlYANNICK FORSTER, Saarland University and University of CambridgeOHAD KAMMAR, University of Oxford and University of CambridgeSAM LINDLEY, University of EdinburghMATIJA PRETNAR, University of LjubljanaWe compare the expressive power of three programming abstractions for user-defined computational effects: Bauerand Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control without answer-type-modification. Thiscomparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstratesthe sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.We present three calculi, one per abstraction, extending Levy’s call-by-push-value. For each calculus, we present syntax,operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoreticdenotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable,soundness and adequacy. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro-expresseach other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semanticsfor the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either bymonadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.1INTRODUCTIONHow should we compare abstractions for user-defined effects?The use of computational effects, such as file, terminal, and network I/O, random-number generation, andmemory allocation and mutation, is controversial in functional programming. While languages like Scheme andML allow these effects to occur everywhere, pure languages like Haskell restrict the use of effects. A main trade-offwhen incorporating computational effects into the language is giving up some of the most basic properties of thelambda calculus, like β-equality, referential transparency, and confluence. The loss of these properties may leadto unpredictable behaviour in lazy languages like Haskell, or limit the applicability of correctness preservingtransformations like common subexpression elimination or code motion.Monads (Moggi 1989; Spivey 1990; Wadler 1990) are the established abstraction for incorporating effects intopure languages. The introduction of monads into Haskell led to their additional use as a programming abstraction,allowing new effects to be declared and used as if they were native. Examples include parsing (Hutton and Meijer1998), backtracking and constraint solving (Schrijvers et al. 2013), and mechanised reasoning (Ziliani et al. 2015;Bulwahn et al. 2008). Libraries now exist for monadic programming even in impure languages such as OCaml1 ,Scheme2 , and C (Sinkovics and Porkoláb 2013).Bauer and Pretnar (2015) propose the use of algebraic effects and handlers to structure programs with userdefined effects. In this approach, the programmer first declares algebraic operations as the syntactic constructsshe will use to cause the effects, in analogy with declaring new exceptions. Then, she defines effect handlers thatdescribe how to handle these operations, in analogy with exception handlers. While exceptions immediatelytransfer control to the enclosing handler without resumption, a computation may continue in the same position1 http://www.cas.mcmaster.ca/ carette/pa monad/2 aft, February 2017

Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnarfollowing an effect operation. In order to support resumption, an effect handler has access to the continuation atthe point of effect invocation. Thus algebraic effects and handlers provide a form of delimited control.Delimited control operators have long been used to encode effects (Danvy 2006) and algorithms with sophisticated control flow (Felleisen et al. 1988). There are many variants of such control operators, and theirinter-relationships are subtle (Shan 2007), and often appear only in folklore. Here we focus on a specific suchoperator: shift-zero and dollar without answer-type-modification (Materzok and Biernacki 2012), whose operationalsemantics and type system are the closest to effect handlers and monads.We study these three different abstractions for user-defined effects: effect handlers, monads, and delimitedcontrol operators. Our goal is to enable language designers to conduct a precise and informed discussion aboutthe relative expressiveness of each abstraction. In order to compare them, we build on an idealised calculusfor functional-imperative programming, namely call-by-push-value (Levy 2004), and extend it with each of thethree abstractions and their corresponding natural type systems. We then assess the expressive power of eachabstraction by rigorously comparing and analysing these calculi.We use Felleisen’s notion of macro expressibility (Felleisen 1991): when a programming language L is extendedby some feature, we say that the extended language L is macro expressible when there is a syntax-directedtranslation from L to L that keeps the features in L fixed. Felleisen introduces this notion of reduction tostudy the expressive power of Turing-complete calculi, as macro expressivity is more sensitive in these contextsthan computability and complexity notions of reduction. We adapt Felleisen’s notion to the situation where oneextension L 1 of a base calculus L is macro expressible in another extension L 2 of the same base calculus L.Doing so enable us to formally compare the expressive power for each approach to user-defined effects.In the first instance, we show that, disregarding types, all three abstractions are macro-expressible in terms ofone another, giving six macro-expression translations. Some of these translations are known in less rigorousforms, either published, or in folklore. One translation, macro-expressing effect-handlers in delimited control,improves on previous concrete implementations (Kammar et al. 2013), which rely on the existence of a globalhigher-order memory cell storing a stack of effect-handlers. The translation from monadic reflection to effecthandlers is completely novel.We also establish whether these translations preserve typeability: the translations of some well-typed programsare untypeable. We show that the translation from delimited control to monadic reflection preserves typeability.A potential difference between the expressive power of handler type systems and between monadic reflection anddelimited control type systems was recently pointed out by Kammar and Pretnar (2017), who give a straightforwardtypeability preserving macro-translation of delimited dynamic state into a calculus effect handlers, whereas existingtranslations using monads and delimited control require more sophistication (Kiselyov et al. 2006). Here, weestablish this difference: we demonstrate how to use the denotational semantics for the monadic calculus to provethat there exists no no macro translation from the effect handlers calculus to the monadic reflection calculus thatpreserves typeability. This set-theoretic denotational semantics and its adequacy for Filinski’s multi-monadicmetalanguage (2010) is another piece of folklore which we prove here. We conjecture that a similar proof, thoughwith more mathematical sophistication, can be used to prove the non-existence of a typeability-preserving macroexpression translation from the monadic calculus to effect handlers. To this end, we give adequate set-theoreticsemantics to the effect handler calculus with its type-and-effect system, and highlight the critical semanticinvariant a monadic calculus will invalidate.Fig. 1 summarises our contributions and conjectured results. Untyped calculi appear on the left and theirtyped equivalents on the right. Unlabelled arrows between the typed calculi signify that the correspondingmacro translation between the untyped calculi preserves typeability. Arrows labelled by are new untypedtranslations. Arrows labelled by @ signify that no macro translation exists between the calculi, not even a partialmacro translation that is only defined for well-typed programs.

On the Expressive Power of User-Defined Effectsdeltyped del @@?efftyped [email protected][email protected] @?typed monFig. 1. Existing and conjectured macro translationsThe non-expressivity results are sensitive to the precise collection of features in each calculus. For example,extending the base calculus with inductive types and primitive recursion would create gaps in our non-existencearguments, and we conjecture that extending the calculi with various forms of polymorphism would make ouruntyped translations typeability-preserving. Adding more features to each calculus blurs the distinction betweeneach abstraction. This sensitivity means that in a realistic programming language, such as Haskell, OCaml, orScheme, the different abstractions are often practically equivalent (Schrijvers et al. 2016). It also teaches us thatmeaningful relative expressivity results must be stated within a rigorous framework such as a formal calculus,where the exact assumptions and features are made explicit. The full picture is still far from complete, and ourwork lays the foundation for such a precise treatment.We supplement our pencil-and-paper proofs with a mechanised formalisation in the Abella proof assistant (Gacek 2008, 2009) of the more syntactic aspects of our work. Specifically, we formalise a Wright andFelleisen style progress-and-preservation soundness theorem (1994), which we also call safety, for each calculus,and correctness theorems for our translations.We make the following contributions: three formal calculi, i.e., syntax and semantics, for effect handlers, monadic reflection, and delimitedcontrol extending a shared call-by-push-value core, and their meta-theory:– set-theoretic denotational semantics for effect handlers and monadic reflection;– denotational soundness and adequacy proofs for effect handlers and monadic reflection;– a termination proof for monadic reflection (proofs for the other calculi appear in existing work); six macro-translations between the three untyped calculi, and variations on three of those translations; formally mechanised meta-theory in Abella3 comprising:– progress and preservation theorems;– the translations between the untyped calculi; and– their correctness proofs in terms of formal simulation results; typeability preservation of the macro translation from delimited control to monadic reflection; and a proof that there exists no typeability-preserving macro translation from effect handlers to either monadicreflection or delimited control.We structure the remainder of the paper as follows. Sections 2–5 present the core calculus and its extensionswith effect handlers, monadic reflection, and delimited control, in this order, along with their meta-theoreticproperties. Section 6 presents the macro translations between these calculi, their correctness, and typeabilitypreservation. Section 7 concludes and outlines further work.2THE CORE-CALCULUS: MAMWe are interested in a functional-imperative calculus where effects and higher-order features interact well. Levy’scall-by-push-value (CBPV) calculus (Levy 2004) fits the bill. The CBPV paradigm subsumes call-by-name and3 cts-formalization

Yannick Forster, Ohad Kammar, Sam Lindley, and Matija PretnarV ,W :: valuesxvariable ()unit value (V1 , V2 ) pairing inj Vvariant {M }thunkM, N :: computationscase V ofproduct(x1 , x2 ) M matching case V of {variantinjx M1 matching. 1 1.inj n xn Mn } V! return V x M; N λx.M MV hM 1 , M 2 i prji ingprojectionFig. 2. mam syntaxcall-by-value, both syntactically and semantically. In CBPV evaluation order is explicit, and the way it combinescomputational effects with higher-order features yields simpler program logic reasoning principles (Plotkin andPretnar 2008; Kammar and Plotkin 2012). CBPV allows us to uniformly deal with call-by-value and call-by-nameevaluation strategies, making the theoretical development relevant to both ML-like and Haskell-like languages.We extend it with a type-and-effect system, and, as adjunctions form the semantic basis for CBPV, we call theresulting calculus the multi-adjunctive metalanguage (mam).Fig. 2 presents mam’s raw term syntax, which distinguishes between values (data) and computations (programs).We assume a countable set of variables ranged over by x, y, . . ., and a countable set of variant constructor literalsranged over by . The unit value, product of values, and finite variants/sums are standard. A computation can besuspended as a thunk {M }, which may be passed around. Products and variants are eliminated with standardpattern matching constructs. Thunks can be forced to resume their execution. A computation may simply returna value, and two computations can be sequenced, as in Haskell’s do notation. A function computation abstractsover values to which it may be applied. In order to pass a function λx .M as data, it must first be suspendedas a thunk {λx .M }. For completeness, we also include CBPV’s binary computation products, which subsumeprojections on product values in call-by-name languages.Example 2.1. Using the boolean values injTrue () and injFalse (), we can implement a logical not operation:not {λb.case b of {injTrue x return injFalse ()injFalse x return injTrue ()}}Fig. 3 presents mam’s standard structural operational semantics, in the style of Felleisen and Friedman (1987).In order to reuse the core definitions as much as possible, we refactor the semantics into β-reduction rules an