Monadic User-Defined Effects in Koka

“Taking control of the semicolon”

Niki Vazou
Mentor: Daan Leijen

1. Async code can be tricky to program

async sync

2. Effectful code is generally tricky

Similar examples:

A parser that needs current input and failure modes.
Ambiguous computations that return a distribution of values.
An interpreter that needs an environment and logging.
… and many others

Goal: A very generic abstraction mechanism that is (type) safe!

Status: Success! (Prototype implementation on top of Koka)

3. Koka

javascript-like syntax
compiles to javascript
strongly typed
tracks effects (eg., exception, divergence, heap …)

4. The exception Effect: Creation

“For all integers x,y, x/y will return an integer or throw an exception”

function (/)  (x :int, y :int) : exn int

5. The exception Effect: Usage

function effectful() : exn int {
  val p = 42 / 2;
  val q = 42 / 0;
  p + q               // p, q : int
}

The exn effect is propagated to user functions
p and q are pure integer values

6. The exception Effect: Discharge

function pure() : int {
   catch(effectful, fun(err){0})
}

If effectful throws an exception, return 0

function catch (action : () -> exn a, handler: exception -> a): a

7. Effects in koka

Special built-in effects: exn, div, io, …
Koka already has polymorphic effect inference
Now support for user-defined effects

User defined effects are not just introducing a new type, but are also a novel and powerful abstraction mechanism that
“let you take control of the semicolon”.

8. The Ambiguous effect : Creation

choice(x, y) ambiguously returns x or y

function choice( x : a, y : a) : amb a

9. The Ambiguous effect : Usage

function xor() : amb bool {
  val p = choice(False, True);
  val q = choice(False, True);
  (p||q) && not(p&&q)           // p, q : bool
}

The amb effect is propagated to user functions of choice
inside functions p and q are pure bool values

How do we evaluate xor?

10. The Ambiguous effect : Discharge

function run( action : () -> amb a ) : list<a>

run(action) returns the list of all ambiguous results of action

> run(xor) 

False
True 
True
False

11. The Ambiguous effect

amb is a monadic user-defined effect

images

12. What is a monad

$m$ is a monad if there exist functions $unit$ and $bind$ , such that

\begin{mdMathprearray}% \mathid{unit}\mathspace{1}:\mathspace{1}(\mathid{a})\mathspace{1}\rightarrow \mathid{m}\langle \mathid{a}\rangle\mathbr{} \mathid{bind}\mathspace{1}:\mathspace{1}(\mathid{x}:\mathid{m}{\langle}\mathid{a}{\rangle},\mathid{f}:(\mathid{a})\mathspace{1}\rightarrow \mathid{m}{\langle}\mathid{b}{\rangle}\mathspace{1})\mathspace{1}\rightarrow \mathid{m}{\langle}\mathid{b}{\rangle} \end{mdMathprearray}

Example: list is a monad!

function unit(x:a){[x]}

function bind(xs:list<a>, f:(a) -> list<b>): list<b>{
    match(xs) {
      Nil -> Nil
      Cons(y,ys) -> f(y) +  bind(ys, f)
    }
}

13. The Ambiguous Effect: Definition

The amb effect is a list with the monadic operators

effect amb<a> = list<a> { 
  function unit( x:a ) : list<a> {
    [x]
  }
  function bind( xs : list<a>, f : a -> list<b> ) : list<b>  {
    match(xs) {
      Nil -> Nil
      Cons(x,xx) -> f(x) +  xx.bind(f)
    }
  }  
}

koka automatically generates

function from_amb(action : () -> amb a) : list<a>   
function to_amb(xs:list<a>) : amb a

14. The Ambiguous effect : Primitive Operations

User Writes

function choice( x : a, y : a ) : amb a {
  to_amb( [x,y] )
}

function run( action : () -> amb a ) : list<a> {
  from_amb(action)
}

15. Example: Truth Tables

Demo

16. Revisiting the xor example

function xor() : amb bool{       //
  val p = choice(False, True);   //    p is a list<bool> of all the amb results
  val q = choice(False, True);   //    
  (p||q) && not(p&&q)            //    p is treated as a bool
}                                //

Take control of the semicolon!

semicolon

17. Revisiting the example

// source effectful code       
function xor() : amb bool{      
  val p = choice(False, True);  
  val q = choice(False, True);  
  (p||q) && not(p&&q)           
}

//translated monadic code  
function xor() : list<bool>{      
  choice(False, True).bind(fun(p){  
    choice(False, True).bind(fun(q){  
      unit((p||q) && not(p&&q)) 
  })})          
}

bind : (list<a>, (a) -> list<b>) -> list<b>   
unit : a -> list<a>

Which bind and unit should we use?

18. Effect Polymorphism

map is polymorphic on effects

function map(xs : list<a>, f : (a) -> e b) : e list<b> {
  match(xs) {
    Nil         -> Nil
    Cons(y, ys) -> val z = f(y);
                   val zs = map(ys, f);
                   Cons(z, zs)
  }
}

19. Effect Polymorphism

map is polymorphic on effects

// source effectful code               
function map(xs:list<a>, f:(a) -> e b): e list<b> {
  match(xs) {
    Nil         -> Nil 
    Cons(y, ys) ->         
         val z = f(y); 
         val zs = map(ys, f);
         Cons(z, zs)   
  }                                     
}

// translated monadic code  
function map(xs:list<a>, f:(a) -> e b): e list<b> {
  match(xs) {
    Nil         -> unit(Nil)
    Cons(y, ys) ->    
      f(y)       `bind` fun(z) {
      map(ys, f) `bind` fun(zs) {
      unit(Cons(z, zs)) 
  }}}}
}

Which bind and unit should we use?

20. Dictionaries

structures that contain bind and unit
automatically generated (hidden from the user)
effect polymorphic functions take them as extra argument
for every effect there exists a dictionary (ie, dict_amb)

21. Dictionary abstraction

map is effect polymorphic on e
internally takes d:dict(e) as extra argument

// source effectful code       
function map(xs:list<a>, f:(a) -> e b): e list<b> {
  match(xs) {
    Nil         -> Nil         
    Cons(y, ys) ->             
      val z = f(y);            
      val zs = map(d, ys, f)   
      Cons(z, zs)               
  }                            
}

// translated monadic code  
function map(d:dict<e>,xs,f)
  match(xs) {
    Nil         -> d.unit(Nil)
    Cons(y, ys) ->             
      f(y)       `d.bind` fun(z) {
      map(d, ys, f) `d.bind` fun(zs) {
      unit(Cons(z, zs)) 
  }}}
}

22. Dictionary application: User-defined Effects

function map : forall a b e. (xs:list<a>, f:(a) -> e b) -> e list<b>
function booltodoubles: (bool) ->  amb double;

map(xs, booltodoubles)

koka intermediate effectfull code

map<bool, double, amb>(xs, booltodoubles)

translated koka intermediate monadic code

map<bool, double, amb>(dict_amb, xs, booltodoubles)

23. Dictionary application: Non User-defined Effects

function map : forall<a,b,e> ( list<a>, (a) -> e b) -> e list<b>
function booltodouble: (bool) -> double;

map(xs, booltodouble)

koka intermediate effectfull code

map<bool, double, total>(xs, booltodouble)

translated koka intermediate monadic code

map<bool, double, total>(dict_id, xs, booltodouble)

24. Wrap Up

Type-directed translation
- from effectful code
- to monadic code
- using dictionaries
Monadic User-Defined Effects
- ambiguous
- parser
- async
- …
Thank you!