{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:01:48Z","timestamp":1770285708720,"version":"3.49.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,8,2]]},"abstract":"<jats:p>The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. 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 signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.<\/jats:p>","DOI":"10.1145\/3408999","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Signature restriction for polymorphic algebraic effects"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan \/ SOKENDAI, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[{"name":"Kyoto University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54444-5_83"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_16"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_2_8_1","volume-title":"A Scheme for a Higher-Level Semantic Algebra","author":"Clinger William D."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236764"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89719-6_6"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863566"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706354"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000121"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_15"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224173"},{"key":"e_1_2_2_21_1","unstructured":"Robert Harper and Mark Lillibridge. 1991. ML with callcc is unsound. Announcement on the types electronic forum. https:\/\/www.cis.upenn.edu\/~bcpierce\/types\/archives\/1991\/msg00034.html  Robert Harper and Mark Lillibridge. 1991. ML with callcc is unsound. Announcement on the types electronic forum. https:\/\/www.cis.upenn.edu\/~bcpierce\/types\/archives\/1991\/msg00034.html"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158630"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019463"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287604"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000320"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017. 486-499","author":"Leijen Daan","year":"2017"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567077"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99622"},{"key":"e_1_2_2_30_1","unstructured":"Paul Blain Levy. 2001. Call-by-push-value. Ph.D. Dissertation. Queen Mary University of London UK. http:\/\/ethos.bl.uk\/ OrderDetails.do?uin=uk. bl.ethos.369233  Paul Blain Levy. 2001. Call-by-push-value. Ph.D. Dissertation. Queen Mary University of London UK. http:\/\/ethos.bl.uk\/ OrderDetails.do?uin=uk. bl.ethos.369233"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","volume-title":"The Definition of Standard ML","author":"Milner Robin","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_2_39_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_2_44_1","volume-title":"Abstraction and Parametric Polymorphism. In IFIP Congress. 513-523","author":"Reynolds John C.","year":"1983"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009875"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_13"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155104"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561306"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316068"},{"key":"e_1_2_2_53_1","doi-asserted-by":"crossref","unstructured":"Andrew K. Wright. 1995. Simple Imperative Polymorphism. Lisp and Symbolic Computation 8 4 ( 1995 ) 343-355.  Andrew K. Wright. 1995. Simple Imperative Polymorphism. Lisp and Symbolic Computation 8 4 ( 1995 ) 343-355.","DOI":"10.1007\/BF01018828"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408999","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408999","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408999"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":54,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408999"],"URL":"https:\/\/doi.org\/10.1145\/3408999","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}