This file implements an extensible effects library stdlib/effect.mc, inspired by algebraic effects / free(er) monads. To learn more, see e.g., ^1,^2,^3.
The main part of the library is the Effect fragment, which defines a type Eff a representing generic effectful computations. Users may extend Eff with their own effectful operations along with handlers for those operations.
Effects interact well with language fragment composition. To use a given effect, simply include the corresponding fragment and start using the effectful operations. A sem clause in one language fragment may use a given effect (e.g., a read-only context) without interfering with the definitions of other clauses (e.g., without having to add an extra parameter even in clauses where the context is unused). The only requirement is that the sem returns an Eff-type.
For example, consider the following fragment:
lang TestLang = Reader + NonDet
sem getInt : Ctx -> Int
sem effProg : () -> Eff Int
sem effProg = | () ->
bind (choose [0,1]) (lam i.
bind (choose [2,3]) (lam j.
bind (ask getInt) (lam k.
return (addi (addi i j) k))))
end
The fragment TestLang imports two effects: read-only context (Reader) and non-determinism (NonDet). effProg defines an effectful program which uses both effects. The program first chooses two numbers i \in [0,1] and j \in [2,3], then reads a number k from the context, and then returns the sum of the three. Note that the context type is kept abstract, we only declare a sem getInt : Ctx -> Int for extracting an integer from it.
To run the program, we provide a concrete implementation of getInt and a value for the context:
lang TestLangImpl = TestLang
syn Ctx = | ICtx Int
sem getInt = | ICtx i -> i
end
mexpr
use TestLangImpl in
utest runEff (handleND (handleReader (ICtx 7) (effProg ())))
with [9,10,10,11] in ()
Here, the Reader effect is first handled using handleReader with a context ICtx 7, and then the nondeterminism effect is resolved using handleND. When all effects are handled, runEff can be used to extract the final value, in this case [9,10,10,11].
There is also stdlib/mexpr/ast-effect.mc, which contains variations of an smapEff-function which can be used to map effectful operations over MExpr AST nodes. The utest part of the file is derived from ast-result.mc, and demonstrates how the Result effect of result.mc can be emulated by Eff using the Writer and Failure effects (although it will not accumulate more than one error, as opposed to Result).
There are two main limitations of the implementation at current. The first is that there is no static check that all effects have been handled. Trying to extract a value from an effectful computation without handling all effects will give a runtime error. This could potentially be solved by constructor types or an extension of them using row polymorphism. The second limitation is that the runtime performance is not very good. There are techniques for improving the efficiency (e.g., ^3), but these are not implemented currently, and achieving very good performance in an in-language implementation may take a lot of effort.
To get optimal support for this kind of effect system, integrating it into the language somehow seems like the best solution. For example, we could consider adding primitives piggybacking on OCaml 5's effect handlers and adding a static check based on some variation of effect rows.
This file implements an extensible effects library
stdlib/effect.mc
, inspired by algebraic effects / free(er) monads. To learn more, see e.g., ^1,^2,^3.The main part of the library is the
Effect
fragment, which defines a typeEff a
representing generic effectful computations. Users may extendEff
with their own effectful operations along with handlers for those operations.Effects interact well with language fragment composition. To use a given effect, simply include the corresponding fragment and start using the effectful operations. A
sem
clause in one language fragment may use a given effect (e.g., a read-only context) without interfering with the definitions of other clauses (e.g., without having to add an extra parameter even in clauses where the context is unused). The only requirement is that thesem
returns anEff
-type.For example, consider the following fragment:
The fragment
TestLang
imports two effects: read-only context (Reader
) and non-determinism (NonDet
).effProg
defines an effectful program which uses both effects. The program first chooses two numbersi \in [0,1]
andj \in [2,3]
, then reads a numberk
from the context, and then returns the sum of the three. Note that the context type is kept abstract, we only declare a semgetInt : Ctx -> Int
for extracting an integer from it.To run the program, we provide a concrete implementation of
getInt
and a value for the context:Here, the
Reader
effect is first handled usinghandleReader
with a contextICtx 7
, and then the nondeterminism effect is resolved usinghandleND
. When all effects are handled,runEff
can be used to extract the final value, in this case[9,10,10,11]
.There is also
stdlib/mexpr/ast-effect.mc
, which contains variations of ansmapEff
-function which can be used to map effectful operations over MExpr AST nodes. The utest part of the file is derived fromast-result.mc
, and demonstrates how theResult
effect ofresult.mc
can be emulated byEff
using theWriter
andFailure
effects (although it will not accumulate more than one error, as opposed toResult
).There are two main limitations of the implementation at current. The first is that there is no static check that all effects have been handled. Trying to extract a value from an effectful computation without handling all effects will give a runtime error. This could potentially be solved by constructor types or an extension of them using row polymorphism. The second limitation is that the runtime performance is not very good. There are techniques for improving the efficiency (e.g., ^3), but these are not implemented currently, and achieving very good performance in an in-language implementation may take a lot of effort.
To get optimal support for this kind of effect system, integrating it into the language somehow seems like the best solution. For example, we could consider adding primitives piggybacking on OCaml 5's effect handlers and adding a static check based on some variation of effect rows.