{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:57Z","timestamp":1779836757523,"version":"3.53.1"},"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                  <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-08T05:56:00Z","timestamp":1591595760000},"source":"Crossref","is-referenced-by-count":5,"title":["Explicit effect subtyping"],"prefix":"10.1017","volume":"30","author":[{"given":"GEORGIOS","family":"KARACHALIAS","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7755-2303","authenticated-orcid":false,"given":"MATIJA","family":"PRETNAR","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"AMR HANY","family":"SALEH","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"STIEN","family":"VANDERHALLEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8771-5559","authenticated-orcid":false,"given":"TOM","family":"SCHRIJVERS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,6,8]]},"reference":[{"key":"S0956796820000131_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292545"},{"key":"S0956796820000131_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40018-9_19"},{"key":"S0956796820000131_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411215"},{"key":"S0956796820000131_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0956796820000131_ref33","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_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"S0956796820000131_ref28","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"S0956796820000131_ref30","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2963"},{"key":"S0956796820000131_ref27","unstructured":"Peyton Jones, S. , Vytiniotis, D. , Weirich, S. & Washburn, G. (2006) Simple unification-based type inference for GADTs. In ICFP\u201906."},{"key":"S0956796820000131_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951945"},{"key":"S0956796820000131_ref25","unstructured":"Jr, Morris ., J. H. (1969) Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology."},{"key":"S0956796820000131_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800529"},{"key":"S0956796820000131_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0956796820000131_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351247"},{"key":"S0956796820000131_ref1","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_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_10"},{"key":"S0956796820000131_ref9","unstructured":"Dolan, S. , White, L. , Sivaramakrishnan, K. C. , Yallop, J. & Madhavapeddy, A. (2015) Effective concurrency through algebraic effects. In OCaml Workshop."},{"key":"S0956796820000131_ref4","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_ref11","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_ref12","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"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"},{"key":"S0956796820000131_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90144-7"},{"key":"S0956796820000131_ref8","doi-asserted-by":"publisher","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."},{"key":"S0956796820000131_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"S0956796820000131_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"S0956796820000131_ref31","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:21)2014"},{"key":"S0956796820000131_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"S0956796820000131_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"S0956796820000131_ref35","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_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_17"},{"key":"S0956796820000131_ref29","doi-asserted-by":"publisher","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."},{"key":"S0956796820000131_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"S0956796820000131_ref16","doi-asserted-by":"publisher","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"},{"key":"S0956796820000131_ref19","unstructured":"Kiselyov, O. & Sivaramakrishnan, K. C. (2016) Eff directly in OCaml. In OCaml Workshop."},{"key":"S0956796820000131_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"S0956796820000131_ref20","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"S0956796820000131_ref21","doi-asserted-by":"publisher","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":[[2026,5,26]],"date-time":"2026-05-26T22:36:51Z","timestamp":1779835011000},"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":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e15"}}