# This file is meant to be read in presentation mode. # Convenient function to mark examples. fun example(m)() { m() } fun undefined() { error("Undefined: Did you forget to reload the slides?") } # Composition operators op h -<- g { fun(m) { h(g(m)) } } op h -< m { h(m) } #! # # Liberating Effects with Rows and Handlers # # Daniel Hillerström and Sam Lindley # The University of Edinburgh, UK # # TyDe'16, Nara, Japan # #? #! # # Introduction # # Monads are a successful abstraction for effectful programming # [Moggi, 1991; Wadler, 1992]. # # Monadic effectful computations do not compose in general. # [Kammar, Lindley, and Oury, 2013; Kiselyov, Sabry, and Swords 2013]. # # Algebraic effects [Plotkin and Power, 2001] combined with handlers # [Plotkin and Pretnar, 2013] provide a modular alternative to monads. # # We say [Hillerström and Lindley, 2016]: # * to be modular an effect type system must support extensible # effects. # * the required abstraction to implement extensible effects and # their handlers is exactly row polymorphism. # #? #! # # About this Talk # # In this talk: # * A taster of programming with row-polymorphic algebraic effects and # handlers in Links. # * These "slides" are in fact a runnable Links program. # # In the paper: # * Mathematical game Nim as an example of programming with handlers. # * Implementation based on a generalised CEK machine. # * Operational semantics and abstract machine semantics. # * Proof that the two semantics coincide. # #? #! # # Links # # Links is a functional research web-programming language # [Cooper, Lindley, Wadler, and Yallop, 2006]: # * Single source language for multi-tier web-programming. # * Syntax reminiscent of JavaScript, e.g. fun uncurriedAdd(x,y) { x + y } fun curriedAdd(x)(y){ x + y } # * Statically typed with Hindley-Milner type inference. # * Comprises three backends: # - a JavaScript compiler for client-side code, # - an interpreter for server-side code, # - and a SQL generator for database code. # * Effect system used to track whether a computation can run in the # front-, back-, or database-end. # #? # # # Motivation # # Many programs comprise an *effectful* component that may # - raise exceptions, # - perform input/output, # - mutate some state, # - spawn processes, # - be non-determinism, # - ... and so forth # # In most programming languages effects are dealt with *implicitly*. # # Algebraic effects combined with handlers provide a modular # abstraction for modelling and controlling user-defined computational # effects such as the aforementioned. # # sig chooseSlide0 : () # # # Algebraic Effects # # An algebraic effect is a collection of abstract operations. For # example, nondeterminism is an algebraic effect given by single # nondeterministic choose operation: {Choose:Bool} # -> Bool fun chooseSlide0() { #! # # Algebraic Effects # # An algebraic effect is a collection of abstract operations. For # example, nondeterminism is given by a single operation `Choose'. # # In Links, an abstract operation is invoked using the `do' primitive: # do Choose #? } # # # Effect Signatures # # We can abstract over the invocation of operations by using # functions. In Links, a function definition begins with the `fun' # keyword, and we may assign it a type using the `sig' keyword: sig choose : () {Choose:Bool |e}-> Bool fun choose() { do Choose } # Here `e' is a row variable which may be instantiated to contain # additional operations. This is to say, that `choose' may be used in # the presence of other effects. # # #! # # A Coin Toss [Kammar, Lindley, and Oury, 2013] # # We may use `Choose' to model a coin toss, e.g. typename Toss = [|Heads|Tails|]; # Variant type with two constructors sig toss : () -%e-> Toss fun toss() { if (do Choose) Heads else Tails } # The variable `e' is a row variable. Links uses Remy-style row # polymorphism [Remy, 1993] to implement extensible effect signatures. # Let us try to evaluate this computation. var ex1 = toss; #? # # # Abstract Computations # # Evaluation of `toss' throws "Unhandled operation: Choose" right at us. # # Thus far we have only considered the *syntax* of effects. We say # that `toss' is an *abstract computation*. # # How can we turn `toss' into a *concrete* computation? # # # # # Syntax of effectful computations # # Thus far we have only considered the *syntax* of effects. # Visually, we may depict `toss` as computation tree, e.g. # # Choose # /\ # true / \ false # / \ # Heads Tails # # Internal nodes: Operation names # Edges: Labelled with return values of the origin operation # Leaves: Return values of the abstract computation # # A handler consists of a collection of clauses, in this case two: # # 1) A Return clause which determines how to handle the # return value `x' of the computation `m', # 2) and an operation clause `Choose' which determines # how to handle the said operation in `m'. # #! # # Effect Handlers # # An effect handler is a modular interpreter for computations. # # As an example consider a random interpretation of `Choose': handler randomResult { case Return(x) -> x case Choose(resume) -> resume(random() > 0.5) } # The operation clause `Choose' expose a function `resume' which is # the delimited continuation of the operation in the handled # computation. # # Using `randomResult' to interpret `toss': var ex2 = randomResult(toss); #? # I am cheating a bit here. sig randomResult0 : (() {Choose:Bool |e}~> a) -> () {Choose{_} |e}~> a handler randomResult0 { case Return(x) -> x case Choose(resume) -> resume(random() > 0.5) } var ex2 = randomResult0(toss); # # # Instantiation of Abstract Computations # # Using `randomResult' we may interpret `toss': #var ex2 = example( randomResult(toss) ); # #! # # Ascribing Types to Handlers # # What might the type of `randomResult' be? # What should we write in place of `e1' and `e2'? sig randomResult : (() -%e1-> a) -> () -%e2-> a handler randomResult { case Return(x) -> x case Choose(resume) -> resume(random() > 0.5) } #? #! # # An Enumerative Interpretation # # The application `randomResult(toss)' yields a computation which # returns *either* `Heads' or `Tails'. # # Alternatively, we can give an interpretation which enumerates the # possible outcomes of a computation: sig allChoices : (() {Choose:Bool |e}~> a) -> () {Choose- |e}~> [a] handler allChoices { case Return(x) -> [x] case Choose(resume) -> resume(true) ++ resume(false) } # An example of it in action var ex3 = allChoices(toss); #? # I'm cheating a bit here. Due to absence I'll not be able to evaluate `ex3' after evaluating `ex1'. sig allChoices0 : (() {Choose:Bool |e}~> a) -> () {Choose{_} |e}~> [a] handler allChoices0 { case Return(x) -> [x] case Choose(resume) -> resume(true) ++ resume(false) } var ex3 = allChoices0(toss); #! # # Exceptions # # Let us introduce another abstract operation `Fail': typename Zero = [||]; # The empty type sig fail : forall a::Type . () {Fail:Zero |e}-> a fun fail() { switch (do Fail) { } } # Because `Fail' returns an element of the empty type `Zero', then an # invocation of `fail' amounts to raising an exception. # #? #! # # A Drunk Coin Toss # # We can use `toss' and `fail' to model a drunkard tossing a coin: sig drunkToss : () -%e-> Toss fun drunkToss() { if (do Choose) toss() # Performs `Choose' else fail() # Performs `Fail' } # The two branches of `drunkToss' perform different effects. So, what # might the effect signature of `drunkToss' be? # # Recall sig toss : () {Choose:Bool |e}-> Toss # Note: We only mention `Choose' once in `drunkToss'. Alternative # systems permit multiple occurrences e.g. Koka [Leijen, 2014]. #? var toss = toss; #! # # Partial Interpretations # # With `randomResult' and `allChoices' we may only give a partial # interpretation of `drunkToss', e.g. # This one will not succeed: var ex4 = allChoices(drunkToss); # Maybe we get lucky: var ex5 = randomResult(drunkToss); #? var ex4 = allChoices0(drunkToss); var ex5 = randomResult0(drunkToss); # While we could include a `Fail' clause in `allChoices', a better and # more modular alternative is to define a separate handler for `Fail' # and then compose it with a handler for `Choose' in order to fully # interpret `drunkToss'. # #! # # Modular Interpretations # # We define a handler that models the possibility of failure as a # Maybe-value: typename Maybe(a) = [|Just:a|Nothing|]; # Maybe type constructor sig maybeResult : (() {Fail:Zero |e}~> a) -> () {Fail- |e}~> Maybe(a) handler maybeResult { case Return(x) -> Just(x) case Fail(_) -> Nothing } #? sig maybeResult0 : (() {Fail:Zero |e}~> a) -> () {Fail{_} |e}~> Maybe(a) handler maybeResult0 { case Return(x) -> Just(x) case Fail(_) -> Nothing } #! # # Drunk Coin Tossing # # Now, we can fully interpret `drunkToss': sig ex6 : () {Choose-,Fail- |e}~> [Maybe (Toss)] fun ex6() { (allChoices -<- maybeResult -< drunkToss)() } # the opposite composition: sig ex7 : () {Choose-,Fail- |e}~> Maybe ([Toss]) fun ex7() { (maybeResult -<- allChoices -< drunkToss)() } # with `randomResult': sig ex8 : () {Choose-,Fail- |e}~> Maybe (Toss) fun ex8() { (randomResult -<- maybeResult -< drunkToss)() } #? var ex6 = allChoices0 -<- maybeResult0 -< drunkToss; var ex7 = maybeResult0 -<- allChoices0 -< drunkToss; var ex7_toss = maybeResult0 -<- allChoices0 -< toss; var ex8 = randomResult0 -<- maybeResult0 -< drunkToss; # # # Stateful Interpretations (I) # # Nondeterminism and failure both comprise a single operation. But, # algebraic effects may in general consist of more operations. # # A canonical example of this is *state* which consists of two # operations: # State retrieval sig get : () {Get:s|_}-> s fun get() { do Get } # State update sig put : (s) {Put:(s) {}-> ()|_}-> () fun put(s) { do Put(s) } # Note: Empty effect signature on `Put', because any effects it may # have are conferred by its handler. # # Replay computation fun replay(n)(m)() { if (n <= 0) () else { var _ = m(); replay(n-1)(m)() } } # # # Stateful Interpretations (II) # # Say, we want to log the outcomes of `drunkToss'. To achieve this we # define a stateful post-processing handler: sig logOutcome : (() {Get:[a],Put:([a]) {}-> () |e}~> a) -> () {Get:[a],Put:([a]) {}-> () |e}~> () handler logOutcome { case Return(x) -> put(x :: get()) } # # # # Stateful Interpretations (III) # # To thread state through a program, we may use a *parameterised* # handler, e.g. # sig runState : (s) -> (() {Get:s ,Put:(s) {}-> () |e}~> a) -> () {Get{_},Put{_} |e}~> (a,s) handler runState(s) { case Return(x) -> (x,s) case Get(resume) -> undefined() case Put(p,resume) -> undefined() } # What should we write in place of `undefined()'? # # # # # Stateful Interpretations (IV) # # Here is an example which logs the outcomes of `n' drunk tosses: sig logDrunkToss : (Int) -> () {Choose:Bool,Fail{_},Get{_},Put{_}|_}~> [Maybe (Toss)] fun logDrunkToss(n)() { # var (_, s) = runState([]) # state handler; # (replay(n) # evaluates a comp. `n' times; # (logOutcome # logs the outcome of a comp; # (maybeResult # exception handler. # (drunkToss))))(); # s undefined() } # According to its effect signature the computation is only partially # instantiated. We need to pick an interpretation of `Choose'. # # #! # # Summary and Future Work # # We have briefly seen that # * Row polymorphism provides a neat abstraction for extensible # effects. # * Effectful computations compose smoothly. # * Handlers provide modular interpretations of effects. # # See the paper for # * The Nim game as another example of programming # with handlers. # * Examples with presence polymorphism (c.f. cheat detection). # * Formalisation: operational semantics, type system, soundness, etc. # * The implementation details (CEK machine). # # Future Work # * A compiler for server-side Links with effect handlers # (see my ML talk on Thursday). # * Type-and-effect directed optimisations of handlers. # * Extend the effect handlers to the client-side. # #? #! # # Thanks / Acknowledgements # # Hillerström was supported by EPSRC grant EP/L01503X/1 (The # University of Edinburgh CDT in Pervasive Parallelism). # # Lindley was supported by EPSRC grant EP/K034413/1 (A Basis for # Concurrency and Distribution). # #? #! # # References # # Moggi, "Notions of Computations and Monads", IC 1991. # # Wadler, "Essence of Functional Programming", POPL 1992. # # Rémy, "Type Inference for a Natural Extension of ML", TAOOP 1993. # # Plotkin and Power, "Adequacy for Algebraic Effects", FoSSaCS 2001. # # Cooper, Lindley, Wadler, and Yallop "Links: Web Programming Without Tiers", FMCO 2006. # # Kammar, Lindley, and Oury, "Handlers in Action", ICFP 2013. # # Kiselyov, Sabry, and Swords, "Extensible Effects", Haskell 2013. # # Plotkin and Pretnar, "Handling Algebraic Effects", LMCS 2013. # # Leijen, "Koka: Programming with Row Polymorphic Effect Types", MSFP 2014. # # Hillerström and Lindley, "Liberating Effects with Rows and Handlers", TyDe 2016. # #?