More Web Proxy on the site http://driver.im/

research-article

Programming and reasoning with algebraic effects and dependent types

Author:

Edwin BradyAuthors Info & Claims

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Pages 133 - 144

https://doi.org/10.1145/2500365.2500581

Published: 25 September 2013 Publication History

Abstract

One often cited benefit of pure functional programming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions with the outside world. Haskell solves this problem using monads to capture details of possibly side-effecting computations --- it provides monads for capturing state, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects.

Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.

References

[1]

J. Aldrich, J. Sunshine, D. Saini, and Z. Sparks. Typestate-oriented programming. In Proceedings of the 24th conference on Object Oriented Programming Systems Languages and Applications, pages 1015--1012, 2009.

Digital Library

[2]

L. Augustsson and M. Carlsson. An exercise in dependent types: A well-typed interpreter, 1999. In Workshop on Dependent Types in Programming, Gothenburg.

[3]

A. Bauer and M. Pretnar. Programming with Algebraic Effects and Handlers, 2012. Available from http://arxiv.org/abs/1203. 1539.

[4]

E. Brady. Idris, a General Purpose Programming Language: Design and Implementation, 2013. Draft.

[5]

E. Brady. Programming in Idris: a Tutorial, 2013. Available from http://idris-lang.org/tutorial.

[6]

newblock {An exercise in dependent types: A well-typed interpreter}, 1999E. Brady and K. Hammond. A verified staged interpreter is a verified compiler. In Generative Programming and Component Engineering (GPCE 2006). ACM, 2006.

Digital Library

[7]

E. Brady and K. Hammond. Correct-by-construction concurrency: Using dependent types to verify implementations of effectful resource usage protocols. Fundamenta Informaticae, 102:145--176, 2010.

Digital Library

[8]

E. Brady and K. Hammond. Scrapping your inefficient engine: Using partial evaluation to improve domain-specific language implementation. In Proceedings of the 15th International Conference on Functional Programming (ICFP '10), pages 297--308. ACM, 2010.

Digital Library

[9]

E. Brady and K. Hammond. Resource-safe Systems Programming with Embedded Domain Specific Languages. In Practical Applications of Declarative Languages, pages 242--257, 2012.

Digital Library

[10]

J. Carette, O. Kiselyov, and C.-C. Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(05):509--543.

Digital Library

[11]

D. Delahaye. A tactic language for the system Coq. In Logic for Programming and Automated Reasoning (LPAR), volume 1955 of LNAI, pages 85--95. Springer, 2000.

Digital Library

[12]

P. Hancock and A. Setzer. Interactive Programs in Dependent Type Theory. In Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, pages 317--331, Aug. 2000.

Digital Library

[13]

M. Hyland, G. Plotkin, and J. Power. Combining effects: Sum and tensor. Theoretical Computer Science, 357:70--99, 2006.

Digital Library

[14]

M. Jaskelioff. Modular monad transformers. In ESOP 09: Proceedings of the 18th European Symposium on Programming Languages and Systems, LNCS, pages 64--79. Springer, 2009.

Digital Library

[15]

O. Kammar, S. Lindley, and N. Oury. Handlers in action. In Proceedings of the 18th International Conference on Functional Programming (ICFP '13). ACM, 2013.

Digital Library

[16]

P. B. Levy. Call-By-Push-Value. PhD thesis, Queen Mary and Westfield College, University of London, 2001.

[17]

S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pages 333--343, New York, New York, USA, Jan. 1995. ACM Press.

Digital Library

[18]

B. Lippmeier. Witnessing Purity, Constancy and Mutability. In 7th Asian Symposium on Programming Languages and Systems (APLAS 2009), volume 5904 of LNCS, pages 95--110. Springer, 2009.

Digital Library

[19]

C. McBride. Kleisli arrows of outrageous fortune, 2011. Draft.

[20]

C. McBride and R. Paterson. Applicative programming with effects. Journal of functional programming, 18(1):1--13, 2008.

Digital Library

[21]

M. Michelbrink and A. Setzer. State dependent IO-monads in type theory. Electronic Notes in Theoretical Computer Science, 122:127--146, 2005.

Digital Library

[22]

A. Nanevski, G. Morrisett, and L. Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5--6):865--911, Sept. 2008.

Digital Library

[23]

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent types for imperative programs. In Proceedings of the 13th International Conference on Functional Programming (ICFP '08), pages 229--240. ACM, 2008.

Digital Library

[24]

M. Odersky, P. Altherr, V. Cremet, B. Emir, S. Maneth, S. Micheloud, N. Mihaylov, M. Schinz, E. Stenman, and M. Zenger. An overview of the Scala programming language. Technical report, 2004.

[25]

E. Pasalic, W. Taha, and T. Sheard. Tagless staged interpreters for typed languages. In Proceedings of the 7th International Conference on Functional Programming (ICFP '02), volume 37, pages 218--229. ACM, Sept. 2002.

Digital Library

[26]

S. Peyton Jones. Haskell 98 Language and Libraries: The Revised Report. Technical report, 2002.

[27]

G. Plotkin and M. Pretnar. Handlers of Algebraic Effects. In ESOP 09: Proceedings of the 18th European Symposium on Programming Languages and Systems, pages 80--94, 2009.

Digital Library

[28]

M. Pretnar. The Logic and Handling of Algebraic Effects. PhD thesis, University of Edinburgh, 2010.

[29]

R. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, SE-12(1):157--171, 1986.

Digital Library

[30]

W. Swierstra. Data types a la carte. Journal of functional programming, 18(4):423--436, 2008.

Digital Library

[31]

P. Wadler. Monads for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, volume 925 of LNCS, pages 24--52. Springer, 1995.

Digital Library

[32]

D. Walker. A Type System for Expressive Security Policies. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '00, pages 254--267. ACM, 2000.

Digital Library

[33]

H. Xi. Imperative Programming with Dependent Types. In 15th Annual IEEE Symposium on Logic in Computer Science, pages 375--387, 2000.

Digital Library

Cited By

Bunkenburg NWu NVazou NMorris J(2024)Making a Curry Interpreter using Effects and HandlersProceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678279(68-82)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678279
Lutze MMadsen M(2024)Associated Effects: Flexible Abstractions for Effectful ProgrammingProceedings of the ACM on Programming Languages10.1145/36563938:PLDI(394-416)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656393
Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Show More Cited By

Index Terms

Programming and reasoning with algebraic effects and dependent types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages

Recommendations

Programming and reasoning with algebraic effects and dependent types
ICFP '13

One often cited benefit of pure functional programming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions with the outside ...
Handling fibred algebraic effects

We study algebraic computational effects and their handlers in the dependently typed setting. We describe computational effects using a generalisation of Plotkin and Pretnar's effect theories, whose dependently typed operations allow us to capture ...
Algebraic effects and effect handlers for idioms and arrows
WGP '14: Proceedings of the 10th ACM SIGPLAN workshop on Generic programming

Plotkin and Power's algebraic effects combined with Plotkin and Pretnar's effect handlers provide a foundation for modular programming with effects. We present a generalisation of algebraic effects and effect handlers to support other kinds of effectful ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

September 2013

484 pages

ISBN:9781450323260

DOI:10.1145/2500365

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Tarmo Uustalu
Institute of Cybernetics at TUT, Estonia

ACM SIGPLAN Notices Volume 48, Issue 9
ICFP '13
September 2013
457 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2544174
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
Northeastern University

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP'13

Sponsor:

SIGPLAN

ICFP'13: ACM SIGPLAN International Conference on Functional Programming

September 25 - 27, 2013

Massachusetts, Boston, USA

Acceptance Rates

ICFP '13 Paper Acceptance Rate 40 of 133 submissions, 30%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

81
Total Citations
View Citations
765
Total Downloads

Downloads (Last 12 months)52
Downloads (Last 6 weeks)1

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bunkenburg NWu NVazou NMorris J(2024)Making a Curry Interpreter using Effects and HandlersProceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678279(68-82)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678279
Lutze MMadsen M(2024)Associated Effects: Flexible Abstractions for Effectful ProgrammingProceedings of the ACM on Programming Languages10.1145/36563938:PLDI(394-416)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656393
Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Frölich Dvan Binsbergen L(2024) i C o L a +Journal of Systems and Software10.1016/j.jss.2024.111979211:COnline publication date: 2-Jul-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.111979
Madsen Mvan de Pol JHenriksen T(2023)Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect SystemsProceedings of the ACM on Programming Languages10.1145/36228167:OOPSLA2(516-543)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622816
Bach Poulsen Cvan der Rest C(2023)Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsProceedings of the ACM on Programming Languages10.1145/35712557:POPL(1801-1831)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571255
Yang ZWu N(2021)Reasoning about effect interaction by fusionProceedings of the ACM on Programming Languages10.1145/34735785:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473578
Spanò ACortesi A(2020)Legodroid: A Type-Driven Library for Android and LEGO Mindstorms InteroperabilitySensors10.3390/s2007192620:7(1926)Online publication date: 30-Mar-2020
https://doi.org/10.3390/s20071926
Swamy NRastogi AFromherz AMerigoux DAhman DMartínez G(2020)SteelCore: an extensible concurrent separation logic for effectful dependently typed programsProceedings of the ACM on Programming Languages10.1145/34090034:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3409003
PIETERS RRIVAS ESCHRIJVERS T(2020)Generalized monoidal effects and handlersJournal of Functional Programming10.1017/S095679682000010630Online publication date: 28-Jul-2020
https://doi.org/10.1017/S0956796820000106
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents