Algebraic Effect Handlers with Bidirectional Type-Checking

In the development of type systems there are multiple paths for achieving more expressiveness. On the one hand, algebraic effect handlers allow us to reason about program’s side effects. On the other hand, dependent types make it possible to more precisely reason about program states and data and to prove general mathematical statements. We propose a new type system based on bidirectional type-checking for algebraic effects handlers and dependent types.