On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
<p>We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion abou...
| Huvudupphovsmän: | , , , |
|---|---|
| Materialtyp: | Journal article |
| Publicerad: |
Association for Computing Machinery (ACM)
2017
|
| Ämnen: |
| _version_ | 1826279056680681472 |
|---|---|
| author | Forster, Y Kammar, O Lindley, S Pretnar, M |
| author_facet | Forster, Y Kammar, O Lindley, S Pretnar, M |
| author_sort | Forster, Y |
| collection | OXFORD |
| description | <p>We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.</p> <p>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-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen&apos;s notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.</p> |
| first_indexed | 2024-03-06T23:53:08Z |
| format | Journal article |
| id | oxford-uuid:734c8c07-0d2e-4f7b-bae0-94e94c3d0640 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T23:53:08Z |
| publishDate | 2017 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | oxford-uuid:734c8c07-0d2e-4f7b-bae0-94e94c3d06402022-03-26T19:55:31ZOn the expressive power of user-defined effects: effect handlers, monadic reflection, delimited controlJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:734c8c07-0d2e-4f7b-bae0-94e94c3d0640operational semanticstheory of computation: control primitivesdenotational semanticsfunctional constructscategorical semanticstype structuresSymplectic Elements at OxfordAssociation for Computing Machinery (ACM)2017Forster, YKammar, OLindley, SPretnar, M <p>We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.</p> <p>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-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen&apos;s notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.</p> |
| spellingShingle | operational semantics theory of computation: control primitives denotational semantics functional constructs categorical semantics type structures Forster, Y Kammar, O Lindley, S Pretnar, M On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control |
| title | On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control |
| title_full | On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control |
| title_fullStr | On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control |
| title_full_unstemmed | On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control |
| title_short | On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control |
| title_sort | on the expressive power of user defined effects effect handlers monadic reflection delimited control |
| topic | operational semantics theory of computation: control primitives denotational semantics functional constructs categorical semantics type structures |
| work_keys_str_mv | AT forstery ontheexpressivepowerofuserdefinedeffectseffecthandlersmonadicreflectiondelimitedcontrol AT kammaro ontheexpressivepowerofuserdefinedeffectseffecthandlersmonadicreflectiondelimitedcontrol AT lindleys ontheexpressivepowerofuserdefinedeffectseffecthandlersmonadicreflectiondelimitedcontrol AT pretnarm ontheexpressivepowerofuserdefinedeffectseffecthandlersmonadicreflectiondelimitedcontrol |