No value restriction is needed for algebraic effects and handlers*. (24th January 2017)

• Record Type: Journal Article
• Authors: KAMMAR, OHAD; PRETNAR, MATIJA
• Is Part Of: Journal of functional programming. Volume 27(2017)
• Publication Date: 2017-01-24
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796816000320
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: 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.