[INCLUDE=presentation] Title : Algebraic effects and handlers Sub Title : New language ideas for user-defined side-effects Author : Gabriel Scherer Affiliation : Northeastern University Email : gabriel.scherer@gmail.com Reveal Theme : solarized Beamer Theme : singapore [TITLE] # Introduction ## Context Last March, I went to a Dagstuhl Seminar on Algebraic Effects and Handlers. ![group photo] [group photo]: http://gallium.inria.fr/~scherer/tmp/dagstuhl.JPG "group photo" { vertical-align:middle } I'm talking about what I learned there. *None* of the talk is about my own work. ## Algebraic effect and handlers: story 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) ## Algebraic effect and handlers: implementations (all in development) - [Eff](http://www.eff-lang.org/try/): Matija Pretnar and Andrej Bauer, 2011-now. - [Links](http://groups.inf.ed.ac.uk/links/) : Daniel Hillerström and Sam Lindley, 2015. - [Frank](http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-march2014.pdf): Conor McBride, 2007, 2012. - [OCaml+effects](http://kcsrk.info/ocaml/multicore/2015/05/20/effects-multicore/): Stephen Dolan, Leo White, KC Sivaramakrishnan, 2016. ## Warmup: ML exceptions ```ocaml 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 ``` ## Warmup `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. ```ocaml 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". ## Resumable exceptions? ```ocaml let pos n = if n >= 0 then n else raise (Foo n) ``` Resumable exceptions in upstream OCaml. Let's imagine: ```ocaml try[@resumable] map pos input with | Foo n k -> continue k (-n) ``` or ```ocaml 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 signatures Effect signature := set of *operations* ```ocaml 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 ``` ## Effectful code Instead of returning a value, one may perform an operation. ```ocaml let rec in_interval a b : int = if a = b then a else if perform Choose then a else in_interval (a + 1) b ``` ```ocaml let incr_twice () : int = perform (Set ((perform Get) + 1)); perform (Set ((perform Get) + 1)); perform (Print "incremented twice"); perform Get ``` ## Effect handlers: examples Handle an operation; maybe resume computation. ```ocaml let a_number = handle (in_interval 1 10) with | Choose k -> continue k (Random.bool ()) ``` ```ocaml 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 ``` ## Effect handlers: subsumes exceptions This subsumes exceptions. ```ocaml 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 -> ... ``` ## Effect handlers: several handlers for an effect Changing the handler brings expressivity. ```ocaml let always_true = handler | Choose k -> continue k true let one = handle (in_interval 1 10) with always_true ``` ```ocaml let random = handler | Choose () k -> let b = Random.bool () in continue k b let random_one = handle (in_interval 1 10) with random ``` ```ocaml 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 *) ``` ## Effect handlers 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. ## Combining handlers ```ocaml 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 ``` # User-defined effects, motivation and theory ## Why would user define their own effects? 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. ## (Theory) Monads vs. algebraic effects Two ways to define algebraic structure: direct construction, or presentation by generators and equations. ```math Monoid1 := (Nat,1,*) ``` ```math 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. ## Monads A Monad `m a` is any parametrized type `m` that support two operations ```haskell 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 Algebraic effects: representation by generators + equations ```ocaml 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. ## Relating an algebraic effect and its monad: State 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 ``` ```ocaml s -> (a * s) ``` (Want more on this? Read [this blog post](http://gallium.inria.fr/blog/lawvere-theories-and-monads/) of Pierre Dagand) ## Aside Does this equation hold? Does this law hold? Language support for equational reasoning. One of the most impactful, overlooked open problems today. # Going further in theory ## Semantic of imperative programs Computation trees ![computation tree] [computation tree]: computation-tree.png "computation tree" { vertical-align:middle } ## Moggi's idea 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) ## Wadler's idea 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`. ```haskell 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 vs. indirect style Direct style: writing and reasoning on the effectful language. Indirect sytle: writing and reasoning on the pure encoding. - Moggi's computational lambda-calculus: direct style. - CPBV: indirect style. Both styles are fine. Direct style semantics models ask an additional, interesting question: what is a *semantic* characterization of pure programs? ## Free monads vs. effect handlers 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 ``` # Going further in practice ## Eff: dynamic effects (1) ```ocaml 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 ``` ## Eff: dynamic effects (2) ```ocaml 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 ``` ```ocaml type state s = effect operation get : unit -> s operation set : s -> unit end;; ``` ## Frank: effectful-call-by-value ```haskell 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). ``` ```haskell 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). ``` ## Encodings You can also abstract over all monads providing given operations: ```haskell 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: - what are the best designs ? - do we need them as language features or are libraries enough? Sometimes library encodings make designs harder to appreciate.