research-article

Open access

Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C

Authors:

Daan LeijenAuthors Info & Claims

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

Article No.: 71, Pages 1 - 30

https://doi.org/10.1145/3473576

Published: 19 August 2021 Publication History

Abstract

This paper studies compilation techniques for algebraic effect handlers. In particular, we present a sequence of refinements of algebraic effects, going via multi-prompt delimited control, _generalized evidence passing_, yield bubbling, and finally a monadic translation into plain lambda calculus which can be compiled efficiently to many target platforms. Along the way we explore various interesting points in the design space. We provide two implementations of our techniques, one as a library in Haskell, and one as a C backend for the Koka programming language. We show that our techniques are effective, by comparing against three other best-in-class implementations of effect handlers: multi-core OCaml, the _Ev.Eff_ Haskell library, and the libhandler C library. We hope this work can serve as a basis for future designs and implementations of algebraic effects.

Supplementary Material

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

This is a presentation video of our ICFP 2021 talk. This paper studies compilation techniques for algebraic effect handlers. In particular, we present a sequence of refinements of algebraic effects, going via multi-prompt delimited control, _generalized evidence passing_, yield bubbling, and finally a monadic translation into plain lambda calculus which can be compiled efficiently to many target platforms. Along the way we explore various interesting points in the design space. We provide two implementations of our techniques, one as a library in Haskell, and one as a C backend for the Koka programming language. We show that our techniques are effective, by comparing against three other best-in-class implementations of effect handlers: multi-core OCaml, the _Ev.Eff_ Haskell library, and the libhandler C library. We hope this work can serve as a basis for future designs and implementations of algebraic effects.

Download
113.07 MB

MP4 File (3473576.mp4)

Presentation Videos

Download
32.44 MB

References

[1]

Kenichi Asai and Yukiyoshi Kameyama. 2007. Polymorphic Delimited Continuations. 239–254. https://doi.org/10.1007/978-3-540-76637-7_16

[2]

Arthur I. Baars and S. Doaitse Swierstra. 2002. Typing Dynamic Typing. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP’02). 157–166. isbn:1581134878 https://doi.org/10.1145/581478.581494

Digital Library

[3]

Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program., 84, 1 (2015), 108–123. https://doi.org/10.1016/j.jlamp.2014.02.001

[4]

Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism. Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 126, Nov., 30 pages. https://doi.org/10.1145/3428194

Digital Library

[5]

Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effekt: Capability-Passing Style for Type- and Effect-safe, Extensible Effect Handlers in Scala. Journal of Functional Programming.

[6]

Olivier Danvy and Andrzej Filinski. 1989. A Functional Abstraction of Typed Contexts. DIKU, University of Copenhagen.

[7]

Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Madhavapeddy, KC Sivaramakrishnan, and Leo White. 2017. Effectively Tackling the Awkward Squad. In ML Workshop.

[8]

Stephen Dolan, Leo White, KC Sivaramakrishnan, Jeremy Yallop, and Anil Madhavapeddy. 2015. Effective concurrency through algebraic effects. In OCaml Workshop.

[9]

R Kent Dybvig, Simon Peyton Jones, and Amr Sabry. 2007. A monadic framework for delimited continuations. Journal of Functional Programming, 17, 6 (2007), 687–730. https://doi.org/10.1017/S0956796807006259

Digital Library

[10]

Kavon Farvardin and John Reppy. 2020. From Folklore to Fact: Comparing Implementations of Stacks and Continuations. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). 75–90. https://doi.org/10.1145/3385412.3385994

Digital Library

[11]

Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, and Bruce F. Duba. 1986. Reasoning with Continuations. In Proceedings of the 1st Symposium on Logic in Computer Science (LICS). 131–141.

[12]

Matthew Flatt and R. Kent Dybvig. 2020. Compiler and Runtime Support for Continuation Marks. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). ACM, 45–58. isbn:9781450376136 https://doi.org/10.1145/3385412.3385981

Digital Library

[13]

Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. 2019. On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. Journal of Functional Programming, 29 (2019), 15. https://doi.org/10.1017/S0956796819000121 arxiv:1610.09161.

[14]

Carl A. Gunter, Didier Rémy, and Jon G. Riecke. 1995. A Generalization of Exceptions and Control in ML-like Languages. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture (FPCA ’95). ACM, 12–23. isbn:0897917197 https://doi.org/10.1145/224164.224173

Digital Library

[15]

Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web up to Speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). Association for Computing Machinery, New York, NY, USA. 185–200. isbn:9781450349888 https://doi.org/10.1145/3062341.3062363

Digital Library

[16]

Daniel Hillerström and Sam Lindley. 2018. Shallow Effect Handlers. In 16th Asian Symposium on Programming Languages and Systems (APLAS’18). 415–435.

[17]

Daniel Hillerstr&ouml, m, Sam Lindley, Bob Atkey, and KC Sivaramakrishnan. 2017. Continuation Passing Style for Effect Handlers. In Proceedings of the second International Conference on Formal Structures for Computation and Deduction (FSCD’17).

[18]

Daniel Hillerström and Sam Lindley. 2016. Liberating Effects with Rows and Handlers. In Proceedings of the 1st International Workshop on Type-Driven Development (TyDe 2016). 15–27. https://doi.org/10.1145/2976022.2976033

Digital Library

[19]

Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in Action. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). ACM, New York, NY, USA. 145–158. isbn:978-1-4503-2326-0 https://doi.org/10.1145/2500365.2500590

Digital Library

[20]

Ohad Kammar and Matija Pretnar. 2017. No value restriction is needed for algebraic effects and handlers. Journal of Functional Programming, 27, 1 (2017), Jan., https://doi.org/10.1017/S0956796816000320

[21]

Oleg Kiselyov and Hiromi Ishii. 2015. Freer Monads, More Extensible Effects. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell (Haskell ’15). 94–105. https://doi.org/10.1145/2804302.2804319

Digital Library

[22]

Oleg Kiselyov, Chung-chieh Shan, and Amr Sabry. 2006. Delimited Dynamic Binding. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). Association for Computing Machinery, New York, NY, USA. 26–37. isbn:1595933093 https://doi.org/10.1145/1159803.1159808

Digital Library

[23]

Oleg Kiselyov and KC Sivaramakrishnan. 2017. Eff directly in OCaml. In ML workshop 2016. http://kcsrk.info/papers/caml-eff17.pdf Extended version.

[24]

Daan Leijen. 2005. Extensible records with scoped labels. In Proceedings of the 2005 Symposium on Trends in Functional Programming. 297–312.

[25]

Daan Leijen. 2017. Implementing Algebraic Effects in C: or Monads for free in C. Programming Languages and Systems, 10695, 1 (2017), 339–363. APLAS’17.

[26]

Daan Leijen. 2017. Type Directed Compilation of Row-typed Algebraic Effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17). 486–499. isbn:978-1-4503-4660-3 https://doi.org/10.1145/3009837.3009872

Digital Library

[27]

Daan Leijen. 2020. The Koka Programming Language. Nov., https://koka-lang.github.io

[28]

Daan Leijen. 2021. Effect Handler Benchmarks. May, https://github.com/daanx/effect-bench

[29]

Paul Blain Levy. 2006. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19, 4 (2006), 377–414.

Digital Library

[30]

Michel Parigot. 1992. λμ-Calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, Andrei Voronkov (Ed.). Springer Berlin Heidelberg, 190–201. isbn:978-3-540-47279-7

[31]

Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Applied Categorical Structures, 11, 1 (2003), 69–94. https://doi.org/10.1023/A:1023064908962

[32]

Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In 18th European Symposium on Programming Languages and Systems (ESOP’09). 80–94. https://doi.org/10.1007/978-3-642-00590-9_7

Digital Library

[33]

Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Logical Methods in Computer Science, 9, 4, https://doi.org/10.2168/LMCS-9(4:23)2013

[34]

Matija Pretnar. 2015. An Introduction to Algebraic Effects and Handlers. Invited Tutorial Paper. Electron. Notes Theor. Comput. Sci., 319, C (2015), Dec., 19–35. issn:1571-0661 https://doi.org/10.1016/j.entcs.2015.12.003

Digital Library

[35]

Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen. 2021. Perceus: Garbage Free Reference Counting with Reuse. In 42rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’21).

[36]

Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff. 2019. Monad Transformers and Modular Algebraic Effects: What Binds Them Together. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell (Haskell 2019). Association for Computing Machinery, New York, NY, USA. 98–113. isbn:9781450368131 https://doi.org/10.1145/3331545.3342595

Digital Library

[37]

Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann. 2020. Compiling Effect Handlers in Capability-Passing Style. Proc. ACM Program. Lang., 4, ICFP (2020), Article 93, Aug., 28 pages. https://doi.org/10.1145/3408975

Digital Library

[38]

KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, and Anil Madhavapeddy. 2021. Retrofitting Effect Handlers onto OCaml. In 42rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’21).

[39]

Martin Sulzmann, Manuel Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007. System F with type equality coercions. In ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI’07). ACM press, 53–66.

Digital Library

[40]

Herb Sutter. 2019. Zero-overhead deterministic exceptions: Throwing values. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p0709r4.pdf ISO/IEC WG2.1, P0709R4.

[41]

Nicolas Wu and Tom Schrijvers. 2015. Fusion for Free: Efficient Algebraic Effect Handlers. In Proceedings of the 12th International Conference on Mathematics of Program Construction (MPC 2015, Vol. 9129). 302.

[42]

Nicolas Wu, Tom Schrijvers, and Ralf Hinze. 2014. Effect Handlers in Scope. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell (Haskell ’14). 1–12. isbn:978-1-4503-3041-1 https://doi.org/10.1145/2633357.2633358

Digital Library

[43]

Ningning Xie, Jonathan Brachthäuser, Phillip Schuster, Daniel Hillerström, and Daan Leijen. 2020. Effect Handlers, Evidently. In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP’2020). https://doi.org/10.1145/3408981

Digital Library

[44]

Ningning Xie and Daan Leijen. 2020. Effect Handlers in Haskell, Evidently. In Proceedings of the 2020 ACM SIGPLAN Symposium on Haskell (Haskell’20). https://doi.org/10.1145/3406088.3409022

Digital Library

[45]

Ningning Xie and Daan Leijen. 2021. Generalized Evidence Passing for Effect Handlers. Microsoft Research. Extended version with proofs.

[46]

Ningning Xie and Daan Leijen. 2021. Mp.Eff: Efficient effect handlers based on Evidence Passing Semantics. March, https://github.com/xnning/MpEff

[47]

Yizhou Zhang and Andrew C. Myers. 2019. Abstraction-Safe Effect Handlers via Tunneling. Proc. ACM Program. Lang., 3, POPL (2019), Jan., 29 pages. https://doi.org/10.1145/3290318

Digital Library

Cited By

Alvarez-Picallo MFreund TGhica DLindley S(2024)Effect Handlers for C via CoroutinesProceedings of the ACM on Programming Languages10.1145/36897988:OOPSLA2(2462-2489)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689798
Ma CGe ZLee EZhang Y(2024)Lexical Effect Handlers, DirectlyProceedings of the ACM on Programming Languages10.1145/36897708:OOPSLA2(1670-1698)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689770
Pham COdersky MRacordon DZendra O(2024)Stack-Copying Delimited Continuations for Scala NativeProceedings of the 19th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems10.1145/3679005.3685979(2-13)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679005.3685979
Show More Cited By

Index Terms

Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Control structures
        Polymorphism
2. Theory of computation
  1. Logic
    1. Type theory

Recommendations

Efficient compilation of algebraic effect handlers

The popularity of algebraic effect handlers as a programming language feature for user-defined computational effects is steadily growing. Yet, even though efficient runtime representations have already been studied, most handler-based programs are still ...
Effects as capabilities: effect handlers and lightweight effect polymorphism

Effect handlers have recently gained popularity amongst programming language researchers. Existing type- and effect systems for effect handlers are often complicated and potentially hinder a wide-spread adoption.

We present the language Effekt with the ...
Handlers in action
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Plotkin and Pretnar's handlers for algebraic effects occupy a sweet spot in the design space of abstractions for effectful computation. By separating effect signatures from their implementation, algebraic effects provide a high degree of modularity, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

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

August 2021

1011 pages

EISSN:2475-1421

DOI:10.1145/3482883

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 August 2021

Published in PACMPL Volume 5, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional / v1.1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
1,062
Total Downloads

Downloads (Last 12 months)266
Downloads (Last 6 weeks)53

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Alvarez-Picallo MFreund TGhica DLindley S(2024)Effect Handlers for C via CoroutinesProceedings of the ACM on Programming Languages10.1145/36897988:OOPSLA2(2462-2489)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689798
Ma CGe ZLee EZhang Y(2024)Lexical Effect Handlers, DirectlyProceedings of the ACM on Programming Languages10.1145/36897708:OOPSLA2(1670-1698)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689770
Pham COdersky MRacordon DZendra O(2024)Stack-Copying Delimited Continuations for Scala NativeProceedings of the 19th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems10.1145/3679005.3685979(2-13)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679005.3685979
Müller MSchuster PStarup JOstermann KBrachthäuser J(2023)From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228317:OOPSLA2(941-970)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622831
Phipps-Costin LRossberg AGuha ALeijen DHillerström DSivaramakrishnan KPretnar MLindley S(2023)Continuing WebAssembly with Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228147:OOPSLA2(460-485)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622814
Leijen DLorenzen A(2023)Tail Recursion Modulo Context: An Equational ApproachProceedings of the ACM on Programming Languages10.1145/35712337:POPL(1152-1181)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571233
Ghica DLindley SBravo MPiróg M(2022)High-level effect handlers in C++Proceedings of the ACM on Programming Languages10.1145/35634456:OOPSLA2(1639-1667)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563445
Xie NCong YIkemori KLeijen D(2022)First-class names for effect handlersProceedings of the ACM on Programming Languages10.1145/35632896:OOPSLA2(30-59)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563289
Lorenzen ALeijen D(2022)Reference counting with frame limited reuseProceedings of the ACM on Programming Languages10.1145/35476346:ICFP(357-380)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547634
Ikemori KCong YMasuhara HLeijen D(2022)Sound and Complete Type Inference for Closed Effect RowsTrends in Functional Programming10.1007/978-3-031-21314-4_8(144-168)Online publication date: 17-Mar-2022
https://dl.acm.org/doi/10.1007/978-3-031-21314-4_8
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents