Gabriel Scherer
Northeastern University
gabriel.scherer@gmail.com |
Last March, I went to a Dagstuhl Seminar on
Algebraic Effects and Handlers.
I'm talking about what I learned there.
None of the talk is about my own work.
A formal presentation of side-effects.
Alternative to monads.
(Gordon Plotkin and John Power, 2002)
Effect handlers: a programming language design inspired by algebraic effect.
(Gordon Plotkin and Matija Pretnar, 2009)
(all in development)
exception Foo of int
let pos n = if n >= 0 then n else raise (Foo n)
let rec map f = function
| [] -> []
| x::xs ->
let a = f x in a :: map f xs
let () =
let pos_input =
try map pos [1; 2; -3; 4] with
| Foo n ->
eprintf "negative input found: %d\n" n;
raise Exit
in List.iter (printf "%d\n") pos_input
match .. with exception
Proposed by Christophe Raffali in 2002, but forgotten.
(Better syntax than Benton and Kennedy's “exceptional syntax”)
Implemented by Jeremy Yallop in OCaml 4.02 (Aug 2014), inspired by effect handlers.
match map pos [1; 2; -3; 4] with
| exception (Foo n) ->
eprintf "negative input found: %d\n" n;
raise Exit
| pos_input -> List.iter (printf "%d\n") pos_input
Idea: “value return” vs. “exceptional return”.
let pos n = if n >= 0 then n else raise (Foo n)
Resumable exceptions in upstream OCaml. Let's imagine:
try[@resumable] map pos input with
| Foo n k -> continue k (-n)
or
try[@resumable] map pos input with
| Foo n k ->
let n = read_int () in
continue k n
Notice: here we need deep rather than shallow handlers.
Typing? How do we know which type k
expects?
Effect signature := set of operations
effect choice =
| Choose : bool
effect IO =
| Print : string -> unit
| Read : string
effect int_state =
| Get : int
| Set : int -> unit
effect scheduler =
| Spawn : (unit -> unit) -> unit
| Yield : unit
Instead of returning a value, one may perform an operation.
let rec in_interval a b : int =
if a = b then a
else
if perform Choose then a
else in_interval (a + 1) b
let incr_twice () : int =
perform (Set ((perform Get) + 1));
perform (Set ((perform Get) + 1));
perform (Print "incremented twice");
perform Get
Handle an operation; maybe resume computation.
let a_number =
handle (in_interval 1 10) with
| Choose k -> continue k (Random.bool ())
let state (f : unit -> 'a) : int -> 'a =
handle f () with
| Get k -> (fun s -> (continue k s) s)
| Set s k -> (fun _ -> (continue k ()) s)
| return v -> (fun _ -> v)
let two = (state incr_twice) 0
This subsumes exceptions.
effect exn =
| Foo : int -> empty
let pos n = if n >= 0 then n else perform (Foo n)
handle map pos [1; 2; -3; 4] with
| Foo n k -> (* k cannot be called, no possible argument at type 'empty' *)
| return pos_int -> ...
Changing the handler brings expressivity.
let always_true = handler
| Choose k -> continue k true
let one = handle (in_interval 1 10) with always_true
let random = handler
| Choose () k ->
let b = Random.bool () in
continue k b
let random_one = handle (in_interval 1 10) with random
let all_choices = handler
| Choose k -> List.append (continue k true) (continue k false)
| return v -> [v]
let all = handle (in_interval 1 10) with all_choices
(* note: type change *)
Change of viewpoint: we are not merely playing with delimited continuations (or resumable exceptions), we are defining side-effects.
(Side-effects implemented through control; “the mother of all monads”)
Claim: this is more structured, makes code easier to understand.
Nota Bene: we can provide different handlers for the same signature.
effect backtrack =
| Fail : empty
| Amb : bool -> a
type 'a option =
| None : 'a option
| Some : 'a -> 'a option
let solve = handler
| return v -> Some v
| Fail k -> None
| Amb k ->
(match continue k true with
| Some v -> Some v
| None -> continue k false)
let f () =
if (perform Amb)
then (incr_twice; perform Fail)
else (perform Get)
(handle (state f) 0 with solve) = Some 0
(state (fun () -> handle f () with solve) 0) = Some 2
Okay, Racket has most effects built-in. Delimited control, state, stack marking, concurrency, randomness, dynamic binding, etc.
But combinatorial explosion: you don't support all combinations.
What about mutable state that is rolled back on backtracking?
Also: less runtime, more library.
Two ways to define algebraic structure: direct construction, or presentation by generators and equations.
Monoid1 := (Nat,1,*)
Monoid2 :=
generators: (a, b)
equations: (b.b = b)
aa
aab
aababaa
abba = aba
Puzzle: what's a direct construction for Monoid2
?
It's non-trivial to go from one presentation to the other. For a given application, one may be more convenient.
A Monad m a
is any parametrized type m
that support two operations
return : a -> m a
bind : m a -> (a -> m b) -> m b
with some equations that those operations must respect. Examples:
Partial A := Maybe A
Error{E} A := A + E
State{S} A := (S -> A * S)
Concurrent A := List A
A monad is the denotational semantics of an effect.
(It became a programming technique only later.)
Algebraic effects: representation by generators + equations
effect state =
| Get : int
| Set : int -> unit
where (* not actual code *)
(Get; Get) = Get
(Set s; Get) = (Set s; s)
(Set s1; Set s2) = (Set s2)
Equations matter; but languages don't support them yet. Need for usable verification technology.
Handling concurrent
effects with Set A
or List A
.
Constraining the producer vs. quotienting the consumer.
What are the equations on state?
Normal form of a sequence of operations: Get; Set
.
Normal form of a term:
let s = perform Get in
let result = ... in
Set (...);
return result
s -> (a * s)
(Want more on this? Read this blog post of Pierre Dagand)
Does this equation hold? Does this law hold?
Language support for equational reasoning.
One of the most impactful, overlooked open problems today.
Computation trees
Computational λ-calculus with effects
⇓ type-transforming translation ⇓
Pure λ-calculus
One effect at a time:
a
+ get/set
⇒ (s → a × s)
A computation tree (above) becomes a values at a richer type (below)
Instead of writing effectful terms in the effectful lambda-calculus, we can write their encoding in the pure lambda-calculus directly.
computation of type a
with monadic effects m
⇒ value at type m a
.
do
n1 <- get
set (n + 1)
n2 <- get
set (n2 + 1)
n3 <- get
return n3
get >>= \n1 -> set (n1 + 1) >>= \() ->
get >>= \n2 -> set (n2 + 1) >>= \() ->
get >>= \n3 -> return n3
The white lie of purity: do
-notation is just as hard to reason about
as imperative code.
Direct style: writing and reasoning on the effectful language.
Indirect sytle: writing and reasoning on the pure encoding.
Both styles are fine.
Direct style semantics models ask an additional, interesting question: what is a semantic characterization of pure programs?
Two ways to get different implementations for the same effects.
Free monad over operations S ~ Terms over an effect signature S
perform (op v1 v2 ...)
let x = e1 in e2
return v
Free monad interpreters ~ Effect handlers
Invariant-enforcing representation ~ Algebraic equations
Concurrent A := List A
Concurrent A := Set A
type choice = effect
operation decide : unit -> bool
end;;
(* We create an instance of choice to work with. *)
let c = new choice
let choose_one c = handler
| c#decide () k -> k true
with choose_one c handle
let x = (if c#decide () then 10 else 20) in
let y = (if c#decide () then 0 else 5) in
x - y
let choose_all c = handler
| c#decide () k -> k true @ k false
| val x -> [x]
let c = new choice
let d = new choice
let choices =
with choose_one c handle
with choose_all d handle
let x = (if c#decide () then 10 else 20) in
let y = (if d#decide () then 0 else 5) in
x - y
type state s = effect
operation get : unit -> s
operation set : s -> unit
end;;
interface State x = get : x
| put : x -> Unit.
toggle : [State Bool]Bool.
toggle = bind (get!) {x -> semi (put (not x)) x}.
evalState : s -> [State s]a -> a.
evalState s v = v.
evalState s [put s' -> k] = evalState s' (k Unit).
evalState s [get -> k] = evalState s (k s).
interface Send x = send : x -> Unit.
interface Receive x = receive : x.
interface Abort = aborting : Zero.
pipe : [Send x]Unit -> [Receive x]y -> [Abort]y.
pipe [_] y = y.
pipe Unit [_] = abort!.
pipe [send x -> s] [receive -> r] = pipe (s Unit) (r x).
You can also abstract over all monads providing given operations:
class MonadPlus m where
fail :: m a
choose :: m a -> m a -> m a
inInterval : MonadPlus choice => Int -> Int -> choice Int
Monad transformer stacks, Oleg's Eff library.
When do we need new/extended languages? Two debates:
Sometimes library encodings make designs harder to appreciate.