{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:06:05Z","timestamp":1779836765385,"version":"3.53.1"},"reference-count":64,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:00:00Z","timestamp":1716768000000},"content-version":"unspecified","delay-in-days":147,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. In the literature, there are two kinds of approaches to this problem: one is to restrict how effects are triggered and the other is to restrict how they are implemented. This work explores a new approach to ensuring the safety of the use of polymorphic effects in polymorphic type assignment. A novelty of our work is to restrict\n                    <jats:italic>effect interfaces<\/jats:italic>\n                    . To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose\n                    <jats:italic>signature restriction<\/jats:italic>\n                    , a new notion to restrict the type signatures of operations and show that signature restriction ensures type safety of a language equipped with polymorphic effects and unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both of the operations that satisfy and those that do not satisfy the signature restriction in a single program.\n                  <\/jats:p>","DOI":"10.1017\/s0956796824000054","type":"journal-article","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T07:17:42Z","timestamp":1716794262000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Signature restriction for polymorphic algebraic effects"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"TARO","family":"SEKIYAMA","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"TAKESHI","family":"TSUKADA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"ATSUSHI","family":"IGARASHI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2024,5,27]]},"reference":[{"key":"S0956796824000054_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863566"},{"key":"S0956796824000054_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000320"},{"key":"S0956796824000054_ref7","first-page":"1","article-title":"Binders by day, labels by night: effect instances via lexically scoped handlers","volume":"4","author":"Biernacki","year":"2020","journal-title":"PACMPL."},{"key":"S0956796824000054_ref45","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"S0956796824000054_ref55","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155104"},{"key":"S0956796824000054_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567077"},{"key":"S0956796824000054_ref61","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316068"},{"key":"S0956796824000054_ref20","unstructured":"Girard, J. Y. (1972) Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de doctorat d\u2019\u00e9tat. Universit\u00e9 Paris 7."},{"key":"S0956796824000054_ref44","unstructured":"Pitts, A. & Stark, I. (1998) Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics, Gordon, A. & Pitts, A. (eds). Publications of the Newton Institute, Cambridge University Press, pp. 227\u2013273. Available at: http:\/\/www.inf.ed.ac.uk\/ stark\/operfl.html."},{"key":"S0956796824000054_ref10","first-page":"1","article-title":"Handling delimited continuations with dependent types","volume":"2","author":"Cong","year":"2018","journal-title":"PACMPL."},{"key":"S0956796824000054_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158630"},{"key":"S0956796824000054_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000121"},{"key":"S0956796824000054_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"S0956796824000054_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224173"},{"key":"S0956796824000054_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"S0956796824000054_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_15"},{"key":"S0956796824000054_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0956796824000054_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706354"},{"key":"S0956796824000054_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"S0956796824000054_ref13","doi-asserted-by":"crossref","unstructured":"Dolan, S. , Eliopoulos, S. , Hillerstr\u00f6m, D. , Madhavapeddy, A. , Sivaramakrishnan, K. C. & White, L. (2017) Concurrent system programming with effect handlers. In Trends in Functional Programming - 18th International Symposium, TFP 2017, Revised Selected Papers, pp. 98\u2013117.","DOI":"10.1007\/978-3-319-89719-6_6"},{"key":"S0956796824000054_ref1","unstructured":"Ahman, D. (2017) Fibred Computational Effects. Ph.D. thesis. University of Edinburgh."},{"key":"S0956796824000054_ref38","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S0956796824000054_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"S0956796824000054_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"S0956796824000054_ref34","unstructured":"Levy, P. B. (2001) Call-by-push-value. Ph.D. thesis. Queen Mary University of London, UK."},{"key":"S0956796824000054_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"S0956796824000054_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"S0956796824000054_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_13"},{"key":"S0956796824000054_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"S0956796824000054_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54444-5_83"},{"key":"S0956796824000054_ref57","unstructured":"The Links team. (2022) The Links programming langauge https:\/\/links-lang.org\/."},{"key":"S0956796824000054_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"S0956796824000054_ref5","article-title":"An effect system for algebraic effects and handlers","volume":"10","author":"Bauer","year":"2014","journal-title":"Log. Methods Comput. Sci."},{"key":"S0956796824000054_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"S0956796824000054_ref46","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"S0956796824000054_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009875"},{"key":"S0956796824000054_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"S0956796824000054_ref36","unstructured":"Lindley, S. , McBride, C. , McLaughlin, C. & Convent, L. (2022) The Frank programming langauge https:\/\/github.com\/frank-lang\/frank."},{"key":"S0956796824000054_ref62","first-page":"343","article-title":"Simple imperative polymorphism","volume":"8","author":"Wright","year":"1995","journal-title":"Lisp Symb. Comput."},{"key":"S0956796824000054_ref63","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796824000054_ref9","unstructured":"Clinger, W. D. , Friedman, D. P. & Wand, M. (1985) A scheme for a higher-level semantic algebra. In Algebraic Methods in Semantics, Nivat, M. & Reynolds, J. C. (eds), chapter 6, Cambridge University Press, pp. 237\u2013250."},{"key":"S0956796824000054_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_16"},{"key":"S0956796824000054_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"S0956796824000054_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0956796824000054_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0956796824000054_ref48","article-title":"Handling algebraic effects","volume":"9","author":"Plotkin","year":"2013","journal-title":"Logical Methods in Computer Science."},{"key":"S0956796824000054_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"S0956796824000054_ref30","unstructured":"Leijen, D. (2023) The Koka programming langauge. https:\/\/koka-lang.github.io\/koka\/doc\/index.html."},{"key":"S0956796824000054_ref50","unstructured":"Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism. In IFIP Congress, pp. 513\u2013523."},{"key":"S0956796824000054_ref60","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"S0956796824000054_ref25","first-page":"361","article-title":"Polymorphic type assignment and CPS conversion","volume":"6","author":"Harper","year":"1993","journal-title":"Lisp Symb. Comput."},{"key":"S0956796824000054_ref56","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"S0956796824000054_ref59","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"S0956796824000054_ref64","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"S0956796824000054_ref26","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287604"},{"key":"S0956796824000054_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99622"},{"key":"S0956796824000054_ref32","unstructured":"Leroy, X. , Doligez, D. , Frisch, A. , Garrigue, J. , R\u00e9my, D. & Vouillon, J. (2020) The OCaml system release 4.10: Documentation and user\u2019s manua."},{"key":"S0956796824000054_ref23","unstructured":"Harper, R. & Lillibridge, M. (1991) ML with callcc is unsound. Announcement on the Types Electronic Forum."},{"key":"S0956796824000054_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"S0956796824000054_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/3408999"},{"key":"S0956796824000054_ref58","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561306"},{"key":"S0956796824000054_ref41","first-page":"1","article-title":"The fire triangle: how to mix substitution, dependent elimination, and effects","volume":"4","author":"P\u00e9drot","year":"2020","journal-title":"PACMPL."},{"key":"S0956796824000054_ref53","doi-asserted-by":"publisher","DOI":"10.1145\/3473600"},{"key":"S0956796824000054_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796824000054","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:37:03Z","timestamp":1779835023000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796824000054\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"references-count":64,"alternative-id":["S0956796824000054"],"URL":"https:\/\/doi.org\/10.1017\/s0956796824000054","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e7"}}