|
|
|
|
|
|
by tome
19 days ago
|
|
|
Ah, thanks, maybe this holds a clue! (Clearly I have been interested in getting to the bottom of this for a while.) So maybe an "algebraic effect" is one that's isomorphic to a free monad of a functor that itself is an algebraic data type. That seems to give an unambiguous specification for what it means to handle an effect (a natural transformation) and to take a "free product" of effects (sum the functors). On the other hand I think it would mean that things like Future and general IO wouldn't be algebraic effects. |
|
|
- An algebraic theory consists of a "signature" (specifying a set of operation symbols with their arities) and a set of equations about those operations. An algebraic theory is purely syntactic, and does not give meaning to the operations or equations.
- An interpretation of an algebraic theory maps each operation symbol to a concrete mathematical object. It maps syntax to semantics.
- A model is an interpretation in which the algebraic theory's equations hold.
- A free model of an algebraic theory, generated by a set, is basically a model that can be mapped to any other model of the theory generated by the set.
So, an example of an algebraic theory is a group (as in the algebraic structure itself, not the various instances of a group). Its signature consists of the binary operation of combining, the unary operation of inverse, and the nullary operation of identity. The models of a group are its instances, such as the integers under additions and subtraction, or permutation functions on a set. The integers are the free group (that is, the free model of the group) generated by the set {1}.
Algebraic theories can also describe the effects of a programming language (e.g. reader, writer, or state). The free model of an algebraic effect is given by the syntax trees describing its effectful computations. Effect handlers are maps from syntax trees, transforming computations into other computations within the programming language.
> On the other hand I think it would mean that things like Future and general IO wouldn't be algebraic effects.
For what it's worth, Example 2.3 in the paper states that IO is an algebraic effect, albeit one with no equations. What might be confusing is that the handler of the IO effect cannot have the level of concreteness to actually implement the IO operations. Effect handlers only map computations to computations within the "pure" programming language. From the paper:
> What we still lack is a mathematical model of computational effects at the level of the external environment in which the program runs. There is always a barrier between the program and its external environment, be it a virtual machine, the operating system, or the underlying hardware. The actual computational effects cross the barrier, and cannot be modeled as handlers. A handler gets access to the continuation, but when a real computational effects happens, the continuation is not available. If it were, then after having launched missiles, the program could change its mind, restart the continuation, and establish world peace.