Local algebraic effect theories. (11th May 2020)

• Record Type: Journal Article
• Authors: LUKŠIČ, ŽIGA; PRETNAR, MATIJA
• Is Part Of: Journal of functional programming. Volume 30(2020)
• Publication Date: 2020-05-11
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796819000212
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. We present an alternative approach where the type system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimisations and reasoning tools.