skip to main content
10.1145/3009837.3009897acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Do be do be do

Published:01 January 2017Publication History

ABSTRACT

We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar's effect handler abstraction.

Effect handlers provide an abstraction for modular effectful programming: a handler acts as an interpreter for a collection of commands whose interfaces are statically tracked by the type system. However, Frank eliminates the need for an additional effect handling construct by generalising the basic mechanism of functional abstraction itself. A function is simply the special case of a Frank operator that interprets no commands. Moreover, Frank's operators can be multihandlers which simultaneously interpret commands from several sources at once, without disturbing the direct style of functional programming with values.

Effect typing in Frank employs a novel form of effect polymorphism which avoid mentioning effect variables in source code. This is achieved by propagating an ambient ability inwards, rather than accumulating unions of potential effects outwards.

We introduce Frank by example, and then give a formal account of the Frank type system and its semantics. We introduce Core Frank by elaborating Frank operators into functions, case expressions, and unary handlers, and then give a sound small-step operational semantics for Core Frank.

Programming with effects and handlers is in its infancy. We contribute an exploration of future possibilities, particularly in combination with other forms of rich type system.

References

  1. A. Abel and B. Pientka. Wellfounded recursion with copatterns: a unified approach to termination and productivity. In Morrisett and Uustalu {43}, pages 185–196. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. M. D. Adams and O. S. A˘gacan. Indentation-sensitive parsing for Parsec. In Haskell. ACM, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. R. Atkey. An algebraic approach to typechecking and elaboration, 2015.Google ScholarGoogle Scholar
  4. R. Atkey and C. McBride. Productive coprogramming with guarded recursion. In Morrisett and Uustalu {43}, pages 197–208. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. A. Bauer and M. Pretnar. An effect system for algebraic effects and handlers. Logical Methods in Computer Science, 10(4), 2014.Google ScholarGoogle Scholar
  6. A. Bauer and M. Pretnar. Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program., 84(1):108–123, 2015.Google ScholarGoogle ScholarCross RefCross Ref
  7. E. Brady. Programming and reasoning with algebraic effects and dependent types. In Morrisett and Uustalu {43}, pages 133–144. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. E. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23:552–593, 9 2013.Google ScholarGoogle ScholarCross RefCross Ref
  9. M. M. T. Chakravarty, Z. Hu, and O. Danvy, editors. ICFP, 2011. ACM.Google ScholarGoogle Scholar
  10. E. Cooper, S. Lindley, P. Wadler, and J. Yallop. Links: Web programming without tiers. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever, editors, FMCO, volume 4709 of Lecture Notes in Computer Science, pages 266–296. Springer, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. S. Dolan, L. White, K. Sivaramakrishnan, J. Yallop, and A. Madhavapeddy. Effective concurrency through algebraic effects. In OCaml Workshop, 2015.Google ScholarGoogle Scholar
  12. A. Filinski. Representing layered monads. In A. W. Appel and A. Aiken, editors, POPL, pages 175–188. ACM, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. A. Filinski. Monads in action. In M. V. Hermenegildo and J. Palsberg, editors, POPL, pages 483–494. ACM, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Y. Forster, O. Kammar, S. Lindley, and M. Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. CoRR, abs/1610.09161, 2012.Google ScholarGoogle Scholar
  15. C. Fournet and G. Gonthier. The reflexive CHAM and the joincalculus. In H. Boehm and G. L. S. Jr., editors, POPL, pages 372–385. ACM, 1996. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. A. Gundry, C. McBride, and J. McKinna. Type inference in context. In MSFP. ACM, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. A. M. Gundry. Type Inference, Haskell and Dependent Types. PhD thesis, University of Strathclyde, 2013.Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. P. Hancock and P. Hyvernat. Programming interfaces and basic topology. Ann. Pure Appl. Logic, 137(1-3):189–239, 2006.Google ScholarGoogle ScholarCross RefCross Ref
  19. D. Hillerström. Handlers for algebraic effects in Links. Master’s thesis, School of Informatics, The University of Edinburgh, 2015.Google ScholarGoogle Scholar
  20. D. Hillerström. Compilation of effect handlers and their applications in concurrency. Master’s thesis, School of Informatics, The University of Edinburgh, 2016.Google ScholarGoogle Scholar
  21. D. Hillerström and S. Lindley. Liberating effects with rows and handlers. In J. Chapman and W. Swierstra, editors, TyDe, pages 15–27. ACM, 2016. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. R. Hinze and J. Voigtländer, editors. MPC, volume 9129 of Lecture Notes in Computer Science, 2015. Springer.Google ScholarGoogle ScholarCross RefCross Ref
  23. J. Hughes. Programming with arrows. In Advanced Functional Programming, volume 3622 of Lecture Notes in Computer Science, pages 73–129. Springer, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. O. Kammar, S. Lindley, and N. Oury. Handlers in action. In Morrisett and Uustalu {43}, pages 145–158. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. O. Kiselyov and H. Ishii. Freer monads, more extensible effects. In B. Lippmeier, editor, Haskell, pages 94–105. ACM, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. O. Kiselyov, A. Sabry, and C. Swords. Extensible effects: an alternative to monad transformers. In C. Shan, editor, Haskell, pages 59–70. ACM, 2013. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. E. A. Kmett. Trifecta (1.5.2), 2015. http://hackage.haskell.org/package/trifecta-1.5.2.Google ScholarGoogle Scholar
  28. D. Leijen. Koka: Programming with row polymorphic effect types. In P. Levy and N. Krishnaswami, editors, MSFP, volume 153 of EPTCS, pages 100–126, 2014.Google ScholarGoogle Scholar
  29. D. Leijen. Type directed compilation of row-typed algebraic effects. In A. D. Gordon, editor, POPL. ACM, 2017. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. D. Leijen and P. Martini. Parsec (3.1.9), 2015. http://hackage.haskell.org/package/parsec-3.1.9.Google ScholarGoogle Scholar
  31. P. B. Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. S. Lindley. Algebraic effects and effect handlers for idioms and arrows. In J. P. Magalh˜aes and T. Rompf, editors, WGP, pages 47– 58. ACM, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. S. Lindley, C. McBride, and C. McLaughlin. Frank junior, 2016. https://www.github.com/cmcl/frankjnr.Google ScholarGoogle Scholar
  34. J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In J. Ferrante and P. Mager, editors, POPL, pages 47–57. ACM, 1988. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. D. B. MacQueen. Modules for standard ML. In LISP and Functional Programming, pages 198–207, 1984. Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. L. Maranget. Compiling pattern matching to good decision trees. In ML, pages 35–46. ACM, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. C. McBride. How might effectful programs look? In Workshop on Effects and Type Theory, 2007. http://cs.ioc.ee/efftt/mcbride-slides.pdf.Google ScholarGoogle Scholar
  38. C. McBride. Kleisli arrows of outrageous fortune, 2011. Draft. https://personal.cis.strath.ac.uk/conor.mcbride/ Kleisli.pdf.Google ScholarGoogle Scholar
  39. C. McBride. Frank (0.3), 2012. http://hackage.haskell.org/package/Frank.Google ScholarGoogle Scholar
  40. C. McBride. Turing-completeness totally free. In Hinze and Voigtländer {22}, pages 257–275.Google ScholarGoogle Scholar
  41. C. McBride. Shonky, 2016. https://github.com/pigworker/shonky.Google ScholarGoogle Scholar
  42. C. McBride and R. Paterson. Applicative programming with effects. J. Funct. Program., 18(1):1–13, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. G. Morrisett and T. Uustalu, editors. ICFP, 2013. ACM.Google ScholarGoogle Scholar
  44. B. C. Pierce and D. N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1–44, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  45. G. D. Plotkin and J. Power. Semantics for algebraic operations. Electr. Notes Theor. Comput. Sci., 45:332–345, 2001.Google ScholarGoogle ScholarCross RefCross Ref
  46. G. D. Plotkin and J. Power. Adequacy for algebraic effects. In F. Honsell and M. Miculan, editors, FOSSACS, volume 2030 of Lecture Notes in Computer Science, pages 1–24. Springer, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  47. G. D. Plotkin and J. Power. Notions of computation determine monads. In M. Nielsen and U. Engberg, editors, FOSSACS, volume 2303 of Lecture Notes in Computer Science, pages 342–356. Springer, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  48. G. D. Plotkin and J. Power. Algebraic operations and generic effects. Appl. Categ. Structures, 11(1):69–94, 2003.Google ScholarGoogle ScholarCross RefCross Ref
  49. G. D. Plotkin and M. Pretnar. Handling algebraic effects. Logical Methods in Computer Science, 9(4), 2013.Google ScholarGoogle Scholar
  50. M. Pretnar. Inferring algebraic effects. Logical Methods in Computer Science, 10(3), 2014.Google ScholarGoogle Scholar
  51. T. Schrijvers, N. Wu, B. Desouter, and B. Demoen. Heuristics entwined with handlers combined: From functional specification to logic programming implementation. In O. Chitil, A. King, and O. Danvy, editors, PPDP, pages 259–270. ACM, 2014. Google ScholarGoogle ScholarDigital LibraryDigital Library
  52. T. Schrijvers, M. Pir`og, N. Wu, and M. Jaskelioff. Monad transformers and modular algebraic effects. Technical report, University of Leuven, 2016.Google ScholarGoogle Scholar
  53. O. Shivers and A. J. Turon. Modular rollback through control logging: a pair of twin functional pearls. In Chakravarty et al. {9}, pages 58–68. Google ScholarGoogle ScholarDigital LibraryDigital Library
  54. N. Swamy, N. Guts, D. Leijen, and M. Hicks. Lightweight monadic programming in ML. In Chakravarty et al. {9}, pages 15–27. Google ScholarGoogle ScholarDigital LibraryDigital Library
  55. W. Swierstra. Data types à la carte. J. Funct. Program., 18(4):423– 436, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  56. W. Swierstra, editor. Haskell, 2014. ACM.Google ScholarGoogle Scholar
  57. J. Talpin and P. Jouvelot. The type and effect discipline. Inf. Comput., 111(2):245–296, 1994. Google ScholarGoogle ScholarDigital LibraryDigital Library
  58. A. van der Ploeg and O. Kiselyov. Reflection without remorse: revealing a hidden sequence to speed up monadic reflection. In SwierstraGoogle ScholarGoogle Scholar
  59. , pages 133–144.Google ScholarGoogle Scholar
  60. K. Vonnegut. Deadeye Dick. Delacorte Press, 1982.Google ScholarGoogle Scholar
  61. P. Wadler. The essence of functional programming. In R. Sethi, editor, POPL, pages 1–14. ACM, 1992. Google ScholarGoogle ScholarDigital LibraryDigital Library
  62. P. Wadler and S. Blott. How to make ad-hoc polymorphism less adhoc. In POPL, pages 60–76. ACM, 1989. Google ScholarGoogle ScholarDigital LibraryDigital Library
  63. N. Wu and T. Schrijvers. Fusion for free - efficient algebraic effect handlers. In Hinze and Voigtländer {22}, pages 302–322.Google ScholarGoogle Scholar

Index Terms

  1. Do be do be do

    Recommendations

    Comments

    Login options

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

    Sign in
    • Published in

      cover image ACM Conferences
      POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
      January 2017
      901 pages
      ISBN:9781450346603
      DOI:10.1145/3009837

      Copyright © 2017 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].

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      • Published: 1 January 2017

      Permissions

      Request permissions about this article.

      Request Permissions

      Check for updates

      Qualifiers

      • research-article

      Acceptance Rates

      Overall Acceptance Rate824of4,130submissions,20%

      Upcoming Conference

      POPL '25

    PDF Format

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader