代數的效果
algebraic effect
限定繼續 (delimited continuation)
shift / reset
control / prompt
code:例.clj
; 指標 (代數。理論) を定義
(def-effect A int->(int, int))
(def-effect B (int, int)->int)
; handler を定義
(handle (th)
(case A i k (k (do-something i))) (case x x)))
; handler の下で實行する
(x-handler "some param" (do
(perform A 42)
(perform B 42 57)))
Eff
Eff is a functional programming language based on algebraic effect handlers. This means that Eff provides handlers of not only exceptions, but of any computational effect, allowing you to redirect output, wrap state modifications in transactions, schedule asynchronous threads, and much much more…
Algebraic effects, on which Eff is built, give rise to a uniform representation of all computational effects. Effects are thus first-class citizens of Eff and can be seamlessly combined. There is no need for the do notation, no need for monad transformers, and no need to reshuffle your whole program just to read a global flag.
Just like exceptions are a particular instance of an effect, exception handlers are a particular instance of effect handlers. In Eff, you can silence standard output, redirect it to a different channel, or even rearrange it. Similarly, state modifications can be prevented or grouped in transactions.
As handlers completely override the behaviour of effects, there is no need for a default behaviour to start with. Eff allows you to define your own effects. Just declare a choice operation and start writing your nondetermnistic programs. Later, you can write a handler that computes a single possible result, an optimal result, or a list of all results.
Koka
A Functional Language with Effect Types and Handlers
a strongly typed functional-style language with effect types and handlers.
Minimal but General
The core of Koka consists of a small set of well-studied language features, like first-class functions, a polymorphic type- and effect system, algebraic data types, and effect handlers. Each of these is composable and avoid the addition of “special” extensions by being as general as possible.
Effect Types
Koka tracks the (side) effects of every function in its type, where pure and effectful computations are distinguished. The precise effect typing gives Koka rock-solid semantics backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers.
Effect Handlers
Effect handlers let you define advanced control abstractions, like exceptions, async/await, iterators, parsers, ambient state, or probabilistic programs, as a user library in a typed and composable way.
Perceus Reference Counting
Perceus is an advanced compilation method for reference counting. This lets Koka compile directly to C code without needing a garbage collector or runtime system! This also gives Koka excellent performance in practice.
Reuse Analysis
Perceus also enables reuse analysis and lets Koka optimize functional-style programs to use in-place updates when possible.