No value restriction is needed for algebraic effects and handlers

Ohad Kammar, Matija Pretnar

Research output: Contribution to journalArticlepeer-review


We present a straightforward, sound, Hindley–Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that 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, and that many programming examples can be recast to use effect handlers instead of these effects. After presenting the calculus and its soundness proof, formalised in Twelf, we analyse the expressive power of effect handlers with respect to state effects. We conjecture handlers alone cannot express reference cells, but show they can simulate dynamically scoped state, establishing that dynamic binding also does not need a value restriction.
Original languageEnglish
Article numbere7
Number of pages34
JournalJournal of Functional Programming
Publication statusPublished - 24 Jan 2017


Dive into the research topics of 'No value restriction is needed for algebraic effects and handlers'. Together they form a unique fingerprint.

Cite this