ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Sun 12 Oct 2025 16:00 - 17:00 at Seminar Room 3 - Session 3

Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in understanding the precise relationship between effect systems with such disparate foundations. The main difficulty is that in both row-based and capability-based systems, effect tracking is entangled with function types.

We compare the expressive power of three styles of effect systems for effect handlers: row-based effect systems, as in Koka, capability-based effect systems, as in Effekt, and modal effect types, a recent novel approach based on multimodal type theory. Modal effect types decouple effect tracking from function types via modalities, providing the flexibility to encode the effect tracking behaviours in other effect systems. We give macro translations from variants of row-based and capability-based effect systems into modal effect types that preserve types and semantics. Our translations are the first to formally compare the expressive power of effect systems with different foundations and provide valuable insights into the essence of their differences.

Sun 12 Oct

Displayed time zone: Perth change

16:00 - 17:30
Session 3HOPE at Seminar Room 3
16:00
60m
Talk
Rows and Capabilities as Modal Effects (Extended Abstract)
HOPE
Wenhao Tang The University of Edinburgh, Sam Lindley University of Edinburgh