Effect handlers and session types are two hot topics in programming language research nowadays. Algebraic effects and effect handlers offer an expressive and modular way to implement computational effects. To enable safe and scalable usage of effect handlers, the type system is usually extended with an effect system to track the effects used by programs. Session types provide static guarantees that concurrent programs respect communication protocols. Intuitively, the interaction between effects and handlers can also be described as communication protocols. Can we design effect systems for effect handlers using the idea of session types?

We explore the possibilities of this new design discipline. Specifically, we propose a call-by-push-value core calculus $\lambda^{\mathrm{ch}}{\mathrm{eff}}$ with a novel effect system inspired by session types. The key notion of it are \emph{channels} which carry protocols represented by behaviour effect types, specifying the behaviours of effects and handlers in programs. $\lambda^{\mathrm{ch}}{\mathrm{eff}}$ tracks channels as capabilites and prevent them from escaping. Different channels do not interfere with each other; effects in one channel must and can only be handled in the dual channel. Channels essentially provide a similar but more flexible version of named handlers. Furthermore, the behavioural effect types of $\lambda^{\mathrm{ch}}_{\mathrm{eff}}$ allows us to easily track more involved control flow like bidirectional effects.