{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:04:20Z","timestamp":1760043860129,"version":"3.40.5"},"reference-count":41,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2020,6,8]],"date-time":"2020-06-08T00:00:00Z","timestamp":1591574400000},"content-version":"unspecified","delay-in-days":159,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effect-aware optimising compiler could be built. Unfortunately, in our experience, implementing optimisations for Eff is overly error-prone because its core language is implicitly typed, making code transformations very fragile. To remedy this, we present an explicitly typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations. Our typing-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content. Additionally, we present a monadic translation from our calculus into a pure language without algebraic effects or handlers, using the effect information to introduce monadic constructs only where necessary.<\/jats:p>","DOI":"10.1017\/s0956796820000131","type":"journal-article","created":{"date-parts":[[2020,6,8]],"date-time":"2020-06-08T09:56:00Z","timestamp":1591610160000},"source":"Crossref","is-referenced-by-count":5,"title":["Explicit effect subtyping"],"prefix":"10.1017","volume":"30","author":[{"given":"GEORGIOS","family":"KARACHALIAS","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7755-2303","authenticated-orcid":false,"given":"MATIJA","family":"PRETNAR","sequence":"additional","affiliation":[]},{"given":"AMR HANY","family":"SALEH","sequence":"additional","affiliation":[]},{"given":"STIEN","family":"VANDERHALLEN","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8771-5559","authenticated-orcid":false,"given":"TOM","family":"SCHRIJVERS","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2020,6,8]]},"reference":[{"doi-asserted-by":"publisher","key":"S0956796820000131_ref41","DOI":"10.1145\/292540.292545"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref38","DOI":"10.1007\/978-3-540-40018-9_19"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref37","DOI":"10.1145\/1411204.1411215"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref34","DOI":"10.1007\/3-540-06859-7_148"},{"unstructured":"Pretnar, M. , Saleh, A. H. , Faes, A. & Schrijvers, T. (2017) Efficient Compilation of Algebraic Effects and Handlers. Technical report. CW 708. KU Leuven Department of Computer Science.","key":"S0956796820000131_ref33"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref32","DOI":"10.1016\/j.entcs.2015.12.003"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref28","DOI":"10.1023\/A:1023064908962"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref30","DOI":"10.1006\/inco.2001.2963"},{"unstructured":"Peyton Jones, S. , Vytiniotis, D. , Weirich, S. & Washburn, G. (2006) Simple unification-based type inference for GADTs. In ICFP\u201906.","key":"S0956796820000131_ref27"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref26","DOI":"10.1145\/2951913.2951945"},{"unstructured":"Jr, Morris ., J. H. (1969) Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology.","key":"S0956796820000131_ref25"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref24","DOI":"10.1145\/800017.800529"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref23","DOI":"10.1016\/0022-0000(78)90014-4"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref7","DOI":"10.1145\/351240.351247"},{"unstructured":"Barendregt, H. (1981) The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland.","key":"S0956796820000131_ref1"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref40","DOI":"10.1007\/978-3-642-25318-8_10"},{"unstructured":"Dolan, S. , White, L. , Sivaramakrishnan, K. C. , Yallop, J. & Madhavapeddy, A. (2015) Effective concurrency through algebraic effects. In OCaml Workshop.","key":"S0956796820000131_ref9"},{"unstructured":"Bi, X. , Oliveira, B. C. d. S. & Schrijvers, T. (2018) The essence of nested composition. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16\u201321, 2018, Amsterdam, The Netherlands, Millstein, T. D. (ed). LIPIcs, vol. 109. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 22:1\u201322:33.","key":"S0956796820000131_ref4"},{"unstructured":"Girard, J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de larithm\u00e9tique dordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII.","key":"S0956796820000131_ref11"},{"volume-title":"Proofs and Types","year":"1989","author":"Girard","key":"S0956796820000131_ref12"},{"key":"S0956796820000131_ref2","first-page":"44","article-title":"From theory to practice of algebraic effects and handlers (dagstuhl seminar 16112)","volume":"6","author":"Bauer","year":"2016","journal-title":"Dagstuhl Reports"},{"key":"S0956796820000131_ref6","first-page":"104","article-title":"Algebraic effect handlers go mainstream (dagstuhl seminar 18172)","volume":"8","author":"Chandrasekaran","year":"2018","journal-title":"Dagstuhl Reports"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref10","DOI":"10.1016\/0304-3975(90)90144-7"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref8","DOI":"10.1145\/582153.582176"},{"key":"S0956796820000131_ref3","first-page":"108","article-title":"Programming with algebraic effects and handlers","volume":"84","author":"Bauer","year":"2015","journal-title":"J. Log. Alg. Program."},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref18","DOI":"10.1145\/2500365.2500590"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref39","DOI":"10.1145\/1190315.1190324"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref31","DOI":"10.2168\/LMCS-10(3:21)2014"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref13","DOI":"10.1016\/0167-6423(94)00004-2"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref14","DOI":"10.1145\/2976022.2976033"},{"unstructured":"Reynolds, J. C. (1983) Types, abstraction, and parametric polymorphism. In Information Processing, Mason, R.E.A. (ed), vol. 83, pp. 513\u2013523.","key":"S0956796820000131_ref35"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref17","DOI":"10.1007\/3-540-55253-7_17"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref29","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"S0956796820000131_ref15","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley","year":"1969","journal-title":"Trans. Am. Math. Soc."},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref5","DOI":"10.1016\/0890-5401(91)90055-7"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref16","DOI":"10.1145\/503502.503505"},{"key":"S0956796820000131_ref36","first-page":"327","article-title":"Explicit effect subtyping","volume":"10801","author":"Saleh","year":"2018","journal-title":"Computer Science"},{"unstructured":"Kiselyov, O. & Sivaramakrishnan, K. C. (2016) Eff directly in OCaml. In OCaml Workshop.","key":"S0956796820000131_ref19"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref22","DOI":"10.1145\/3009837.3009897"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref20","DOI":"10.4204\/EPTCS.153.8"},{"doi-asserted-by":"publisher","key":"S0956796820000131_ref21","DOI":"10.1145\/3009837.3009872"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796820000131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,8]],"date-time":"2020-06-08T09:56:07Z","timestamp":1591610167000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796820000131\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":41,"alternative-id":["S0956796820000131"],"URL":"https:\/\/doi.org\/10.1017\/s0956796820000131","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"type":"print","value":"0956-7968"},{"type":"electronic","value":"1469-7653"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e15"}}