{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:21Z","timestamp":1776891441149,"version":"3.51.2"},"reference-count":113,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2017,1,24]],"date-time":"2017-01-24T00:00:00Z","timestamp":1485216000000},"content-version":"unspecified","delay-in-days":23,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present a straightforward, sound, Hindley\u2013Milner 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\u2013Milner 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.<\/jats:p>","DOI":"10.1017\/s0956796816000320","type":"journal-article","created":{"date-parts":[[2017,1,24]],"date-time":"2017-01-24T04:27:51Z","timestamp":1485232071000},"source":"Crossref","is-referenced-by-count":21,"title":["No value restriction is needed for algebraic effects and handlers"],"prefix":"10.46298","volume":"27","author":[{"given":"OHAD","family":"KAMMAR","sequence":"first","affiliation":[]},{"given":"MATIJA","family":"PRETNAR","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2017,1,24]]},"reference":[{"key":"S0956796816000320_ref104","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"S0956796816000320_ref95","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"S0956796816000320_ref96","doi-asserted-by":"publisher","DOI":"10.1145\/143165"},{"key":"S0956796816000320_ref85","unstructured":"Pretnar M. (2010) Logic and Handling of Algebraic Effects. Ph.D. thesis, University of Edinburgh, UK."},{"key":"S0956796816000320_ref81","first-page":"342","volume-title":"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","author":"Plotkin","year":"2002"},{"key":"S0956796816000320_ref43","first-page":"349","volume-title":"Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012","author":"Kammar","year":"2012"},{"key":"S0956796816000320_ref42","unstructured":"Kammar O. (2014) An Algebraic Theory of Type-and-Effect Systems. Ph.D. Thesis, University of Edinburgh, UK."},{"key":"S0956796816000320_ref22","first-page":"1","volume-title":"CSL-LICS","author":"Fiore","year":"2014"},{"key":"S0956796816000320_ref61","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010020917337"},{"key":"S0956796816000320_ref52","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"S0956796816000320_ref69","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0956796816000320_ref4","unstructured":"Appel A. W. & MacQueen D. B. (1991) Standard ML of New Jersey. In PLILP, pp. 1\u201313."},{"key":"S0956796816000320_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019463"},{"key":"S0956796816000320_ref105","first-page":"97","volume-title":"Proceedings of the 2nd International Workshop on Types in Compilation, TIC '98","author":"Tolmach","year":"1998"},{"key":"S0956796816000320_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289435"},{"key":"S0956796816000320_ref97","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9010-4"},{"key":"S0956796816000320_ref49","first-page":"223","volume-title":"Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, TLCA 2007","author":"Kiselyov","year":"2007"},{"key":"S0956796816000320_ref47","unstructured":"Kiselyov O. (2015) Generating Code with Polymorphic Let. Technical Report, Tohoku University, Japan. Extended abstract submitted to the ACM SIGPLAN Workshop on ML."},{"key":"S0956796816000320_ref41","first-page":"239","volume-title":"Proceedings of Functional and Logic Programming, 9th International Symposium, FLOPS 2008","author":"Kameyama","year":"2008"},{"key":"S0956796816000320_ref25","first-page":"196","volume-title":"FLOPS","author":"Garrigue","year":"2004"},{"key":"S0956796816000320_ref16","unstructured":"Danvy O. & Filinski A. (1989) A Functional Abstraction of Typed Contexts. Technical Report 89\/12. DIKU."},{"key":"S0956796816000320_ref106","first-page":"1","volume-title":"Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '92)","author":"Wadler","year":"1992"},{"key":"S0956796816000320_ref80","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0956796816000320_ref107","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"},{"key":"S0956796816000320_ref37","first-page":"131","volume-title":"Conference Record of the 18th Annual ACM Symposium on Principles of Programming Languages","author":"Harper","year":"1991"},{"key":"S0956796816000320_ref30","volume-title":"Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Paris","author":"Gordon","year":"2017"},{"key":"S0956796816000320_ref28","unstructured":"Gifford D. K. & Lucassen J. M. (1986) Integrating functional and imperative programming. In LISP and Functional Programming, pp. 28\u201338."},{"key":"S0956796816000320_ref26","first-page":"360","volume-title":"Proceedings of the 8th Asian Symposium on Programming Languages and Systems, APLAS 2010","author":"Garrigue","year":"2010"},{"key":"S0956796816000320_ref79","unstructured":"Pitts A. M. (2011\u20132016) Types. Lecture notes, University of Cambridge Computer Laboratory."},{"key":"S0956796816000320_ref17","doi-asserted-by":"crossref","unstructured":"Danvy O. & Filinski A. (1990) Abstracting control. In LISP and Functional Programming. pp. 151\u2013160.","DOI":"10.1145\/91556.91622"},{"key":"S0956796816000320_ref46","first-page":"633","volume-title":"Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14","author":"Katsumata","year":"2014"},{"key":"S0956796816000320_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.007"},{"key":"S0956796816000320_ref101","first-page":"519","volume-title":"LICS","author":"Staton","year":"2013"},{"key":"S0956796816000320_ref113","first-page":"15","volume-title":"Proceedings of the 3rd ACM Workshop on Programming Languages meets Program Verification, PLPV 2009","author":"Zeilberger","year":"2009"},{"key":"S0956796816000320_ref78","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796816000320_ref110","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"S0956796816000320_ref70","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0956796816000320_ref10","first-page":"18","volume-title":"Proceedings of the 15th International Symposium on Trends in Functional Programming, TFP 2014","author":"Brady","year":"2014"},{"key":"S0956796816000320_ref15","unstructured":"Danvy O. (2006) An Analytical Approach to Programs as Data oObjects. DSc dissertation, Department of Computer Science, University of Aarhus."},{"key":"S0956796816000320_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159808"},{"key":"S0956796816000320_ref75","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143200"},{"key":"S0956796816000320_ref53","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"S0956796816000320_ref57","first-page":"220","volume-title":"POPL","author":"Leroy","year":"1993"},{"key":"S0956796816000320_ref68","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08918-8_23","volume-title":"Proceedings of Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014","author":"Melli\u00e8s","year":"2014"},{"key":"S0956796816000320_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"S0956796816000320_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934509"},{"key":"S0956796816000320_ref44","first-page":"145","volume-title":"ICFP","author":"Kammar","year":"2013"},{"key":"S0956796816000320_ref60","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"S0956796816000320_ref83","first-page":"118","volume-title":"Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24\u201327 June 2008","author":"Plotkin","year":"2008"},{"key":"S0956796816000320_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"S0956796816000320_ref23","doi-asserted-by":"crossref","unstructured":"Forster Y. , Kammar O. , Lindley S. & Pretnar M. (2016) On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. arXiv:1610.09161 [cs.LO].","DOI":"10.1145\/3110257"},{"key":"S0956796816000320_ref18","first-page":"180","volume-title":"Conference Record of the 15th Annual ACM Symposium on Principles of Programming Languages","author":"Felleisen","year":"1988"},{"key":"S0956796816000320_ref94","unstructured":"Saleh A. H. & Schrijvers T. (2016) Efficient algebraic effect handlers for prolog. Corr abs\/1608.00816."},{"key":"S0956796816000320_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_99"},{"key":"S0956796816000320_ref2","first-page":"36","volume-title":"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","author":"Ahman","year":"2016"},{"key":"S0956796816000320_ref77","first-page":"202","volume-title":"CADE","author":"Pfenning","year":"1999"},{"key":"S0956796816000320_ref92","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_7"},{"key":"S0956796816000320_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224173"},{"key":"S0956796816000320_ref65","first-page":"47","volume-title":"POPL","author":"Lucassen","year":"1988"},{"key":"S0956796816000320_ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_30"},{"key":"S0956796816000320_ref102","first-page":"395","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015","author":"Staton","year":"2015"},{"key":"S0956796816000320_ref82","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"S0956796816000320_ref55","first-page":"476","volume-title":"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","author":"Lepigre","year":"2016"},{"key":"S0956796816000320_ref109","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00047-5"},{"key":"S0956796816000320_ref111","first-page":"302","volume-title":"Proceedings of the 12th International Conference on Mathematics of Program Construction, MPC 2015","author":"Wu","year":"2015"},{"key":"S0956796816000320_ref51","first-page":"59","volume-title":"Haskell","author":"Kiselyov","year":"2013"},{"key":"S0956796816000320_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"S0956796816000320_ref90","unstructured":"R\u00e9my D. (2015) Type Systems. Lecture notes, Parisian Master of Research in Computer Science."},{"key":"S0956796816000320_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"S0956796816000320_ref74","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99393"},{"key":"S0956796816000320_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"key":"S0956796816000320_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"S0956796816000320_ref76","doi-asserted-by":"publisher","DOI":"10.1145\/218570.218572"},{"key":"S0956796816000320_ref33","first-page":"317","volume-title":"Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic","author":"Hancock","year":"2000"},{"key":"S0956796816000320_ref87","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"S0956796816000320_ref103","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"S0956796816000320_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.014"},{"key":"S0956796816000320_ref66","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/1481861.1481868","volume-title":"Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009","author":"Marino","year":"2009"},{"key":"S0956796816000320_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169696"},{"key":"S0956796816000320_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000049"},{"key":"S0956796816000320_ref1","unstructured":"Ahman D. (2015) Refinement types for algebraic effects (2015). In: Abstracts of the 21st Meeting \u2018Types for Proofs and Programs\u2019 (TYPES), Institute of Cybernetics, Tallinn University of Technology, pp. 10\u201311."},{"key":"S0956796816000320_ref5","first-page":"239","volume-title":"APLAS","author":"Asai","year":"2007"},{"key":"S0956796816000320_ref93","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1145\/1596550.1596596","volume-title":"Proceeding of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009","author":"Rompf","year":"2009"},{"key":"S0956796816000320_ref64","first-page":"95","volume-title":"Proceedings of the 7th Asian Symposium on Programming Languages and Systems, APLAS 2009","author":"Lippmeier","year":"2009"},{"key":"S0956796816000320_ref6","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"S0956796816000320_ref58","first-page":"291","volume-title":"POPL","author":"Leroy","year":"1991"},{"key":"S0956796816000320_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000066"},{"key":"S0956796816000320_ref108","first-page":"37","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS '87)","author":"Wand","year":"1987"},{"key":"S0956796816000320_ref98","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.103"},{"key":"S0956796816000320_ref14","first-page":"266","volume-title":"Proceedings of the 5th International Symposium on Formal Methods for Components and Objects, FMCO 2006","author":"Cooper","year":"2006"},{"key":"S0956796816000320_ref59","volume-title":"Call-by-Push-Value: A Functional\/Imperative Synthesis","author":"Levy","year":"2004"},{"key":"S0956796816000320_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"S0956796816000320_ref62","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103798"},{"key":"S0956796816000320_ref63","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"S0956796816000320_ref73","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-48092-7_6","volume-title":"Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the Occasion of his Retirement from his Professorship at the University of Kiel)","author":"Nielson","year":"1999"},{"key":"S0956796816000320_ref56","unstructured":"Leroy X. (1992) Typage Polymorphe D'un Langage Algorithmique. PhD Thesis (in French), Universit\u00e9 Paris 7."},{"key":"S0956796816000320_ref84","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"S0956796816000320_ref71","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010087314987"},{"key":"S0956796816000320_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"S0956796816000320_ref11","first-page":"431","volume-title":"Formal Description of Programming Concepts","author":"Cardelli","year":"1991"},{"key":"S0956796816000320_ref91","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0956796816000320_ref88","unstructured":"R\u00e9my D. (1990) Alg\u00e8bres touffues. application au typage polymorphe des objets enregistrements dans les langages fonctionnels. Th\u00e8se de doctorat, Universit\u00e9 de Paris 7."},{"key":"S0956796816000320_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"S0956796816000320_ref20","doi-asserted-by":"crossref","unstructured":"Felleisen M. , Wand M. , Friedman D. P. & Duba B. F. (1988) Abstract continuations: A mathematical semantics for handling full jumps. In LISP and Functional Programming, pp. 52\u201362.","DOI":"10.1145\/62678.62684"},{"key":"S0956796816000320_ref86","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:21)2014"},{"key":"S0956796816000320_ref34","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1145\/158511.158630","volume-title":"Conference Record of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Harper","year":"1993"},{"key":"S0956796816000320_ref24","first-page":"329","volume-title":"Proceedings of the 2nd Asian Workshop on Programming Languages and Systems, APLAS'01, Korea Advanced Institute of Science and Technology","author":"Garrigue","year":"2001"},{"key":"S0956796816000320_ref29","unstructured":"Girard J.-Y. (1972) (June) Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arith-m\u00e9tique d'ordre sup\u00e9rieur. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 Paris VII."},{"key":"S0956796816000320_ref99","first-page":"48","volume-title":"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","author":"Staton","year":"2010"},{"key":"S0956796816000320_ref67","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.46"},{"key":"S0956796816000320_ref100","first-page":"401","volume-title":"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","author":"Staton","year":"2013"},{"key":"S0956796816000320_ref112","first-page":"1","volume-title":"Haskell","author":"Wu","year":"2014"},{"key":"S0956796816000320_ref89","unstructured":"R\u00e9my D. 1991 (May) Type Inference for Records in a Natural Extension of ML. Research Report 1431. Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:53Z","timestamp":1776889193000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000320\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":113,"alternative-id":["S0956796816000320"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000320","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e7"}}