Simplifying explicit subtyping coercions in a polymorphic calculus with effects

Koprivec, Filip (avtor), Pretnar, Matija (avtor)

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.

• Jezik: Angleški jezik
• Ključne besede: computational effects, optimizing compilation, algebraic effects, polymorphic compilation, subtyping, denotational semantics
• Vrsta gradiva: Članek v reviji
• Tipologija: 1.01 - Izvirni znanstveni članek
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Status publikacije: Objavljeno
• Različica publikacije: Objavljena publikacija
• Datum objave: 01.01.2025
• Leto izida: 2025
• Št. strani: Str. 25:1-25:40
• Številčenje: Vol. 21, iss. 4, art. no. 25
• PID: 20.500.12556/RUL-179773
• UDK: 004.43:510.6
• ISSN pri članku: 1860-5974
• DOI: 10.46298/lmcs-21(4:25)2025
• COBISS.SI-ID: 269472003
• Datum objave v RUL: 24.02.2026

Gradivo je del revije

• Naslov: Logical methods in computer science
• Skrajšan naslov: Log. methods comput. sci.
• Založnik: Institut für Theoretische Informatik, Technische Universität Braunschweig.
• ISSN: 1860-5974
• COBISS.SI-ID: 16816473

Licence

• Licenca: CC BY 4.0, Creative Commons Priznanje avtorstva 4.0 Mednarodna
• Povezava: http://creativecommons.org/licenses/by/4.0/deed.sl
• Opis: To je standardna licenca Creative Commons, ki daje uporabnikom največ možnosti za nadaljnjo uporabo dela, pri čemer morajo navesti avtorja.

Projekti

• Financer: AFOSR - Air Force Office of Scientific Research
• Številka projekta: FA9550-17-1-0326

• Financer: AFOSR - Air Force Office of Scientific Research
• Številka projekta: FA9550-21-1-0024