Skip to content

Research at St Andrews

Programming and reasoning with algebraic effects and dependent types

Research output: Chapter in Book/Report/Conference proceedingConference contribution



School/Research organisations


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.


Original languageEnglish
Title of host publicationICFP '13
Subtitle of host publicationProceedings of the 18th ACM SIGPLAN international conference on Functional programming
Place of PublicationNew York
ISBN (Print)978-1-4503-2326-0
Publication statusPublished - 2013

    Research areas

  • Dependent Types, Algebraic Effects

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Value-dependent session design in a dependently typed language

    de Muijnck-Hughes, J., Brady, E. C. & Vanderbauwhede, W., 2 Apr 2019, Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, Prague, Czech Republic, 7th April 2019. Martins, F. & Orchard, D. (eds.). Open Publishing Association, p. 47-59 (Electronic Proceedings in Theoretical Computer Science; vol. 291).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Subtype polymorphism à la carte via machine learning on dependent types

    Swan, J., Johnson, C. G. & Brady, E. C., 16 Jul 2018, Companion Proceedings for the ISSTA/ECOOP 2018 Workshops. New York, NY: Association for Computing Machinery, Inc, p. 14-16 3 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  3. Type driven development of concurrent communicating systems

    Brady, E. C., 7 Jul 2017, In : Computer Science. 18, 3, 22 p., 1413.

    Research output: Contribution to journalArticle

  4. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C., 17 Mar 2017, In : Logical Methods in Computer Science. 13, 1, 23 p., 7.

    Research output: Contribution to journalArticle

  5. Type-driven development with Idris

    Brady, E. C., Mar 2017, Shelter Island: Manning Publications Co. 480 p.

    Research output: Book/ReportBook

ID: 61401371