Algebraic Effects in Interaction Nets

README.md

Algebraic Effects in Interaction Nets

(Borrowing terminology from https://unison-lang.org/, which is what prompted me to think about / write this.)

Scroll down to "Examples" to see how this would be used in practice.

The representation of abilities uses mutable references, a primitive that can be expressed naturally in interaction combinators. Here, they're implemented using scopeless lambdas, but the ergonomics leave something to be desired -- one must explicitly call ref.split and ref.drop when using references non-linearly.

With compiler support for mutable references (which, I'll note, would not even need to be type-directed), I think this would be a quite ergonomic experience.

Four different effects are implemented here as examples:

• Try, implementing fallibility
• Store, implementing mutable state ¹
• Branch, implementing non-deterministic choice
• Seer, implementing mutable state with reverse causality (i.e. values set "in the future" appear "in the past")²

Note that there's a bug in current hvm-lang that will cause this program to print * indefinitely; for now, one can run on commit a3362b2.

The output of the program is as follows:

---------Try---------
(Ok 123)
(Err "uh oh")
(Ok (Node (Node (Leaf 1) (Leaf 2)) (Leaf 3)))
(Err it_was_zero)
(Err it_was_zero)
---------Store---------
(1, 2)
---------Branch---------
(Node (Node (Leaf 0) (Leaf 1)) (Node (Leaf 2) (Leaf 3)))
---------Seer---------
((Some 123), None)
---------All-Together-Now---------
(Node (Node (Node (Leaf (Err it_was_zero)) (Leaf (Ok 1))) (Node (Leaf (Ok 2)) (Leaf (Ok 3)))) (Node (Node (Leaf (Ok 4)) (Leaf (Ok 5))) (Node (Leaf (Ok 6)) (Leaf (Ok 7)))))

Footnotes

1. This specific effect is kind of pointless in this context, given that the whole effect system is based on mutable references, which could be used directly instead. But it remains a good example of the ways in which this can be used. ↩

2. Just be careful not to cause temporal paradoxes, which will create vicious circles. ↩

abilities.hvml

// --- Mutable References --- //
  // &a = @$final initial

  // ref.mut : &a -> (a -> a) -> ()
  ref.mut ref fn = (@$new * (fn (ref $new)))

  // these would ideally be automatically inserted by a compiler (a la implicit dups/erase):
    // ref.split : &a -> (&a, &a)
    ref.split ref = let x = (ref $z); (@$y x, @$z $y)
    // ref.drop : &a -> ()
    ref.drop ref = (@$x * (ref $x))

// --- Abilities & Handlers --- //
  data Request = (Request.pure value) | (Request.yield data resume)

  // yield : {A} -> A -> A.return
  yield ability data = (
    do (ref.mut ability @fn
      let handler = (fn $out);
      let out = (handler (Request.yield data @$handler @$cont $value));
      @$value (@$out $handler out)
    )
    $cont
  )

  // handle : ({A} -> t) -> (Request A t -> u) -> u
  handle cb handler =
    let value = (cb (@$fin @$out handler))
    let handler = ($fin $val);
    let val = (handler (Request.pure value));
    (@$val $out val)

// --- Try --- //
  data Try
    = (Try.throw. err) // -> !

  // Try.throw : {Try e} -> e -> !
  Try.throw .t err = (yield .t (Try.throw. err))

  // Try : ({Try e} -> t) -> Result t e
  Try cb = (handle cb Try.handler)

  // Try.handler : Request e t -> Result t e
  Try.handler (Request.pure value) = (Ok value)
  Try.handler (Request.yield (Try.throw. err) *) = (Err err)

  // --- Usage --- //
    // validate : {Try String} -> Tree Nat -> Tree PosNat
    (validate .t (Leaf x)) = (Leaf (validate.n .t x))
    (validate .t (Node x y)) =
      let (.t0, .t1) = (ref.split .t);
      (Node (validate .t0 x) (validate .t1 y))

    // validate : {Try String} -> Nat -> PosNat
    (validate.n .t 0) = (Try.throw .t it_was_zero)
    (validate.n .t n) = (do (ref.drop .t) n)

    Option.unwrap .t (Some x) = (do (ref.drop .t) x)
    Option.unwrap .t None = (Try.throw .t unexpected_none)


// --- Store --- //
  data Store
    = (Store.set. val) // -> ()
    | (Store.get.) // -> t
  
  Store.get .s = (yield .s Store.get.)
  Store.set .s val = (yield .s (Store.set. val))
  
  Store init cb = (handle cb (Store.handler init))

  Store.handler * (Request.pure value) = value
  Store.handler * (Request.yield (Store.set. held) resume) = (resume (Store.handler held) *)
  Store.handler held (Request.yield (Store.get.) resume) = (resume (Store.handler held) held)


// --- Branch --- //
  data Branch
    = Branch.branch. // -> 0 | 1
  
  Branch.branch .b = (yield .b Branch.branch.)
  
  Branch cb = (handle cb Branch.handler)

  Branch.handler (Request.pure value) = (Leaf value)
  Branch.handler (Request.yield Branch.branch. resume) = (Node
    (resume Branch.handler 0)
    (resume Branch.handler 1)
  )


// --- Seer --- //
  data Seer
    = (Seer.prophesize.) // -> t
    | (Seer.fulfill. x) // -> ()

  Seer.prophesize .S = (yield .S Seer.prophesize.)
  Seer.fulfill .S x = (yield .S (Seer.fulfill. x))
  
  Seer cb = (handle cb (Seer.handler *))

  Seer.handler back (Request.pure value) = (do (back None) value)
  Seer.handler back (Request.yield (Seer.fulfill. x) resume) = (do (back (Some x)) (resume (Seer.handler *) *))
  Seer.handler back (Request.yield (Seer.prophesize.) resume) = let v = $val; (resume (Seer.handler @$val (back v)) v)


// --- Examples --- //
  main = (print_list @x x [
    ---------Try---------
    (Try @.t (do (ref.drop .t) 123))
    (Try @.t (Try.throw .t "uh oh"))
    (Try @.t (validate .t (Node (Node (Leaf 1) (Leaf 2)) (Leaf 3))))
    (Try @.t (validate .t (Node (Node (Leaf 1) (Leaf 0)) (Leaf 3))))
    (Try @.t (validate .t (Node (Node (Leaf 0) (Leaf 0)) (Leaf 0))))
    ---------Store---------
    (Store 1 @.s let (.s0, .s) = (ref.split .s); let (.s1, .s2) = (ref.split .s);
      let a = (Store.get .s0);
      (do (Store.set .s1 2)
      let b = (Store.get .s2);
      (a, b)
    ))
    ---------Branch---------
    (Branch @.b let (.b0, .b1) = (ref.split .b);
      let a = (Branch.branch .b0);
      let b = (Branch.branch .b1);
      (+ (* a 2) b)
    )
    ---------Seer---------
    (Seer @.S let (.S0, .S) = (ref.split .S); let (.S1, .S2) = (ref.split .S);
      let a = (Seer.prophesize .S0); // sees the future :O
      (do (Seer.fulfill .S1 123) // the prophecy is fulfilled
      let b = (Seer.prophesize .S2); // the end is nigh!
      (a, b)
    ))
    ---------All-Together-Now---------
    (Branch  @.b let (.b0, .b) = (ref.split .b); let (.b1, .b2) = (ref.split .b);
    (Try     @.t let (.t0, .t) = (ref.split .t); let (.t1, .t2) = (ref.split .t);
    (Seer    @.S let (.S0, .S) = (ref.split .S); let (.S1, .S2) = (ref.split .S);
    (Store 1 @.s let (.s0, .s1) = (ref.split .s);
      let x = (Branch.branch .b0);
      let y = (Branch.branch .b1);
      (do (Store.set .s0 (Branch.branch .b2))
      let x = (* x (Option.unwrap .t0 (Seer.prophesize .S0)));
      let x = (+ x y);
      let x = (* x (Option.unwrap .t1 (Seer.prophesize .S1)));
      (do (Seer.fulfill .S2 2)
      let x = (+ x (Store.get .s1));
      (validate.n .t2 x)
    ))))))
  ])




// --- Utilities --- //
  data Tree = (Leaf n) | (Node x y)
  data Option = (Some x) | None
  data Result_ = (Ok val) | (Err err)

  do * x = x

  print_list k (List.cons h t) = (print_list (k HVM.log h) t)
  print_list k (List.nil) = (k HVM.exit 0)

  it_was_zero = "it was zero :("
  unexpected_none = "unexpected none?!"

  ---------Try--------- = *
  ---------Store--------- = *
  ---------Branch--------- = *
  ---------Seer--------- = *
  ---------All-Together-Now--------- = *