Inferring Algebraic Effects

Matija Pretnar

doi:10.2168/LMCS-10(3:21)2014

Matija Pretnar - Inferring Algebraic Effects

lmcs:1004 - Logical Methods in Computer Science, September 12, 2014, Volume 10, Issue 3 - https://doi.org/10.2168/LMCS-10(3:21)2014

Inferring Algebraic EffectsArticle

Authors: Matija Pretnar

We present a complete polymorphic effect inference algorithm for an ML-style language with handlers of not only exceptions, but of any other algebraic effect such as input & output, mutable references and many others. Our main aim is to offer the programmer a useful insight into the effectful behaviour of programs. Handlers help here by cutting down possible effects and the resulting lengthy output that often plagues precise effect systems. Additionally, we present a set of methods that further simplify the displayed types, some even by deliberately hiding inferred information from the programmer.

https://doi.org/10.2168/LMCS-10(3:21)2014

Source: arXiv.org:1312.2334

Volume: Volume 10, Issue 3

Published on: September 12, 2014

Imported on: December 5, 2013

Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

68N18 - Functional programming and lambda calculus

Sources:

[1] zbMATH Open.

Bibliographic References

19 Documents citing this article

Wenhao Tang;Daniel Hillerström;Sam Lindley;J. Garrett Morris, 2024, Soundly Handling Linearity, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 1600-1628, 10.1145/3632896, https://doi.org/10.1145/3632896.

Cas van der Rest;Casper Bach Poulsen, Lecture notes in computer science, Towards a Language for Defining Reusable Programming Language Components, pp. 18-38, 2022, 10.1007/978-3-031-21314-4_2.

Kazuki Ikemori;Youyou Cong;Hidehiko Masuhara;Daan Leijen, Lecture notes in computer science, Sound and Complete Type Inference for Closed Effect Rows, pp. 144-168, 2022, 10.1007/978-3-031-21314-4_8.

Yahui Song;Darius Foo;Wei-Ngan Chin, Zenodo (CERN European Organization for Nuclear Research), Automated Temporal Verification for Algebraic Effects, pp. 88-109, 2022, 10.1007/978-3-031-21037-2_5, https://zenodo.org/record/7009119.

GEORGIOS KARACHALIAS;MATIJA PRETNAR;AMR HANY SALEH;STIEN VANDERHALLEN;TOM SCHRIJVERS, 2020, Explicit effect subtyping, arXiv (Cornell University), 30, 10.1017/s0956796820000131, https://arxiv.org/abs/2005.13814.

LUKAS CONVENT;SAM LINDLEY;CONOR MCBRIDE;CRAIG MCLAUGHLIN, 2020, Doo bee doo bee doo, Journal of Functional Programming, 30, 10.1017/s0956796820000039, https://doi.org/10.1017/s0956796820000039.

YANNICK FORSTER;OHAD KAMMAR;SAM LINDLEY;MATIJA PRETNAR, 2019, On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control, Edinburgh Research Explorer (University of Edinburgh), 29, 10.1017/s0956796819000121, https://dl.acm.org/citation.cfm?doid=3136534.3110257.

Amr Hany Saleh;Georgios Karachalias;Matija Pretnar;Tom Schrijvers, Lecture notes in computer science, Explicit Effect Subtyping, pp. 327-354, 2018, 10.1007/978-3-319-89884-1_12, https://doi.org/10.1007/978-3-319-89884-1_12.

Daan Leijen, 2017, Type directed compilation of row-typed algebraic effects, ACM SIGPLAN Notices, 52, 1, pp. 486-499, 10.1145/3093333.3009872.

Daan Leijen, Lecture notes in computer science, Implementing Algebraic Effects in C, pp. 339-363, 2017, 10.1007/978-3-319-71237-6_17.

Daan Leijen, Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, Structured asynchrony with algebraic effects, 2017, Oxford UK, 10.1145/3122975.3122977.

OHAD KAMMAR;MATIJA PRETNAR, 2017, No value restriction is needed for algebraic effects and handlers, arXiv (Cornell University), 27, 10.1017/s0956796816000320, https://arxiv.org/abs/1605.06938.

Sam Lindley;Conor McBride;Craig McLaughlin, 2017, Do be do be do, ACM SIGPLAN Notices, 52, 1, pp. 500-514, 10.1145/3093333.3009897.

Yannick Forster;Ohad Kammar;Sam Lindley;Matija Pretnar, 2017, On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control, Proceedings of the ACM on Programming Languages, 1, ICFP, pp. 1-29, 10.1145/3110257, https://doi.org/10.1145/3110257.

Daan Leijen, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Type directed compilation of row-typed algebraic effects, 2016, Paris France, 10.1145/3009837.3009872.

Daniel Hillerström;Sam Lindley, Edinburgh Research Explorer (University of Edinburgh), Liberating effects with rows and handlers, 2016, Nara Japan, 10.1145/2976022.2976033, https://www.research.ed.ac.uk/en/publications/a55cafe9-5000-4b27-a887-baf7bf8ba5b1.

Sam Lindley;Conor McBride;Craig McLaughlin, Edinburgh Research Explorer (University of Edinburgh), Do be do be do, 2016, Paris France, 10.1145/3009837.3009897, http://hdl.handle.net/20.500.11820/bd2598b0-20ce-4272-821f-985974bdd4f6.

Matija Pretnar, 2015, An Introduction to Algebraic Effects and Handlers. Invited tutorial paper, Electronic Notes in Theoretical Computer Science, 319, pp. 19-35, 10.1016/j.entcs.2015.12.003, https://doi.org/10.1016/j.entcs.2015.12.003.

Andrej Bauer;Matija Pretnar, 2014, An Effect System for Algebraic Effects and Handlers, Logical Methods in Computer Science, Volume 10, Issue 4, 10.2168/lmcs-10(4:9)2014, https://doi.org/10.2168/lmcs-10(4:9)2014.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2518 times.

This article's PDF has been downloaded 755 times.