No value restriction is needed for algebraic effects and handlers
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 unres...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Journal article |
| Published: |
Cambridge University Press
2017
|
| _version_ | 1797064974291435520 |
|---|---|
| author | Kammar, O Pretnar, M |
| author2 | Felleisen, M |
| author_facet | Felleisen, M Kammar, O Pretnar, M |
| author_sort | Kammar, O |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T21:21:59Z |
| format | Journal article |
| id | oxford-uuid:41c04594-0d79-4b81-ab31-da032f036bd9 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T21:21:59Z |
| publishDate | 2017 |
| publisher | Cambridge University Press |
| record_format | dspace |
| spelling | oxford-uuid:41c04594-0d79-4b81-ab31-da032f036bd92022-03-26T14:45:33ZNo value restriction is needed for algebraic effects and handlersJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:41c04594-0d79-4b81-ab31-da032f036bd9Symplectic Elements at OxfordCambridge University Press2017Kammar, OPretnar, MFelleisen, MGibbons, JWe 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. |
| spellingShingle | Kammar, O Pretnar, M No value restriction is needed for algebraic effects and handlers |
| title | No value restriction is needed for algebraic effects and handlers |
| title_full | No value restriction is needed for algebraic effects and handlers |
| title_fullStr | No value restriction is needed for algebraic effects and handlers |
| title_full_unstemmed | No value restriction is needed for algebraic effects and handlers |
| title_short | No value restriction is needed for algebraic effects and handlers |
| title_sort | no value restriction is needed for algebraic effects and handlers |
| work_keys_str_mv | AT kammaro novaluerestrictionisneededforalgebraiceffectsandhandlers AT pretnarm novaluerestrictionisneededforalgebraiceffectsandhandlers |