No value restriction is needed for algebraic effects and handlers

TL;DR

This paper introduces a simple, sound Hindley-Milner type system for algebraic effects and handlers in a call-by-value setting, allowing generalization of all computations, not just values, which challenges previous assumptions about effects.

Contribution

It demonstrates that unrestricted polymorphism is sound for algebraic effects and handlers, expanding the understanding of type systems in effectful programming languages.

Findings

Type variable generalisation applies to all computations, not just values.

Unrestricted call-by-value Hindley-Milner polymorphism remains sound with algebraic effects.

Effect handlers cannot express reference cells but can simulate dynamically scoped state.

Abstract

We present a straightforward, sound Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which allows type variable generalisation of arbitrary computations, not just values. This result is surprising. On the one hand, the soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations. On the other hand, many programming examples can be recast to use effect handlers instead of these effects. Analysing the expressive power of effect handlers with respect to state effects, we claim handlers cannot express reference cells, and show they can simulate dynamically scoped state.