Brandon Bloom on Programming with Algebraic Effects and Handlers by Andrej Bauer and Matija Pretnar

Some great papers embody insights, others package up those insights into digestible bites. "Programing with Algebraic Effects and Handlers" is the later sort of great paper. After two decades of fundamental research in to the nature of computation, a lot of mysterious ideas in computer science such as continuations and exception handling finally made sense to a number of mathematically inclined geniuses. Bauer and Pretnar's Eff programming language cuts right through the heart of the theory in a way that makes sense to anybody who has ever written a functional program. This paper uses the Eff language to explore a number of simple computational effects that were traditionally viewed as quite varied and complex.

Transcript

1. Programing With Algebraic Effects ! Authors: Andrej Bauer & Matija Pretnar! http://math.andrej.com/eff/ ! ! ! Presenter: Brandon Bloom @brandonbloom
2. Programing With Algebraic Effects ! Authors: Andrej Bauer & Matija Pretnar! http://math.andrej.com/eff/ ! ! ! Presenter: Brandon Bloom @brandonbloom
3. Talk Outline • Definitions & Background • The Eff Language • Eff’s Unique Constructs • Examples of Effects & Handlers
4. What are “Effects”? Useful programs do either or both of these: 1. Return answers 2. Affect other systems effects are about this! types are about these…
5. What’s “Algebraic” mean? Pertaining to an “algebra” • …with useful properties and equational theories • Math way outside the scope of this talk
6. What’s “Algebraic” mean? Ostensibly: Amenable to formal reasoning ! Pragmatically: Amenable to informal reasoning
7. Algebraic Effects • Algebraic Effects are to Effect Systems
 as Algebraic Data Types are to Type Systems • They enable useful reasoning about how programs affect their dynamic environments
8. cf. Monads Eff is a programming language based on the algebraic approach to effects, in which computational effects are modelled as operations of a suitably chosen algebraic the- ory [12]. Common computational effects such as input, output, state, exceptions, and non-determinism, are of this kind. Continuations are not algebraic [4], but they turn out to be naturally supported by eff as well. Effect handlers are a related notion [14, 17] which encompasses exception handlers, stream redirection, transactions, backtracking, and many others. These are modelled as homomorphisms induced by the universal property of free algebras. Because an algebraic theory gives rise to a monad [11], algebraic effects are sub- sumed by the monadic approach to computational effects [1]. They have their own virtues, though. Effects are combined more easily than monads [5], and the interaction between effects and handlers offers new ways of programming. An experiment in the design of a programming language based on the algebraic approach therefore seems warranted. Philip Wadler once opined [19] that monads as a programming concept would not have been discovered without their category-theoretic counterparts, but once they were, programmers could live in blissful ignorance of their origin. Because the same holds 1 “ ” Monads don’t compose! See: Monad Transformer Stacks
9. • Constrain the world inside • I’ll give you a T • What the function computes • Constrain the world outside • You’ll handle Es • How the function computes + Effects Types
10. Analogy #1: Exceptions • Checked Exceptions (Java and C++) • A sucky and broken effect system • throws clauses spread like a virus (also true of monads) • Generalization: Common Lisp Conditions • http://www.gigamonkeys.com/book/beyond-exception- handling-conditions-and-restarts.html
11. Background: Continuations Represents “the rest of the computation” Think of “a program with a hole in it” (f  (g  x)  (h  y))   ! (f  □  (h  y))
12. • Widely useful in compilers, historically • “Continuation Passing Style” enables many useful program transformations • Static-Single Assignment now more popular • Unrealized potential in applications • Traditionally, very hard to teach or learn • “The goto of functional programming” • aka JavaScript/Node.js people are insane
13. Delimited Continuations • Also called “composable continuations” • Behave like call, not jump • Undelimited (aka “full”) continuations… • are less expressive (you need state too) • don’t exist in practice • See “An argument against call/cc” (Oleg)
14. Analogy #2: System Calls • Unlike standard calls, syscalls yield to the kernel • The abort() function never returns. • The fork() function returns twice! • Your entire process is a delimited continuation • System calls are parameterized “effects” • The process itself is a parameter • OS virtualization works by mocking syscall interface
15. Analogy #3: Yield • In service of Iterators, Enumerators, Generators, etc. • Ruby, Python, JavaScript, C# and others have some form of yield, but… • Each lacks some expressivity of the others • A generalized variant of yield is equivalent to monads and delimited continuations • See this other great paper:
 Roshan P. James and Amr Sabry.
 Yield: Mainstream Delimited Continuations
16. Paper Outline The Eff Language! • Motivation (Intro) • Syntax • Unique constructs • Type checking • Denotational semantics Selected Examples! • Choice • Exceptions • State • Input and Output • Cooperative threads
17. Syntax Its types include products, sums, records, and recursive type definitions. To keep to the point, we focus on a core language with monomorphic types and type checking. The concrete syntax follows that of OCaml [6], and except for new constructs, we discuss it only briefly. 1.1 Types Apart from the standard types, eff has effect types E and handler types A ) B : A, B, C ::= int bool unit empty (type) A ⇥ B A + B A ! B E A ) B, E ::= effect ( operation opi : Ai ! Bi)i end. (effect type) In the rule for effect types and elsewhere below (· · · )i indicates that · · · may be re- peated a finite number of times. We include the empty type as we need it to describe exceptions, see Section 6.2. An effect type describes a collection of related operation symbols, for example those for writing to and reading from a communication channel. We write op : A ! B 2 E or just op 2 E to indicate that the effect type E contains an operation op with parameters of type A and results of type B . The handler type A ) B should be understood as the type of handlers acting on computations of type A and yielding computations of type B . 2 “The concrete syntax follows that of OCaml [6], and except for new constructs, we discuss it only briefly.” 1.2 Expressions and computations Eff distinguishes between expressions and computations, which are similar to values and producers of fine-grain call-by-value [7]. The former are inert and free from com- putational effects, including divergence, while the latter may diverge or cause computa- tional effects. As discussed in Section 5, the concrete syntax of eff hides the distinction and allows the programmer to freely mix expressions and computations. Beware that we use two kinds of vertical bars below: the tall separates grammat- ical alternatives, and the short | separates cases in handlers and match statements. The expressions are e ::= x n c true false () (e1, e2) (expression) Left e Right e fun x : A 7! c e # op h, h ::= handler ( ei # opi x k 7! ci)i | val x 7! cv | finally x 7! cf , (handler) where x signifies a variable, n an integer constant, and c other built-in constants. The expressions () , (e1, e2) , Left e , Right e , and fun x : A 7! c are introduction forms for the unit, product, sum, and function types, respectively. Operations e # op and handlers h are discussed in Section 2. The computations are c ::= val e let x = c1 in c2 let rec f x = c1 in c2 (computation) if e then c1 else c2 match e with match e with (x, y) 7! c match e with Left x 7! c1 | Right y 7! c2 e1 e2 1.2 Expressions and computations Eff distinguishes between expressions and computations, which are similar to values and producers of fine-grain call-by-value [7]. The former are inert and free from com- putational effects, including divergence, while the latter may diverge or cause computa- tional effects. As discussed in Section 5, the concrete syntax of eff hides the distinction and allows the programmer to freely mix expressions and computations. Beware that we use two kinds of vertical bars below: the tall separates grammat- ical alternatives, and the short | separates cases in handlers and match statements. The expressions are e ::= x n c true false () (e1, e2) (expression) Left e Right e fun x : A 7! c e # op h, h ::= handler ( ei # opi x k 7! ci)i | val x 7! cv | finally x 7! cf , (handler) where x signifies a variable, n an integer constant, and c other built-in constants. The expressions () , (e1, e2) , Left e , Right e , and fun x : A 7! c are introduction forms for the unit, product, sum, and function types, respectively. Operations e # op and handlers h are discussed in Section 2. The computations are c ::= val e let x = c1 in c2 let rec f x = c1 in c2 (computation) if e then c1 else c2 match e with match e with (x, y) 7! c match e with Left x 7! c1 | Right y 7! c2 e1 e2 new E new E @ e with ( operation opi x @ y 7! ci)i end with e handle c. An expression e is promoted to a computation with val e , but in the concrete syntax
18. Unique Constructs etc. The extended form of new creates an effect instance with an associated resource which determines the default behaviour of operations and is explained separately i Section 2.3. For each effect instance e of effect type E and an operation symbol op 2 E ther is an operation e # op , also known as a generic effect [12]. By itself, an operation is value, and hence effect-free, but an applied operation e # op e 0 is a computational effec whose ramifications are determined by enveloping handlers and the resource associate with e . 2.2 Handlers A handler h = handler ( ei # opi x k 7! ci)i | val x 7! cv | finally x 7! cf may be applied to a computation c with the handling construct with h handle c, (1 which works as follows (we ignore the finally clause for the moment): 1. If c evaluates to val e , (1) evaluates to cv with x bound to e . 2. If the evaluation of c encounters an operation ei # opi e , (1) evaluates to ci wit x bound to e and k bound to the continuation of ei # opi e , i.e., whatever remain i x bound to e and k bound to the continuation of ei # opi e , i.e., whatever remains to be computed after the operation. The continuation is delimited by (1) and is handled by h as well. The finally clause can be thought of as an outer wrapper which performs an addi- tional transformation, so that (1) is equivalent to let x = ( with h 0 handle c ) in cf where h 0 is like h without the finally clause. Such a wrapper is useful because we often perform the same transformation every time a given handler is applied. For ex- ample, the handler for state handles a computation by transforming it to a function ac- cepting the state, and finally applies the function to the initial state, see Section 6.3. If the evaluation of c encounters an operation e # op e 0 that is not listed in h , the control propagates to outer handling constructs, and eventually to the toplevel, where the behaviour is determined by the resource associated with e . 2.3 Resources The construct new E @ e with ( operation opi x @ y 7! ci)i end 4 it only briefly. 1.1 Types Apart from the standard types, eff has effect types E and handler types A ) B : A, B, C ::= int bool unit empty (type) A ⇥ B A + B A ! B E A ) B, E ::= effect ( operation opi : Ai ! Bi)i end. (effect type) In the rule for effect types and elsewhere below (· · · )i indicates that · · · may be re- peated a finite number of times. We include the empty type as we need it to describe exceptions, see Section 6.2. An effect type describes a collection of related operation symbols, for example those for writing to and reading from a communication channel. We write op : A ! B 2 E or just op 2 E to indicate that the effect type E contains an operation op with parameters of type A and results of type B . The handler type A ) B should be understood as the type of handlers acting on computations of type A and yielding computations of type B . 2
19. Example #1: Choice type  choice  =  effect      operation  decide  :  unit  -­‐>  bool   end   ! let  c  =  new  choice   ! !    let  x  =  (if  c#decide  ()  then  10  else  20)  in      let  y  =  (if  c#decide  ()  then  0  else  5)  in          x  -­‐  y   ! handle   ! ! ! with   |  c#decide  ()  k  -­‐>  k  true
20. let  choose_true  e  =  handler   |  e#decide  ()  k  -­‐>  k  true   ! with  choose_true  c  handle      let  x  =  (if  c#decide  ()  then  10  else  20)  in      let  y  =  (if  c#decide  ()  then  0  else  5)  in          x  -­‐  y
21. let  choose_true  e  =  handler   |  e#decide  ()  k  -­‐>  k  true   ! with  choose_true  c  handle      let  x  =  (if  c#decide  ()  then  10  else  20)  in      let  y  =  (if  c#decide  ()  then  0  else  5)  in          x  -­‐  y Answer: 10
22. let  choose_all  d  =  handler   |  d#decide  ()  k  -­‐>  k  true  @  k  false   |  val  x  -­‐>  [x]   ! with  choose_all  c  handle      let  x  =  (if  c#decide  ()  then  10  else  20)  in      let  y  =  (if  c#decide  ()  then  0  else  5)  in          x  -­‐  y   !
23. let  choose_all  d  =  handler   |  d#decide  ()  k  -­‐>  k  true  @  k  false   |  val  x  -­‐>  [x]   ! with  choose_all  c  handle      let  x  =  (if  c#decide  ()  then  10  else  20)  in      let  y  =  (if  c#decide  ()  then  0  else  5)  in          x  -­‐  y   ! Answer: [10;5;20;15]
24. let  choose_all  d  =  handler   |  d#decide  ()  k  -­‐>  k  true  @  k  false   |  val  x  -­‐>  [x]   ! let  c1  =  new  choice  in   let  c2  =  new  choice  in      with  choose_all  c1  handle      with  choose_all  c2  handle          let  x  =  (if  c1#decide  ()  then  10  else  20)  in          let  y  =  (if  c2#decide  ()  then  0  else  5)  in              x  -­‐  y   ! Answer: [[10;5];[20;15]]
25. Example #2: Exceptions type  'a  exception  =  effect      operation  raise  :  'a  -­‐>  empty   end
26. let  optionalize  e  =  handler   |  e#raise  a  k  -­‐>  None   |  val  x  -­‐>  Some  x   ! Effect instance divisionByZero is pre-defined ! with  optionalize  divisionByZero   handle  10  /  0   Answer: None ! with  optionalize  divisionByZero   handle  10  /  5   Answer: Some  2
27. Example #3: State type  'a  ref  =  effect      operation  lookup:  unit  -­‐>  'a      operation  update:  'a  -­‐>  unit   end   ! ! let  (!)  r  =  r#lookup  ()   let  (:=)  r  v  =  r#update  v
28. let  state  r  x  =  handler   |  val  y  -­‐>  (fun  s  -­‐>  y)   |  r#lookup  ()  k  -­‐>  (fun  s  -­‐>  k  s  s)   |  r#update  s'  k  -­‐>  (fun  s  -­‐>  k  ()  s')   |  finally  f  -­‐>  f  x   ! let  r  =  new  ref  in      with  state  r  5  handle          r  :=  !r  +  3;   Answer: 8
29. let  r  =  new  ref  in      (with  state  r  x  handle            computation);      r   Answer: <instance  #12>   !    !r   Runtime  error:  uncaught  operation   <instance  #12>.lookup  ()
30. let  ref  x  =  new  ref  @  x  with      operation  lookup  ()  @  s  -­‐>  (s,  s)      operation  update  s'  @  _  -­‐>  ((),  s')   end   ! let  r  =  ref  5  in      r  :=  !r  +  3  ;      !r   Answer: 8
31. Example #4: Input/Output type  channel  =  effect      operation  read  :  unit  -­‐>  string      operation  write  :  string  -­‐>  unit   end std is predefined: std#write <— stdout     std#read <— stdin   ! But we can intercept handlers!
32. let  accumulate  =  handler   |  std#write  x  k  -­‐>      let  (v,  xs)  =  k  ()  in  (v,  x  ::  xs)   |  val  v  -­‐>  (v,  [])   ! ! with  accumulate  handle      std#write  "hello";      std#write  "world";      3  *  14   Answer: (42,  ["hello";  "world"])
33. let  read_from_list  lst  =  handler      |  std#read  ()  k  -­‐>          (fun  (s::lst')  -­‐>  k  s  lst')      |  val  x  -­‐>  (fun  _  -­‐>  x)      |  finally  f  -­‐>  f  lst
34. Example #5:
 Cooperative Multithreading type  coop  =  effect      operation  yield  :  unit  -­‐>  unit      operation  fork  :  (unit  -­‐>  unit)  -­‐>  unit   end
35. let  round_robin  c  =      let  threads  =  ref  []  in      let  enqueue  t  =  threads  :=  !threads  @  [t]  in      let  dequeue  ()  =          match  !threads  with          |  []  -­‐>  ()          |  t  ::  ts  -­‐>  threads  :=  ts  ;  t  ()      in          let  rec  scheduler  ()  =  handler          |  c#yield  ()  k  -­‐>  enqueue  k  ;  dequeue  ()          |  c#fork  t  k  -­‐>              enqueue  k  ;              with  scheduler  ()  handle  t  ()          |  val  ()  -­‐>  dequeue  ()      in          scheduler  ()
37. Programing With Algebraic Effects ! Authors: Andrej Bauer & Matija Pretnar! http://math.andrej.com/eff/ ! ! ! Presenter: Brandon Bloom @brandonbloom