Rows and Capabilities as Modal Effects (Extended Abstract)
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 OctDisplayed time zone: Perth change
16:00 - 17:30 | |||
16:00 60mTalk | Rows and Capabilities as Modal Effects (Extended Abstract) HOPE | ||