Abstract:
We propose a novel type system for effects and handlers using modal types. Conventional effect systems attach effects to function types, which can lead to verbose effect-polymorphic types, especially for higher-order functions. Our modal effect system provides succinct types for higher-order first-class functions without losing modularity and reusability. The core idea is to decouple effects from function types and instead to track effects through relative and absolute modalities, which represent transformations on the ambient effects provided by the context.
We formalise the idea of modal effect types in a multimodal System F-style core calculus
Met
with effects and handlers.Met
supports modular effectful programming via modalities without relying on effect variables. We encode a practical fragment of a conventional row-based effect system with effect polymorphism, which captures most common use-cases, intoMet
in order to formally demonstrate the expressive power of modal effect types. To recover the full power of conventional effect systems beyond this fragment, we seamlessly extendMet
toMete
with effect variables. We propose a surface languageMetel
forMete
with a sound and complete type inference algorithm inspired byFreezeML
.
Modal logic and modal types have also been used to implement Rust-like “ownership”, staged metaprogramming, distributed programming, and more.