×

zbMATH — the first resource for mathematics

No value restriction is needed for algebraic effects and handlers. (English) Zbl 1418.68034
Summary: We present a straightforward, sound, Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that the soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and that many programming examples can be recast to use effect handlers instead of these effects. After presenting the calculus and its soundness proof, formalised in Twelf, we analyse the expressive power of effect handlers with respect to state effects. We conjecture handlers alone cannot express reference cells, but show they can simulate dynamically scoped state, establishing that dynamic binding also does not need a value restriction.

MSC:
68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
Eff; Links; ML; Twelf
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ahman, D., (2015)
[2] Ahman, D.; Ghani, N.; Plotkin, G. D.; Jacobs, B.; Löding, C., Proceedings of the 19th International Conference, Foundations of Software Science and Computation Structures - FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Dependent types and fibred computational effects, 36-54, (2016), Berlin: Springer, Berlin
[3] Ahman, D.; Staton, S., Normalization by evaluation and algebraic effects., Electr. Notes Theor. Comput. Sci., 298, 51-69, (2013) · Zbl 1334.68046
[4] Appel, A. W.; Macqueen, D. B., (1991)
[5] Asai, K.; Kameyama, Y., APLAS, Polymorphic delimited continuations, 239-254, (2007), Springer · Zbl 1137.68344
[6] Bauer, A.; Pretnar, M., An effect system for algebraic effects and handlers., Log. Methods Comput. Sci., 10, 1-29, (2014) · Zbl 1448.68203
[7] Bauer, A.; Pretnar, M., Programming with algebraic effects and handlers., J. Log. Algebr. Meth. Program., 84, 108-123, (2015) · Zbl 1304.68025
[8] Benton, N.; Kennedy, A.; Russell, G.; Felleisen, M.; Hudak, P.; Queinnec, C., Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Compiling standard ML to java bytecodes, 129-140, (1998), ACM
[9] Brady, E.; Morrisett, G.; Uustalu, T., Proceedings of ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Programming and reasoning with algebraic effects and dependent types, 133-144, (2013), ACM
[10] Brady, E.; Hage, J.; Mccarthy, J., Proceedings of the 15th International Symposium on Trends in Functional Programming, TFP 2014, Resource-dependent algebraic effects, 18-33, (2014), Berlin: Springer, Berlin
[11] Cardelli, L.; Neuhold, E. J.; Paul, M., Formal Description of Programming Concepts, Typeful programming, 431-507, (1991), Berlin: Springer-Verlag, Berlin
[12] Cardelli, L.; Mitchell, J. C., Operations on records., Math. Struct. Comput. Sci., 1, 3-48, (1991) · Zbl 0727.68020
[13] Cartwright, R.; Felleisen, M.; Hagiya, M.; Mitchell, J. C., Proceedings of International Conference TACS ’94 on Theoretical Aspects of Computer Software, Extensible denotational language specifications., 244-272, (1994), Springer
[14] Cooper, E.; Lindley, S.; Wadler, P.; Yallop, J.; De Boer, F. S.; Bonsangue, M. M.; Graf, S.; De Roever, W. P., Proceedings of the 5th International Symposium on Formal Methods for Components and Objects, FMCO 2006, Links: Web programming without tiers., 266-296, (2006), Springer
[15] Danvy, O., (2006)
[16] Danvy, O.; Filinski, A., (1989)
[17] Danvy, O.; Filinski, A., (1990)
[18] Felleisen, M.; Ferrante, J.; Mager, P., Conference Record of the 15th Annual ACM Symposium on Principles of Programming Languages, The theory and practice of first-class prompts., 180-190, (1988), ACM Press
[19] Felleisen, M., On the expressive power of programming languages., Sci. Comput. Program., 17, 35-75, (1991) · Zbl 0745.68033
[20] Felleisen, M.; Wand, M.; Friedman, D. P.; Duba, B. F., (1988)
[21] Filinski, A.; Boehm, H.-J.; Lang, B.; Yellin, D. M., Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Representing monads., 446-457, (1994), ACM Press
[22] Fiore, M. P.; Staton, S., CSL-LICS, Substitution, jumps, and algebraic effects., 1-10, (2014), ACM
[23] Forster, Y.; Kammar, O.; Lindley, S.; Pretnar, M., (2016)
[24] Garrigue, J., Proceedings of the 2nd Asian Workshop on Programming Languages and Systems, APLAS’01, Korea Advanced Institute of Science and Technology, Simple type inference for structural polymorphism., 329-343, (2001), Daejeon, Korea
[25] Garrigue, J., FLOPS, Relaxing the value restriction., 196-213, (2004), Berlin: Springer, Berlin · Zbl 1122.68398
[26] Garrigue, J.; Ueda, K., Proceedings of the 8th Asian Symposium on Programming Languages and Systems, APLAS 2010, A certified implementation of ML with structural polymorphism., 360-375, (2010), Springer
[27] Garrigue, J., A certified implementation of ML with structural polymorphism and recursive types., Math. Struct. Comput. Sci., 25, 867-891, (2015) · Zbl 1361.68038
[28] Gifford, D. K.; Lucassen, J. M., (1986)
[29] Girard, J.-Y., (1972)
[30] Gordon, A. D., Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Paris, (2017), ACM: ACM, New York, NY, USA · Zbl 1355.68012
[31] Gordon, M. J. C.; Milner, R.; Wadsworth, C. P., Edinburgh LCF, (1979), Berlin: Springer, Berlin
[32] Gunter, C. A.; Rémy, D.; Riecke, J. G., FPCA, A generalization of exceptions and control in ML-like languages., 12-23, (1995), ACM
[33] Hancock, P.; Setzer, A.; Clote, P.; Schwichtenberg, H., Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, Interactive programs in dependent type theory., 317-331, (2000), Springer · Zbl 0973.68041
[34] Harper, R.; Lillibridge, M.; Deusen, M. S. Van; Lang, B., Conference Record of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Explicit polymorphism and CPS conversion., 206-219, (1993), ACM Press
[35] Harper, R.; Lillibridge, M., Polymorphic type assignment and CPS conversion., Lisp Symbolic Comput., 6, 361-380, (1993)
[36] Harper, R.; Mitchell, J. C., On the type structure of standard ML., ACM Trans. Program. Lang. Syst., 15, 211-252, (1993)
[37] Harper, R.; Pierce, B. C.; Wise, D. S., Conference Record of the 18th Annual ACM Symposium on Principles of Programming Languages, A record calculus based on symmetric concatenation., 131-142, (1991), ACM Press
[38] Hillerström, D.; Lindley, S.; Chapman, J.; Swierstra, W., Proceedings of the 1st International Workshop on Type-Driven Development, September 2016, Liberating effects with rows and handlers., 15-27, (2016), ACM
[39] Hyland, M.; Plotkin, G. D.; Power, J., Combining effects: Sum and tensor., Theor. Comput. Sci., 357, 70-99, (2006) · Zbl 1096.68088
[40] Jaber, G.; Tzevelekos, N., Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16), Trace semantics for polymorphic references., 585-594, (2016), ACM: ACM, New York, NY, USA · Zbl 1401.68033
[41] Kameyama, Y.; Yonezawa, T.; Garrigue, J.; Hermenegildo, M. V., Proceedings of Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Typed dynamic control operators for delimited continuations., 239-254, (2008), Springer
[42] Kammar, O., (2014)
[43] Kammar, O.; Plotkin, G. D.; Field, J.; Hicks, M., Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Algebraic foundations for effect-dependent optimisations., 349-360, (2012), ACM · Zbl 1321.68200
[44] Kammar, O.; Lindley, S.; Oury, N., ICFP, Handlers in action., 145-158, (2013), ACM · Zbl 1323.68126
[45] Katsumata, S., Relating computational effects by ⊤⊤-lifting., Inf. Comput., 222, 228-246, (2013) · Zbl 1267.68087
[46] Katsumata, S.; Jagannathan, S.; Sewell, P., Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, Parametric effect monads and semantics of effect systems., 633-646, (2014), ACM
[47] Kiselyov, O., (2015)
[48] Kiselyov, O.; Ishii, H.; Lippmeier, B., Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Freer monads, more extensible effects., 94-105, (2015), ACM
[49] Kiselyov, O.; Shan, C.-C.; Rocca, S.; Ronchi, D., Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, TLCA 2007, A substructural type system for delimited continuations., 223-239, (2007), Springer · Zbl 1215.68124
[50] Kiselyov, O.; Shan, C.-C.; Sabry, A., ICFP, Delimited dynamic binding, 26-37, (2006), ACM · Zbl 1321.68128
[51] Kiselyov, O.; Sabry, A.; Swords, C., Haskell, Extensible effects: An alternative to monad transformers., 59-70, (2013), ACM
[52] Landin, P. J., The mechanical evaluation of expressions., Comput. J., 6, 308-320, (1964) · Zbl 0122.36106
[53] Leijen, D., (2014)
[54] Leijen, D., Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Type directed compilation of row-typed algebraic effects, 486-499, (2017), ACM: ACM, New York, NY, USA · Zbl 1380.68097
[55] Lepigre, R.; Thiemann, P., Proceedings of the 25th European Symposium on Programming, Programming Languages and Systems, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, A classical realizability model for a semantical value restriction., 476-502, (2016), Springer
[56] Leroy, X., (1992)
[57] Leroy, X., POPL, Polymorphism by name for references and continuations., 220-231, (1993), ACM Press
[58] Leroy, X.; Weis, P., POPL, Polymorphic type inference and assignment., 291-302, (1991), ACM Press
[59] Levy, P. B., Call-by-Push-Value: A Functional/Imperative Synthesis, (2004), Berlin: Springer, Berlin
[60] Levy, P. B.; Power, J.; Thielecke, H., Modelling environments in call-by-value programming languages., Inf. Comput., 185, 182-210, (2003) · Zbl 1069.68073
[61] Lillibridge, M., Unchecked exceptions can be strictly more powerful than call/cc., Higher-Order Symbol. Comput., 12, 75-104, (1999) · Zbl 0935.68010
[62] Lindley, S.; Cheney, J., TLDI, Row-based effect types for database integration., 91-102, (2012), ACM
[63] Lindley, S.; Mcbride, C.; Mclaughlin, C.; Gordon, A. D., Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Do be do be do., 500-514, (2017), ACM: ACM, New York, NY, USA · Zbl 1380.68098
[64] Lippmeier, B.; Hu, Z., Proceedings of the 7th Asian Symposium on Programming Languages and Systems, APLAS 2009, Witnessing purity, constancy and mutability., 95-110, (2009), Springer
[65] Lucassen, J. M.; Gifford, D. K., POPL, Polymorphic effect systems., 47-57, (1988), ACM Press
[66] Marino, D.; Millstein, T. D.; Kennedy, A.; Ahmed, A., Proceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, A generic type-and-effect system., 39-50, (2009), ACM
[67] Melliès, P.-A., Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, Segal condition meets computational effects., 150-159, (2010), IEEE Computer Society
[68] Melliès, Paul-André.; Dowek, G., Proceedings of Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Local states in string diagrams., 334-348, (2014), Springer
[69] Milner, R., A theory of type polymorphism in programming., J. Comput. Syst. Sci., 17, 348-375, (1978) · Zbl 0388.68003
[70] Moggi, E., Notions of computation and monads., Inf. Comput., 93, 55-92, (1991) · Zbl 0723.68073
[71] Moreau, L., A syntactic theory of dynamic binding., Higher-order and Symbolic Computation, 11, 233-279, (1998) · Zbl 0934.68038
[72] Munch-Maccagnoni, G.; Grädel, E.; Kahle, R., Computer Science Logic ’09, Focalisation and classical realisability., 409-423, (2009), Heidelberg: Springer, Heidelberg · Zbl 1257.03055
[73] Nielson, F.; Nielson, H. R.; Olderog, E.-R.; Steffen, B., Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the Occasion of his Retirement from his Professorship at the University of Kiel), Type and effect systems., 114-136, (1999), Berlin: Springer, Berlin
[74] Ohori, A.; Stoy, J. E., Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture, FPCA 1989, A simple semantics for ML polymorphism., 281-292, (1989), ACM
[75] Ohori, A.; Sethi, R., Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’92), A compilation method for ML-style polymorphic record calculi., 154-165, (1992), ACM: ACM, New York, NY, USA
[76] Ohori, A., A polymorphic record calculus and its compilation., ACM Trans. Program. Lang. Syst., 17, 844-895, (1995)
[77] Pfenning, F.; Schürmann, C., CADE, System description: Twelf - A meta-logical framework for deductive systems., 202-206, (1999), Springer
[78] Pierce, B. C., Types and Programming Languages, (2002), Cambridge, MA, USA: MIT Press, Cambridge, MA, USA
[79] Pitts, A. M., (2011)
[80] Plotkin, G. D., LCF considered as a programming language., Theor. Comput. Sci., 5, 223-255, (1977) · Zbl 0369.68006
[81] Plotkin, G. D.; Power, J.; Nielsen, M.; Engberg, U., Proceedings of the 5th International Conference, Foundations of Software Science and Computation Structures, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Notions of computation determine monads., 342-356, (2002), Springer · Zbl 1077.68676
[82] Plotkin, G. D.; Power, J., Algebraic operations and generic effects., Appl. Categorical Struct., 11, 69-94, (2003) · Zbl 1023.18006
[83] Plotkin, G. D.; Pretnar, M., Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, A logic for algebraic effects., 118-129, (2008), Pittsburgh, PA, USA: IEEE Computer Society, Pittsburgh, PA, USA
[84] Plotkin, G. D.; Pretnar, M., Handling algebraic effects., Logical Methods in Comput. Sci., 9, (2013) · Zbl 1314.68191
[85] Pretnar, M., (2010)
[86] Pretnar, M., Inferring algebraic effects., Log. Methods Comput. Sci., 10, (2014) · Zbl 1341.68024
[87] Pretnar, M., An introduction to algebraic effects and handlers. invited tutorial paper., Electr. Notes Theor. Comput. Sci., 319, 19-35, (2015) · Zbl 1351.68079
[88] Rémy, D., (1990)
[89] Rémy, D., (1991)
[90] Rémy, D., (2015)
[91] Reynolds, J. C., Programming Symposium, Proceedings Colloque Sur La Programmation, Towards a theory of type structure., 408-423, (1974), London, UK: Springer-Verlag, London, UK
[92] Reynolds, J. C.; Kahn, G.; Macqueen, D. B.; Plotkin, G. D., Proceedings of Semantics of Data Types, International Symposium, Sophia-Antipolis, Polymorphism is not set-theoretic., 145-156, (1984), Springer
[93] Rompf, T.; Maier, I.; Odersky, M.; Hutton, G.; Tolmach, A. P., Proceeding of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009, Implementing first-class polymorphic delimited continuations by a type-directed selective cps-transform., 317-328, (2009), ACM · Zbl 1302.68187
[94] Saleh, A. H.; Schrijvers, T., (2016)
[95] Scott, D. S., A type-theoretical alternative to ISWIM, CUCH, OWHY., Theor. Comput. Sci., 121, 411-440, (1993) · Zbl 0942.68522
[96] Sethi, R., Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (1992), ACM: ACM, New York, NY, USA
[97] Shan, C.-C., A static simulation of dynamic delimited control., Higher-Order Symbol. Comput., 20, 371-401, (2007) · Zbl 1128.68010
[98] Staton, S., Two cotensors in one: Presentations of algebraic theories for local state and fresh names., Electr. Notes Theor. Comput. Sci., 249, 471-490, (2009) · Zbl 1338.18034
[99] Staton, S.; Ong, C.-H. Luke, Proceedings of 13th International Conference, Foundations of Software Science and Computational Structures, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Completeness for algebraic theories of local state., 48-63, (2010), Springer
[100] Staton, S.; Pfenning, F., Proceedings of 16th International Conference, Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, An algebraic presentation of predicate logic - (extended abstract)., 401-417, (2013), Springer
[101] Staton, S., LICS, Instances of computational effects: An algebraic perspective., 519, (2013), IEEE Computer Society · Zbl 1368.68183
[102] Staton, S.; Rajamani, S. K.; Walker, D., Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Algebraic effects, linearity, and quantum programming languages., 395-406, (2015), ACM · Zbl 1345.68137
[103] Swierstra, W., Data types à la carte., J. Funct. Program., 18, 423-436, (2008) · Zbl 1153.68015
[104] Tofte, M., Type inference for polymorphic references., Inf. Comput., 89, 1-34, (1990) · Zbl 0705.68028
[105] Tolmach, A. P.; Leroy, X.; Ohori, A., Proceedings of the 2nd International Workshop on Types in Compilation, TIC ’98, Optimizing ML using a hierarchy of monadic types., 97-115, (1998), Springer
[106] Wadler, P.; Sethi, R., Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’92), The essence of functional programming, 1-14, (1992), ACM: ACM, New York, NY, USA
[107] Wadler, P.; Thiemann, P., The marriage of effects and monads., ACM Trans. Comput. Log., 4, 1-32, (2003) · Zbl 1365.68166
[108] Wand, M., Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Complete type inference for simple objects., 37-44, (1987), IEEE Computer Society
[109] Wells, J. B., Typability and type checking in System F are equivalent and undecidable., Ann. Pure Appl. Logic, 98, 111-156, (1999) · Zbl 0932.03017
[110] Wright, A. K., Simple imperative polymorphism., Lisp Symbol. Comput., 8, 343-355, (1995)
[111] Wu, N.; Schrijvers, T.; Hinze, R.; Voigtländer, J., Proceedings of the 12th International Conference on Mathematics of Program Construction, MPC 2015, Fusion for free—efficient algebraic effect handlers., 302-322, (2015), Springer
[112] Wu, N.; Schrijvers, T.; Hinze, R., Haskell, Effect handlers in scope., 1-12, (2014), ACM
[113] Zeilberger, N.; Altenkirch, T.; Millstein, T. D., Proceedings of the 3rd ACM Workshop on Programming Languages meets Program Verification, PLPV 2009, Refinement types and computational duality., 15-26, (2009), ACM
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.