thoughts on effects and typestates

[ecioppettini]

Thoughts on how to represent stateful utxos

NOTE: This is not about proving, but I'm using the same idea underneath.

Background

Let's start by defining an object model based on effect systems, inspired by
the objects in effekt. Which is similar
to the way utxos methods work in Starstream's original design.

Note however that we can return these objects instead of having to write everything in CPS.

Basically we want to implement "methods" as effect handlers:

interface Object {
  foo(): u32
  bar(): String
}

def object = {
  def foo() = {
    1
  }

  def bar() = {
    "bar"
  }
}

let x = object.foo()
let y = object.bar()

Where this is the same as:

try {
  object.foo()
  object.bar()
}
with object: Object {
  def foo() = {
    1
  }

  def bar() = {
    "bar"
  }
}

In Starstream, we can implement that with something like this (in rusty
pseudo-code, but imagine wasm):

let mut (r, k) = yield();
loop {
  (r, k) = match r { // k is the caller
    Object::Foo => {
      resume(k, 1);
    }
    Object::Bar => {
      resume(k, "bar");
    }
  }
}

Where k is some handle to the coroutine that did call the method (it's
suspened on a resume call, and the input here is the output).

State

With that framework, let's say we want to implement a utxo with a typestate-like
interface.

Let's say with have a utxo (coroutine) with states A and B. Each one with its
own interface. A goes to B, and B goes to A.

interface A {
  a(): String
}

interface B {
  b(): String
}

On the runtime side, this can be implemented by chaining two handlers (TCO can
eliminate recursion):

struct Storage {}

fn utxo() {
  let storage = Storage::new();

  let (r, k) = yield();

  utxo_a(r, k, &storage);
}

fn utxo_a(r, k, storage: &Storage) {
    let (r, k) = match r {
      A::a => {
        resume(k, "a");
      }
      Star::Supports(i) => {
        resume(k, i == A::HASH);
      } 
      _ => abort("unsupported operation")
    };

    utxo_b(r, k, storage)
}

fn utxo_b(r, k, storage: &Storage) {
    let (r, k) = match r {
      B::b => {
        resume(k, "b");
      }
      Star::Supports(i) => {
        resume(k, i == B::HASH);
      } 
      _ => abort("unsupported operation")
    }

    utxo_a(r, k, storage)
}

On the coordination script side you could just do:

let s1 = utxo.a(); // moves the coroutine to the second yield
let s2 = utxo.b(); // goes back to the first yield
let s1 = utxo.a();

Where invoking an unavailable operation will just fail and abort the
transaction.

The main question then becomes how to describe the type of such utxo, for the
purposes of static checking mainly, and also how to make it ergonomic, since it
has to be checked in any case.

Par-inspired idea

Extend the effect system with trees (for typestates), inspired by session
types and Par
(although the following is not session types, that also requires duality for
deadlock freedom).

I don't think the indexed types idea necessarily applies only to channels,
although it's simpler with named handlers like the boxed computations described
above, than with just contextual effects.

fn utxo(): Coroutine<Rec{ A.B.Self }> { ... }

Where the . (dot) means chaining, Rec is used to type the loop operator
(there could be a different one).

Then this could be used like this:

let u = utxo();
// u: Coroutine<Rec{ A.B.Self }>
let s = u.a();
// unfold Rec
// u: Coroutine<B.Rec{ A.B.Self }>
let s = u.b();
// back to the beginning
// u: Coroutine<Rec { A.B.Self }>
let s = u.a();

I think this is not super hard to type-check. The type of u changes across the
function, but I think that could be implemented by updating the type environment
(Γ), like some sort of flow typing, or maybe by desugaring u into unique
variables.

This also subsumes affine types, since you could just have Coroutine<A>
instead of Coroutine<Rec{A.Self}>. Linearity requires also branching types,
which also can be added.

Type inference on the other hand may be tricker though, since (I think) the
usual unification method leads to something like this:

let s = u.a();
// infer(u): Coroutine<A>
let s = u.b();
// infer(u): Coroutine<A.B>
let s = u.a();
// infer(u): Coroutine<A.B.A>

And this may require some sort of subtyping (doable though).

On the other hand though, we may not need to infer this and just get away with
bidirectional typechecking.

Another feature that I think could be useful is some sugar for chaining with
variable binding:

let u
  .a() [s1]
  .b() [s2]

Instead of

let s1 = u.a();
let s2 = u.b();

State

A quick note about the coroutine state. The example above has the same state for
both interfaces. I think probably an ADT would work if each state has different
storage (kind of what async functions are compiled to in rust, where each yield
point is a variant). I'm not sure if we need this though.

Syntax

Maybe something like this?

I think the hard part is separating lifetime from implementation, mostly.

One limitation is what would happen if you need two different impls of the same
interface but in different states. This is solved by labelling though, just ugly.

utxo Utxo {
  main {
    loop {
      with A {
        yield;
      }

      with B {
        yield;
      }
    }
  }

  impl Rec { A.B.Self } {
    fn a() -> String {
      "a"
    }

    fn b() -> String {
      "b"
    }
  }
}

script {
  fn driver(u: Coroutine<Recv { A.B.Self }>) {
    let s1 = u.a();
    let s2 = u.b();
  }
}

Branching:

The weird thing about branching is that it doesn't play that well with the
nominal interfaces.

But let's start with plain unions. Let's say we have this type Rec { A.End | B.Self }.

I think it's weird to express this while keeping the idea of separating
lifetime from implementations, if we really want to keep that model. Writing the
coroutine with the matches explicitly inside directly is simpler to read in my
opinion, but if we want to do that, I think we could do something like this:

Perhaps something like this:

utxo Utxo {
  main {
    loop {
      offer { // yields
        A => break,
        B => continue,
      }
    }

    return
  }

  impl Rec { (A.End | B.Self) } {
    fn a() {
      "a"
    }

    fn b() {
      "b"
    }
  }
}

Where the coroutine gets compiled to:

let storage = Storage::new();

loop {
  let (r, k) = yield();

  (r, k) = match r {
    A::a => {
      resume(r, k, "a");

      // note that this requires that the utxo to be resumed once more for the
      // coroutine to really end
      //
      // this means End is also an "interface" in a way (the empty one).

      // the other option is to have a `resume` that also deletes the coroutine.

      // return probably needs to be a host call to prove linearity
      return();
    },
    B::b => {
      resume(r, k, "b")
    }
  }
}

Also probably want to support an anonymous interface notation, by just using
labels directly or something (see the choice types in Par).

Simpler constructions?

I think there also simpler constructions if the above is too hard to implement
(although I think it may be worth it eventually since it's more about ergonomics
than safety, since we have to do runtime checking anyway).

The obvious option is to just type the utxo/coroutine with both interfaces (or
the union of all the handlers), and then just do the runtime checking.

Allowing boxed handlers (objects) to return other interfaces could also work in
some cases:

interface A[C] {
  a(): (Coroutine<C>, String)
}

interface B[C] {
  b(): (Coroutine<C>, String)
}

interface End {}

fn utxo(): Coroutine<A[B[End]]> { ... }

This also requires linear types.

In the case of a utxo, it would just return itself as the next coroutine:

** NOTE ** however that this is not recursive like the example before, since
that's harder to represent without adding some nominal recursion.

It could however be done for fixed interfaces with named loops, where b
returns Coroutine<A[B[End]>.

struct Storage {
  self_k: CoroutineId,
}

fn utxo() {
  let self_k = kid();

  let (r, k) = yield();

  utxo_a(r, k);
}

fn utxo_a(storage: &Storage) {
    let (r, k) = match r {
      A::a => {
        resume(k, (storage.self_k, "a"));
      }
      Star::Supports(i) => {
        resume(k, i == A::HASH);
      } 
      _ => abort("unsupported operation")
    };

    utxo_b()
}

fn utxo_b(storage: &Storage) {
    let (r, k) = match r {
      B::b => {
        resume(k, (storage.self_k, "b"));
      }
      Star::Supports(i) => {
        resume(k, i == B::HASH);
      } 
      _ => abort("unsupported operation")
    }
}

[ecioppettini]

(although the following is not session types, that also requires duality for
deadlock freedom).

To expand briefly on this, in case anyone reading this cares.

Session types are typestates over channels. But the point of sessions is that they encode a communication protocol.

This means the types are not for a single process, but for an aggregation of them.

If you have something like this:

fn p1(c: Chan<Send<u32, Recv<bool, End>>) {
  let c = c.send(10);
  let (c, r) = c.recv(); // doing a send wouldn't type, c has type Recv<bool, End>
  c.end();
}
fn p2(c: Chan<Recv<u32, Send<bool, End>>) {
  let (c, r) = c.recv();
  c.send(r > 1000);
  c.end();
}

Then you can type the function that runs both processes in parallel (toy example though, there is also a rust implementation of par with more practical code)

trait Session {
  type Dual;
}

fn chan() -> (Chan<T>, Chan<T::Dual>) {}

fn par() {
  let (c1, c2) = chan();
  p1(c1);
  p2(c2);
}

And then you have a statically checked guarantee that each send is paired with a recv, and viceversa. Which also implies you don't have deadlocks.

But the important thing is that the type describes two processes. And there are generalizations of session types for more participants too (although that's much more complicated).

In our case, I don't think we really care about these kind of properties. Or at least not as a priority, though, this is mostly to clarify the terminology. In theory a coordination script probably describes a multiparty (global) session type, but implementing that is probably too complex to be worth it. Binary sessions are not that complicated, but it may not be worth it at least until we collect proper use-cases.

[ecioppettini]

LAST EDIT: Since edits are not super visible (but I still want to have a single document on top)

I changed the "syntax" part example to this, which I think reflects more the original design of splitting lifetime from impl, but I still think it's not really possible to not mention the interfaces in the main function.

utxo Utxo {
  main {
    loop {
      with A {
        yield;
      }

      with B {
        yield;
      }
    }
  }

  impl Rec { A.B.Self } {
    fn a() -> String {
      "a"
    }

    fn b() -> String {
      "b"
    }
  }
}

script {
  fn driver(u: Coroutine<Recv { A.B.Self }>) {
    let s1 = u.a();
    let s2 = u.b();
  }
}

Also added a branching example:

utxo Utxo {
  main {
    loop {
      offer { // yields
        A => break,
        B => continue,
      }
    }

    return
  }

  impl Rec { (A.End | B.Self) } {
    fn a() {
      "a"
    }

    fn b() {
      "b"
    }
  }
}

And its possible compilation:

let storage = Storage::new();

loop {
  let (r, k) = yield();

  (r, k) = match r {
    A::a => {
      resume(r, k, "a");

      // note that this requires that the utxo to be resumed once more for the
      // coroutine to really end
      //
      // this means End is also an "interface" in a way (the empty one).

      // the other option is to have a `resume` that also deletes the coroutine.

      // return probably needs to be a host call to prove linearity
      return();
    },
    B::b => {
      resume(r, k, "b")
    }
  }
}

[ecioppettini]

Performing effects in methods (which are handlers)

This is a slightly different topic, but somewhat related.

Utxo methods are effect handlers, and one of the issues is that those may
need to perform other effects.

The handlers for those effects could in principle do all of the following:

Do reads. Without modifying ledger state or coordinator script state.

This is the case with external functions. Or it's also the case with something
like the permissioned token example we had, in which you ask for a proof of
something, but that proof is just a read.

These are mainly about ergonomics, since it's otherwise not that simple to just
inject arbitrary inputs (dynamic witnesses that are computed from current state,
like doing an offchain indexer call).

Modify some transaction-local state, but not ledger state.

A method may be invoked ten times, and the coordinator script needs to keep
track of this, so it changes its own state each time.

Change the ledger state. Like resuming a utxo.

I think this one is the most problematic, since it could lead to re-entrancy, but not necessarily. I think we can just make the methods "atomic".

In the implementation framework I'm proposing, a "method" compiles to
a yield followed by a match and a resume.

For example:

interface B {
  b(): str
}

interface A {
  a(): str / { B }
}

utxo Utxo {
  main { yield }

  impl A {
    fn a() {
      do B::b()
    }
  }
}

(Not really sure yet if the above can be statically typed without the
bidirectional effect, otherwise we'd need some sort of subtyping?)

The low level code transformation would be:

fn utxo(handler: Coroutine<B>) {
  let (r, k) = yield();

  match r {
    A::a => {
      // do B::b(3)
      //
      // this calls the B::b handler currently installed in the coroutine
      // identified by handler
      //
      // which is currently suspended on a resume followed by a match just like us before
      let (br, response_k) = resume(handler, B::b);

      // we called handler with a specific effect, so no one else should resume us.
      assert_eq!(response_k, handler);

      // since we expect a specific response (B::b has a specific return type),
      // no-one can resume this utxo with a new "request".
      let br = match br {
        B::b::Ret(br) => br,
        _ => abort("re-entrancy")
      };

      // the interleaving proof needs to guarantee that the control flow is
      // correct (from_k and handler match the program that sent this data)

      // k is the original method caller
      resume(k, br)
    }
  }
} 

I think this implementation ensures that this utxo cannot be resumed
incorrectly (getting stuck in a weird state). We also may need to prove
linearity, that is, this utxo must be resumed in this transaction (not
necessarily, but maybe only yield should be affine).

For that, resume could set a flag in the scheduler that says that this utxo needs to be
resumed or the transaction is wrong. This should also not be hard to prove. When
folding the interleaved trace we set a flag in the same manner, and we turn it
off on resumption. At the end of the transaction we just check these flags.

The point of this is that we want to ensure that the utxo doesn't die or change
states before the "method" finishes.

The other case is that any other utxo could be resumed in the B::b handler,
since we don't know what it does. The only way I can think of solving this is
by taking a lock on the current utxo, and no other utxo can be resumed with the
lock on. I'm not sure this is:

a) Necessary, because it may not be an issue.
b) Easily typed. Because how would you check this? It's similar to coloring
read-only (pure) and read-write (impure) effects, but that's non trivial.