No value restriction is needed for algebraic effects and handlers
From MaRDI portal
Publication:5372003
DOI10.1017/S0956796816000320zbMATH Open1418.68034arXiv1605.06938MaRDI QIDQ5372003FDOQ5372003
Publication date: 23 October 2017
Published in: Journal of Functional Programming (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1605.06938
Recommendations
Cites Work
- A theory of type polymorphism in programming
- Edinburgh LCF. A mechanized logic of computation
- Programming with algebraic effects and handlers
- An Effect System for Algebraic Effects and Handlers
- LCF considered as a programming language
- Modelling environments in call-by-value programming languages.
- Algebraic operations and generic effects
- Combining effects: sum and tensor
- Normalization by evaluation and algebraic effects
- Title not available (Why is that?)
- Algebraic foundations for effect-dependent optimisations
- Title not available (Why is that?)
- An Algebraic Presentation of Predicate Logic
- Handlers in action
- Instances of Computational Effects: An Algebraic Perspective
- Notions of computation and monads
- Typability and type checking in System F are equivalent and undecidable
- Title not available (Why is that?)
- Types and programing languages
- Title not available (Why is that?)
- On the expressive power of programming languages
- Relating computational effects by \(\top \top \)-lifting
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Operations on records
- The Mechanical Evaluation of Expressions
- Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
- Title not available (Why is that?)
- Delimited dynamic binding
- Polymorphic Delimited Continuations
- A Substructural Type System for Delimited Continuations
- An introduction to algebraic effects and handlers (invited tutorial paper)
- Focalisation and Classical Realisability
- Type inference for polymorphic references
- The marriage of effects and monads
- A syntactic theory of dynamic binding
- Handling algebraic effects
- Data types à la carte
- Programming and reasoning with algebraic effects and dependent types
- Unchecked exceptions can be strictly more powerful than call/cc
- Typed Dynamic Control Operators for Delimited Continuations
- Title not available (Why is that?)
- Efficient algebraic effect handlers for Prolog
- Parametric effect monads and semantics of effect systems
- Compiling standard ML to Java bytecodes
- Algebraic effects, linearity, and quantum programming languages
- Trace semantics for polymorphic references
- Dependent Types and Fibred Computational Effects
- A static simulation of dynamic delimited control
- A Classical Realizability Model for a Semantical Value Restriction
- Functional and Logic Programming
- Two cotensors in one: presentations of algebraic theories for local state and fresh names
- Local States in String Diagrams
- Inferring algebraic effects
- Completeness for Algebraic Theories of Local State
- Fusion for Free
- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
- Title not available (Why is that?)
- Type directed compilation of row-typed algebraic effects
- Do be do be do
- A certified implementation of ML with structural polymorphism and recursive types
Cited In (6)
- A type system for effect handlers and dynamic labels
- Signature restriction for polymorphic algebraic effects
- Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
- Functional and Logic Programming
- Continuation passing style for effect handlers
- Local algebraic effect theories
Uses Software
This page was built for publication: No value restriction is needed for algebraic effects and handlers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5372003)
