#{BEGIN: header} # # PROGRAMMING WITH ALGEBRAIC EFFECTS AND HANDLERS # Daniel Hillerström # The University of Edinburgh # # E-mail : daniel.hillerstrom@ed.ac.uk # Website: http://homepages.inf.ac.ed.uk/s1467124 # Twitter: @dhillerstrom # #{END} #{BEGIN: aboutme} # # About me: # # Danish national with Swedish roots living in the UK. # # Background: # - Joint degree in maths and CS from Aalborg University, Denmark # - Master's degree in CS from the University of Edinburgh # - Currently, PhD student at the University of Edinburgh # # Religious beliefs: Principled abstractions, disciplined programming. # # Interests: Compilers and programming languages. # #{END} #{BEGIN: disclaimer} # # Notice: # # The slides in this talk are in fact a runnable program written in # Links. # # I have developed an extension to Links known as "effect handlers", # which I am going to give you an introduction to. # # The syntax of Links is similar to that of JavaScript, but with a # sane semantics. # #{END} ## Some standard functions fun maximum(a,b) { if (a < b) b else a } fun showPlayer(p) { switch(p) { case Alice -> "Alice" case Bob -> "Bob" } } fun concatMap(f, l) { switch (l) { case [] -> [] case hd::tl -> f(hd) ++ concatMap(f, tl) } } fun filter(p, l) { concatMap (fun (x) {if(p(x)) [x] else []}, l) } fun drop(n, xs) { switch((n,xs)) { case (0,xs) -> xs case (_,[]) -> [] case (_,x :: xs) -> drop(n-1, xs) } } fun take(n, xs) { switch ((n,xs)) { case (0, _) -> [] case (_, []) -> [] case (_, x :: xs) -> x :: take(n-1, xs) } } fun fold_left(f,acc,xs) { switch(xs) { case x :: xs -> fold_left(f, f(acc,x), xs) case [] -> acc } } fun map(f,xs) { switch(xs) { case x1 :: xs -> f(x1) :: map(f,xs) case [] -> [] } } sig zip : ([a], [b]) ~> [(a, b)] fun zip(l, r) { switch ((l, r)) { case ([], []) -> [] case (lh::lt, rh::rt) -> (lh, rh) :: zip (lt, rt) case (_, _) -> [] } } fun range(a,b) { fun range_aux(n, acc) { if (n < a) acc else range_aux(n-1, n :: acc) } range_aux(b, []) } fun any(p, l) { switch (l) { case [] -> false case x::xs -> p(x) || any(p, xs) } } fun elem(x,xs) { any(fun(y) { x == y }, xs) } fun const(x)(_) { x } fun run(m) { m() } fun example(m)() { run(m) } ## Motivation #{BEGIN: motivation} # Motivation # # Virtually, every program comprise an *effectful* component, e.g. # - raise exceptions # - perform input/output # - mutate some state # - fork threads # - non-determinism # - ... and so forth # # In most programming languages effects are dealt with *implicitly*. # # Algebraic effects and handlers provide a modular abstraction for modelling and controlling effects *explicitly*. #{END} #{BEGIN: prologue} # _____ _ # | __ \ | | _ # | |__) | __ ___ | | ___ __ _ _ _ ___ (_) # | ___/ '__/ _ \| |/ _ \ / _` | | | |/ _ \ # | | | | | (_) | | (_) | (_| | |_| | __/ _ # |_| |_| \___/|_|\___/ \__, |\__,_|\___| (_) # __/ | # |___/ # # _____ _ _ _ _ # / ____| | (_) | | (_) # | | | |__ ___ _ ___ ___ _ __ ___ __ _| | ___ _ __ __ _ # | | | '_ \ / _ \| |/ __/ _ \ | '_ ` _ \ / _` | |/ / | '_ \ / _` | # | |____| | | | (_) | | (_| __/ | | | | | | (_| | <| | | | | (_| | # \_____|_| |_|\___/|_|\___\___| |_| |_| |_|\__,_|_|\_\_|_| |_|\__, | # __/ | # |___/ #{END} ## Warm-up example #{BEGIN: choose} # Nondeterminism as an algebraic effect # # An algebraic effect is a collection of abstract operations. A # concrete example is *nondeterminism* which is described by a # nondeterministic choice operation, called Choose: sig choose : () {Choose:Bool |_}-> Bool fun choose() { do Choose } # The imperative primitive 'do' invokes the operation. Operations are # entirely syntactical; on their own they are meaningless. #{END} #{BEGIN: coin-flip} # Coin flipping model # # We can use Choose to model a coin flip: typename Toss = [|Heads|Tails|]; sig toss : () {Choose:Bool |_}-> Toss fun toss() { if (choose()) Heads else Tails } # The function 'toss' is said to be an abstract computation. Abstract # computations are composed from abstract operations. Again, they are # meaningless. #{END} #{BEGIN: randomResult} # A random interpretation # # An effect handler interpret operations by instantiating them with # concrete implementations. For example, we can give a random # interpretation of Choose: typename Comp(e::Row, a) = () ~e~> a; sig randomResult : (Comp({Choose:Bool |e}, a)) -> Comp({Choose{_} |e}, a) fun randomResult(m)() { handle(m) { case Return(x) -> x case Choose(k) -> k(random() > 0.5) } } # The Return-clause is invoked when the computation m returns. The # parameter x gets bound tot the return value of m. # The Choose-clause exposes a parameter k which is the continuation of # Choose in the computation m. # Example 1 var ex1 = example( randomResult(toss) ); #{END} #{BEGIN: allResults} # Another interpretation # # We can give an alternative interpretation that enumerates the sample # space. The key idea is to interpret Choose twice: # - First as true, # - and afterwards as false. sig allResults : (Comp({Choose:Bool |e}, a)) -> Comp({Choose{_} |e}, [a]) fun allResults(m)() { handle(m) { case Return(x) -> [x] case Choose(k) -> k(true) ++ k(false) } } # The Return-clause lifts each outcome into a singleton list. # The Choose-clause concatenates the results of both interpretations. # Example 2 var ex2 = example( allResults(toss) ); #{END} #{BEGIN: generalised-choice} # Generalised choice # # We may easily generalise the binary choice to a n-ary choice: sig chooseFrom : ([a]) {Choose:Bool |_}~> a fun chooseFrom(xs) { var len = length(xs); if (len > 1) { if (choose()) chooseFrom(take(len / 2, xs)) else chooseFrom(drop(len / 2, xs)) } else { hd(xs) } } # Examples 3 and 4: var ex3 = example( randomResult( fun() { chooseFrom([Heads,Tails]) : Toss } ) ); var ex4 = example( allResults( fun() { chooseFrom([Heads,Tails]) : Toss } ) ); #{END} #{BEGIN: whycare} # But, why? # # Why should we care about this style of programming? # - Modular reasoning for effectful programs (Craig MchLaughlin) # - Modular abstractions for effectful programming (me) # - New ways of thinking about programs #{END} #{BEGIN: nim} # _ _ _ # | \ | (_) # | \| |_ _ __ ___ __ _ __ _ _ __ ___ ___ # | . ` | | '_ ` _ \ / _` |/ _` | '_ ` _ \ / _ \ # | |\ | | | | | | | | (_| | (_| | | | | | | __/ # |_| \_|_|_| |_| |_| \__, |\__,_|_| |_| |_|\___| # __/ | # |___/ #{END} #{BEGIN: nim-rules} # A mathematical game # # Nim game (https://en.wikipedia.org/wiki/Nim) # This example is adapted from Kammar et al. (2013) # (https://github.com/slindley/effect-handlers) # # Mathematical game Nim # # Rules: # - Two players: Alice and Bob; Alice always starts. # - One heap of N sticks. # - Turn-based, one move per turn. # - A player may pick between 1-3 sticks at each turn. # - The player, who takes the last stick, wins. # #{END} #{BEGIN: player-model} # Modelling players # # A datatype modelling the players: typename Player = [|Alice|Bob|]; #{END} #{BEGIN: move} # Defining move # # The notion of *move* is centric to the game. # We model a move as an abstract operation, that is parameterised by # the active player and the number of sticks left in the heap: sig move : (Player, Int) {Move:(Player,Int) {}-> Int |_}~> Int fun move(p, n) { do Move(p,n) } #{END} #{BEGIN: aliceTurn} # Game model # # We model the game as two mutually recursive functions, that are # parameterised by the number of sticks left in the game: sig aliceTurn : (Int) {Move:(Player,Int) {}-> Int |_}~> Player fun aliceTurn(n) { if (n <= 0) Bob else bobTurn(n - move(Alice,n)) } # The definition of bobTurn is completely analogous: sig bobTurn : (Int) {Move:(Player,Int) {}-> Int |_}~> Player fun bobTurn(n) { if (n <= 0) Alice else aliceTurn(n - move(Bob,n)) } #{END} #{BEGIN: game} # A convenient function that starts a game with n sticks: fun game(n)() { aliceTurn(n) } #{END} #{BEGIN: strategies} # _____ _ _____ # | __ \ | | |_ _| _ # | |__) |_ _ _ __| |_ | | (_) # | ___/ _` | '__| __| | | # | | | (_| | | | |_ _| |_ _ # |_| \__,_|_| \__| |_____| (_) # _____ _ _ _ # / ____| | | | (_) # | (___ | |_ _ __ __ _| |_ ___ __ _ _ ___ ___ # \___ \| __| '__/ _` | __/ _ \/ _` | |/ _ \/ __| # ____) | |_| | | (_| | || __/ (_| | | __/\__ \ # |_____/ \__|_| \__,_|\__\___|\__, |_|\___||___/ # __/ | # |___/ # #{END} #{BEGIN: perfect} # The perfect strategy # # It seems natural to interpret Move as part of some strategy. # For example, the perfect strategy is defined by # ps(n) = max{1, n mod 4} # in our game. # # We may implement handler *perfect* that assigns the ps to both # players: sig perfect : (Comp({Move:(Player,Int) {}-> Int |e}, a)) -> Comp({Move{_} |e}, a) fun perfect(m)() { handle(m) { case Return(x) -> x case Move(p,n,k) -> k( maximum(1, n `mod` 4) ) } } # Example game with n = 5 var ex5 = example( perfect(game(5)) ); # Example game with n = 7 var ex6 = example ( perfect(game(7)) ); # Example game with n = 12 var ex7 = example ( perfect(game(12)) ); #{END} #{BEGIN: perfect-sugar} # Syntactic sugar # # The abstract-over-handle idiom is so common that we provide some # syntactic sugar for it: sig perfect_s : (Comp({Move:(Player,Int) {}-> Int |e}, a)) -> Comp({Move{_} |e}, a) handler perfect_s { case Return(x) -> x case Move(p,n,k) -> k( maximum(1, n `mod` 4) ) } #{END} #{BEGIN: strategy} # Generic strategy handler # # Handlers are first-class citizens. We may define a generic strategy # handler that assigns a strategy s(p) to player p: fun strategy(s) { handler { case Return(x) -> x case Move(p,n,k) -> s(p)(n,k) } } #{END} #{BEGIN: ps} # The perfect strategy again # # Now, we can define ps as: fun ps(n,k) { k( maximum(1, n `mod` 4) ) } # Then, we can define perfect as: var perfect = strategy(const(ps)); # Here, const is a function that always returns its first argument. #{END} #{BEGIN: ms} # Mixed strategies # # We may implement *mixed* strategies using our generalised choice # function: fun ms(n, k) { var choice = chooseFrom( range(1,n) ); k(choice) } # Example of mixed vs mixed with n = 7 var ex8 = example( randomResult(strategy(const(ms))(game(7))) ); # All possible winners with n = 7 var ex9 = example( allResults(strategy(const(ms))(game(7))) ); #{END} #{BEGIN: gamedata} # _____ _ _____ _____ # | __ \ | | |_ _|_ _| _ # | |__) |_ _ _ __| |_ | | | | (_) # | ___/ _` | '__| __| | | | | # | | | (_| | | | |_ _| |_ _| |_ _ # |_| \__,_|_| \__| |_____|_____| (_) # # _____ _ _ _ _ # / ____| | | (_) | | | | # | | ___ _ __ ___ _ __ _ _| |_ _ _ __ __ _ __| | __ _| |_ __ _ # | | / _ \| '_ ` _ \| '_ \| | | | __| | '_ \ / _` | / _` |/ _` | __/ _` | # | |___| (_) | | | | | | |_) | |_| | |_| | | | | (_| | | (_| | (_| | || (_| | # \_____\___/|_| |_| |_| .__/ \__,_|\__|_|_| |_|\__, | \__,_|\__,_|\__\__,_| # | | __/ | # |_| |___/ # #{END} #{BEGIN: data-intro} # Computing game trees # # We may extend the idea of example 9 to compute data about the game. # # Let's define a handler that computes the game tree of a given game. # We define a game tree inductively: typename GameTree = [|Take:(Player,[(Int,GameTree)]) |Winner:(Player)|]; #{END} # Auxiliary function that computes the set of legal moves sig validMoves : (Int) ~> [Int] fun validMoves(n) { filter(fun(m) {m <= n}, [1,2,3]) } #{BEGIN: gametree} # Game tree handler # # The following handler generates a game tree for a given game # - The Return-clause generates leaf nodes. # - In the Move-clause we explore every possible by subgame, by invoking # the continuation multiple times. sig gametree : (Comp({Move:(Player,Int) {}-> Int |e}, Player)) -> Comp({Move{_} |e}, GameTree) handler gametree { case Return(x) -> Winner(x) case Move(p,n,k) -> var subgames = map(k, validMoves(n)); var subtrees = zip([1,2,3], subgames); Take(p, subtrees) } # Example with n = 3 var ex10 = example( gametree(game(3)) ); #{END} #{BEGIN: cheat-detection} # _____ _ _____ _____ _____ # | __ \ | | |_ _|_ _|_ _| _ # | |__) |_ _ _ __| |_ | | | | | | (_) # | ___/ _` | '__| __| | | | | | | # | | | (_| | | | |_ _| |_ _| |_ _| |_ _ # |_| \__,_|_| \__| |_____|_____|_____| (_) # # _____ _ _ _ _ _ _ # / ____| | | | | | | | | | (_) # | | | |__ ___ __ _| |_ __| | ___| |_ ___ ___| |_ _ ___ _ __ # | | | '_ \ / _ \/ _` | __| / _` |/ _ \ __/ _ \/ __| __| |/ _ \| '_ \ # | |____| | | | __/ (_| | |_ | (_| | __/ || __/ (__| |_| | (_) | | | | # \_____|_| |_|\___|\__,_|\__| \__,_|\___|\__\___|\___|\__|_|\___/|_| |_| # #{END} #{BEGIN: cheat-strategy} # A cheating strategy # # It is very easy to cheat in our game. An example of a cheating # strategy is: fun cs(n,k) { k(n) } # Any player playing cs will win any game in a single move. #{END} #{BEGIN: bobCheats} # Bob cheats # # Here's a strategy function that assigns cs to Bob: fun bobCheats(p) { switch (p) { case Alice -> ps case Bob -> cs } } # Example of Bob cheating with n = 7 var ex11 = example( strategy(bobCheats)(game(7)) ); #{END} #{BEGIN: cheat} # Cheat as an exception # # We introduce a new operation: cheat. # It's intended to signal that a cheater has been caught: typename Zero = [||]; sig cheat : (Player) {Cheat:(Player) {}-> Zero|_}-> _ fun cheat(p) { switch (do Cheat(p)) { } } # The codomain of Cheat is the empty type Zero, thus an invocation of # Cheat may never return. In fact, Cheat is an instance of an # exception. Exceptions are algebraic effects that never returns # control to its caller. #{END} sig checker : (Comp({Cheat:(Player) {}-> Zero, Move: (Player,Int) {}-> Int|e},a)) -> Comp({Cheat:(Player) {}-> Zero, Move: (Player,Int) {}-> Int|e},a) #{BEGIN: checker} # Analysing moves # # We need some mechanism to check whether cheating has occurred. # To achieve this we introduce *yet another layer of indirection*. # # The checker analyses the moves of players. If a player perform an # illegal move, then the player gets reported: handler checker { case Return(x) -> x case Move(p,n,k) -> var m = move(p,n); if (m `elem` validMoves(n)) k(m) # Everything's OK. else cheat(p) # Cheating detected! } #{END} #{BEGIN: cheatReport} # Reporting cheaters # # Finally, we need some mechanism for handling the Cheat operation. # # Let us treat Cheat as a fatal exception that prints the cheater's # name, and afterwards halts the program: sig cheatReport : (Comp({Cheat:(Player) {}-> Zero|e},a)) -> Comp({Cheat{p}|e},a) handler cheatReport { case Return(x) -> x case Cheat(p,_) -> error(showPlayer(p) ^^ " was caught cheating!") } #{END} #{BEGIN: combinators} # Convenient combinators # # Small aside: We now have so many handlers that we run into a # "parenthesis-hell" when applying them. To prevent us from going # insane, we define two combinators for handlers: op h -<- g { fun(m) { h(g(m)) } } op h -< m { h(m) } #{END} #{BEGIN: cheating-examples} # Examples using cheat detection # # Here's an example using our cheat detection mechanism: var ex12 = example( cheatReport -<- randomResult -<- strategy(bobCheats) -<- checker -< game(7) ); # Though, we have to be careful about the ordering of handlers: var ex13 = example( cheatReport -<- randomResult -<- checker -<- strategy(bobCheats) -< game(7) ); #{END} #{BEGIN: scoreboard} # _____ _ _______ __ # | __ \ | | |_ _\ \ / / _ # | |__) |_ _ _ __| |_ | | \ \ / / (_) # | ___/ _` | '__| __| | | \ \/ / # | | | (_| | | | |_ _| |_ \ / _ # |_| \__,_|_| \__| |_____| \/ (_) # # _____ _ _ # / ____| | | | | # | (___ ___ ___ _ __ ___| |__ ___ __ _ _ __ __| | # \___ \ / __/ _ \| '__/ _ \ '_ \ / _ \ / _` | '__/ _` | # ____) | (_| (_) | | | __/ |_) | (_) | (_| | | | (_| | # |_____/ \___\___/|_| \___|_.__/ \___/ \__,_|_| \__,_| # #{END} #{BEGIN: conclusion} # Conclusion # # Algebraic effects and handlers provide a modular abstraction for # effectful programming. # # The open world assumption of handlers enables us to do type-safe # generic programming. # # This style of programming let's us focus on the core of our model, # and then iteratively extend it. # #{END} #{BEGIN: epilogue} # Connection to concurrency and parallelism: ... #{END} #print(showPlayer(run(randomResult(strategy(fun(_) { ms })(game(5))))))