Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAn Effect System for Algebraic Effects and Handlers
194
0
0.0
(
0
)
Added by
Andrej Bauer
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Authors
Andrej Bauer
Ask ChatGPT about the research
No Arabic abstract
We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff, using Pittss theory of minimal invariant relations, and prove it adequate. We use this fact to develop tools for finding useful contextual equivalences, including an induction principle. To demonstrate their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We have formalized the effect system, the operational semantics, and the safety theorem in Twelf.
rate research
Read More
Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semantics of eff and discuss a prototype implementation based on it. Through examples we demonstrate how the standard effects are treated in eff, and how eff supports programming techniques that use various forms of delimited continuations, such as backtracking, breadth-first search, selection functionals, cooperative multi-threading, and others.
We introduce a new diagrammatic notation for representing the result of (algebraic) effectful computations. Our notation explicitly separates the effects produced during a computation from the possible values returned, this way simplifying the extension of definitions and results on pure computations to an effectful setting. Additionally, we show a number of algebraic and order-theoretic laws on diagrams, this way laying the foundations for a diagrammatic calculus of algebraic effects. We give a formal foundation for such a calculus in terms of Lawvere theories and generic effects.
This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 Algebraic effect handlers go mainstream. It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra. We draw an uninterrupted line of thought between algebra and computational effects. We begin on the mathematical side of things, by reviewing the classic notions of universal algebra: signatures, algebraic theories, and their models. We then generalize and adapt the theory so that it applies to computational effects. In the last step we replace traditional mathematical notation with one that is closer to programming languages.
Effect systems are used to statically reason about the effects an expression may have when evaluated. In the literature, such effects include various behaviours as diverse as memory accesses and exception throwing. Here we present CallE, an object-oriented language that takes a flexible approach where effects are just method calls: this works well because ordinary methods often model things like I/O operations, access to global state, or primitive language operations such as thread creation. CallE supports both flexible and fine-grained control over such behaviour, in a way designed to minimise the complexity of annotations. CallEs effect system can be used to prevent OO code from performing privileged operations, such as querying a database, modifying GUI widgets, exiting the program, or performing network communication. It can also be used to ensure determinism, by preventing methods from (indirectly) calling non-deterministic primitives like random number generation or file reading.
We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only. Thus, our technique avoids the explicit use of inductive proof rules during satisfiability proofs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates corresponding to the lemmas that are often needed when making inductive proofs. We present an algorithm that uses the new rule, together with the traditional folding/unfolding transformation rules, for the automatic removal of ADTs. We prove that if the set of the transformed clauses is satisfiable, then so is the set of the original clauses. By an experimental evaluation, we show that the use of the differential replacement rule significantly improves the effectiveness of ADT removal, and we show that our transformation-based approach is competitive with respect to a well-established technique that extends the CVC4 solver with induction.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
