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.
- 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 ScholarDigital Library
- M. D. Adams and O. S. A˘gacan. Indentation-sensitive parsing for Parsec. In Haskell. ACM, 2014. Google ScholarDigital Library
- R. Atkey. An algebraic approach to typechecking and elaboration, 2015.Google Scholar
- R. Atkey and C. McBride. Productive coprogramming with guarded recursion. In Morrisett and Uustalu {43}, pages 197–208. Google ScholarDigital Library
- A. Bauer and M. Pretnar. An effect system for algebraic effects and handlers. Logical Methods in Computer Science, 10(4), 2014.Google Scholar
- A. Bauer and M. Pretnar. Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program., 84(1):108–123, 2015.Google ScholarCross Ref
- E. Brady. Programming and reasoning with algebraic effects and dependent types. In Morrisett and Uustalu {43}, pages 133–144. Google ScholarDigital Library
- E. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23:552–593, 9 2013.Google ScholarCross Ref
- M. M. T. Chakravarty, Z. Hu, and O. Danvy, editors. ICFP, 2011. ACM.Google Scholar
- 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 ScholarDigital Library
- S. Dolan, L. White, K. Sivaramakrishnan, J. Yallop, and A. Madhavapeddy. Effective concurrency through algebraic effects. In OCaml Workshop, 2015.Google Scholar
- A. Filinski. Representing layered monads. In A. W. Appel and A. Aiken, editors, POPL, pages 175–188. ACM, 1999. Google ScholarDigital Library
- A. Filinski. Monads in action. In M. V. Hermenegildo and J. Palsberg, editors, POPL, pages 483–494. ACM, 2010. Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- A. Gundry, C. McBride, and J. McKinna. Type inference in context. In MSFP. ACM, 2010. Google ScholarDigital Library
- A. M. Gundry. Type Inference, Haskell and Dependent Types. PhD thesis, University of Strathclyde, 2013.Google ScholarDigital Library
- P. Hancock and P. Hyvernat. Programming interfaces and basic topology. Ann. Pure Appl. Logic, 137(1-3):189–239, 2006.Google ScholarCross Ref
- D. Hillerström. Handlers for algebraic effects in Links. Master’s thesis, School of Informatics, The University of Edinburgh, 2015.Google Scholar
- D. Hillerström. Compilation of effect handlers and their applications in concurrency. Master’s thesis, School of Informatics, The University of Edinburgh, 2016.Google Scholar
- 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 ScholarDigital Library
- R. Hinze and J. Voigtländer, editors. MPC, volume 9129 of Lecture Notes in Computer Science, 2015. Springer.Google ScholarCross Ref
- J. Hughes. Programming with arrows. In Advanced Functional Programming, volume 3622 of Lecture Notes in Computer Science, pages 73–129. Springer, 2004. Google ScholarDigital Library
- O. Kammar, S. Lindley, and N. Oury. Handlers in action. In Morrisett and Uustalu {43}, pages 145–158. Google ScholarDigital Library
- O. Kiselyov and H. Ishii. Freer monads, more extensible effects. In B. Lippmeier, editor, Haskell, pages 94–105. ACM, 2015. Google ScholarDigital Library
- 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 ScholarDigital Library
- E. A. Kmett. Trifecta (1.5.2), 2015. http://hackage.haskell.org/package/trifecta-1.5.2.Google Scholar
- 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 Scholar
- D. Leijen. Type directed compilation of row-typed algebraic effects. In A. D. Gordon, editor, POPL. ACM, 2017. Google ScholarDigital Library
- D. Leijen and P. Martini. Parsec (3.1.9), 2015. http://hackage.haskell.org/package/parsec-3.1.9.Google Scholar
- P. B. Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. Google ScholarDigital Library
- 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 ScholarDigital Library
- S. Lindley, C. McBride, and C. McLaughlin. Frank junior, 2016. https://www.github.com/cmcl/frankjnr.Google Scholar
- J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In J. Ferrante and P. Mager, editors, POPL, pages 47–57. ACM, 1988. Google ScholarDigital Library
- D. B. MacQueen. Modules for standard ML. In LISP and Functional Programming, pages 198–207, 1984. Google ScholarDigital Library
- L. Maranget. Compiling pattern matching to good decision trees. In ML, pages 35–46. ACM, 2008. Google ScholarDigital Library
- C. McBride. How might effectful programs look? In Workshop on Effects and Type Theory, 2007. http://cs.ioc.ee/efftt/mcbride-slides.pdf.Google Scholar
- C. McBride. Kleisli arrows of outrageous fortune, 2011. Draft. https://personal.cis.strath.ac.uk/conor.mcbride/ Kleisli.pdf.Google Scholar
- C. McBride. Frank (0.3), 2012. http://hackage.haskell.org/package/Frank.Google Scholar
- C. McBride. Turing-completeness totally free. In Hinze and Voigtländer {22}, pages 257–275.Google Scholar
- C. McBride. Shonky, 2016. https://github.com/pigworker/shonky.Google Scholar
- C. McBride and R. Paterson. Applicative programming with effects. J. Funct. Program., 18(1):1–13, 2008. Google ScholarDigital Library
- G. Morrisett and T. Uustalu, editors. ICFP, 2013. ACM.Google Scholar
- B. C. Pierce and D. N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1–44, 2000. Google ScholarDigital Library
- G. D. Plotkin and J. Power. Semantics for algebraic operations. Electr. Notes Theor. Comput. Sci., 45:332–345, 2001.Google ScholarCross Ref
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- G. D. Plotkin and J. Power. Algebraic operations and generic effects. Appl. Categ. Structures, 11(1):69–94, 2003.Google ScholarCross Ref
- G. D. Plotkin and M. Pretnar. Handling algebraic effects. Logical Methods in Computer Science, 9(4), 2013.Google Scholar
- M. Pretnar. Inferring algebraic effects. Logical Methods in Computer Science, 10(3), 2014.Google Scholar
- 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 ScholarDigital Library
- T. Schrijvers, M. Pir`og, N. Wu, and M. Jaskelioff. Monad transformers and modular algebraic effects. Technical report, University of Leuven, 2016.Google Scholar
- 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 ScholarDigital Library
- N. Swamy, N. Guts, D. Leijen, and M. Hicks. Lightweight monadic programming in ML. In Chakravarty et al. {9}, pages 15–27. Google ScholarDigital Library
- W. Swierstra. Data types à la carte. J. Funct. Program., 18(4):423– 436, 2008. Google ScholarDigital Library
- W. Swierstra, editor. Haskell, 2014. ACM.Google Scholar
- J. Talpin and P. Jouvelot. The type and effect discipline. Inf. Comput., 111(2):245–296, 1994. Google ScholarDigital Library
- A. van der Ploeg and O. Kiselyov. Reflection without remorse: revealing a hidden sequence to speed up monadic reflection. In SwierstraGoogle Scholar
- , pages 133–144.Google Scholar
- K. Vonnegut. Deadeye Dick. Delacorte Press, 1982.Google Scholar
- P. Wadler. The essence of functional programming. In R. Sethi, editor, POPL, pages 1–14. ACM, 1992. Google ScholarDigital Library
- P. Wadler and S. Blott. How to make ad-hoc polymorphism less adhoc. In POPL, pages 60–76. ACM, 1989. Google ScholarDigital Library
- N. Wu and T. Schrijvers. Fusion for free - efficient algebraic effect handlers. In Hinze and Voigtländer {22}, pages 302–322.Google Scholar
Index Terms
- Do be do be do
Recommendations
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 ...
Do be do be do
POPL '17We 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 ...
Algebraic effects and effect handlers for idioms and arrows
WGP '14: Proceedings of the 10th ACM SIGPLAN workshop on Generic programmingPlotkin 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