Simplifying explicit subtyping coercions in a polymorphic calculus with effects

Koprivec, Filip (author), Pretnar, Matija (author)

Algebraic effect handlers are becoming an increasingly popular way of structuring effectful computations, and their performance is often a concern. One of the proposed approaches towards efficient compilation is tracking effect information through explicit subtyping coercions. However, in the presence of polymorphism, these coercions are compiled into additional arguments of compiled functions, incurring significant overhead. In this paper, we present a polymorphic effectful calculus, identify simplification phases needed to reduce the number of unnecessary constraints, and prove that they preserve semantics. In addition, we implement the simplification algorithm in the Eff language and evaluate its performance on a number of benchmarks. Though we do not prove the optimality of the presented simplifications, the results show that the algorithm eliminates all coercions, resulting in code as efficient as manually monomorphised one.

• Language: English
• Keywords: computational effects, optimizing compilation, algebraic effects, polymorphic compilation, subtyping, denotational semantics
• Work type: Article
• Typology: 1.01 - Original Scientific Article
• Organization: FMF - Faculty of Mathematics and Physics
• Publication status: Published
• Publication version: Version of Record
• Publication date: 01.01.2025
• Year: 2025
• Number of pages: Str. 25:1-25:40
• Numbering: Vol. 21, iss. 4, art. no. 25
• PID: 20.500.12556/RUL-179773
• UDC: 004.43:510.6
• ISSN on article: 1860-5974
• DOI: 10.46298/lmcs-21(4:25)2025
• COBISS.SI-ID: 269472003
• Publication date in RUL: 24.02.2026

Record is a part of a journal

• Title: Logical methods in computer science
• Shortened title: Log. methods comput. sci.
• Publisher: Institut für Theoretische Informatik, Technische Universität Braunschweig.
• ISSN: 1860-5974
• COBISS.SI-ID: 16816473

Licences

• License: CC BY 4.0, Creative Commons Attribution 4.0 International
• Link: http://creativecommons.org/licenses/by/4.0/
• Description: This is the standard Creative Commons license that gives others maximum freedom to do what they want with the work as long as they credit the author.

Projects

• Funder: AFOSR - Air Force Office of Scientific Research
• Project number: FA9550-17-1-0326

• Funder: AFOSR - Air Force Office of Scientific Research
• Project number: FA9550-21-1-0024