No value restriction is needed for algebraic effects and handlers
From MaRDI portal
Publication:5372003
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 1670486 (Why is no real title available?)
- scientific article; zbMATH DE number 3882404 (Why is no real title available?)
- scientific article; zbMATH DE number 51766 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 1479618 (Why is no real title available?)
- scientific article; zbMATH DE number 2087441 (Why is no real title available?)
- A Classical Realizability Model for a Semantical Value Restriction
- A Substructural Type System for Delimited Continuations
- A certified implementation of ML with structural polymorphism and recursive types
- A static simulation of dynamic delimited control
- A syntactic theory of dynamic binding
- A theory of type polymorphism in programming
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Algebraic effects, linearity, and quantum programming languages
- Algebraic foundations for effect-dependent optimisations
- Algebraic operations and generic effects
- An algebraic presentation of predicate logic (extended abstract)
- An effect system for algebraic effects and handlers
- An introduction to algebraic effects and handlers (invited tutorial paper)
- Combining effects: sum and tensor
- Compiling standard ML to Java bytecodes
- Completeness for algebraic theories of local state
- Data types à la carte
- Delimited dynamic binding
- Dependent types and fibred computational effects
- Do be do be do
- Edinburgh LCF. A mechanized logic of computation
- Efficient algebraic effect handlers for Prolog
- Focalisation and Classical Realisability
- Functional and Logic Programming
- Fusion for free. Efficient algebraic effect handlers
- Handlers in action
- Handling algebraic effects
- Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
- Inferring algebraic effects
- Instances of computational effects: an algebraic perspective
- Koka: programming with row polymorphic effect types
- LCF considered as a programming language
- Local states in string diagrams
- Modelling environments in call-by-value programming languages.
- Normalization by evaluation and algebraic effects
- Notions of computation and monads
- On the expressive power of programming languages
- Operations on records
- Parametric effect monads and semantics of effect systems
- Polymorphic Delimited Continuations
- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
- Programming and reasoning with algebraic effects and dependent types
- Programming with algebraic effects and handlers
- Relating computational effects by \(\top \top \)-lifting
- The Mechanical Evaluation of Expressions
- The marriage of effects and monads
- Trace semantics for polymorphic references
- Two cotensors in one: presentations of algebraic theories for local state and fresh names
- Typability and type checking in System F are equivalent and undecidable
- Type directed compilation of row-typed algebraic effects
- Type inference for polymorphic references
- Typed Dynamic Control Operators for Delimited Continuations
- Types and programing languages
- Unchecked exceptions can be strictly more powerful than call/cc
Cited in
(7)- A type system for effect handlers and dynamic labels
- Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
- Signature restriction for polymorphic algebraic effects
- Functional and Logic Programming
- Handling polymorphic algebraic effects
- Continuation passing style for effect handlers
- Local algebraic effect theories
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)
