Lambda the Ultimate

The syntax of Frank proposed in the paper actually restricts effectful operations (such as open, write in your example above) to a "pure" interface (A1 -> ... -> An -> B) instead of an arbitrary computation type (<Delta1>A1 -> ... -> <Deltan>An -> [Sigma]B). So your proposed (String -> [Logging]Handle) is not supported for now: catching an operation always gives a value, and handling it cannot add new effects to the ambient ability. (I asked the authors, and) Extending this is future work.

Note that the handlers of <IO> do not have to return the same type as what the operations return, this type only informs what handlers need to pass to the continuation. So you can write

logging_FS : <IO>X -> [Logging]X

or even more flexible forms such as

logging_FS : <IO>X -> LogState -> (LogState * X)

which lets you pass around an intermediate LogState value that contains aggregated information on how to log -- solving the "you must decide logging one IO operation at a time" problem you mentioned. This is, of course, just a state monad, so you can also do

logging_FS : <IO>X -> [LogState]X

and latter write a <LogState> handler that keeps its state and makes [Logging] decisions.

Yes, I see that you can always pass the logging "up" from the handler by having it introduce the logging effect, but I was focusing on the case where you want to pass the logging effects back "down" into the continuation, giving it a chance to handle them. I should have made that explicit.

So once the authors extend interfaces to allow arbitrary computation types, there really won't be much difference between a process and effectful computation. The effectful approach just singles out one of the ports (yield pure value) and gives it special significance. In the process approach you do the same thing, but in the core calculus "yield" is just another port. I think I may have figured this out last time we discussed algebraic effects on here...

I don't have as much experience programming with processes (I'm sure Sam Lindley, who also works on Session Types, would have interesting things to say there), so I can't comment much besides agreeing that Frank's handling style feels a lot like message-passing to me.

There is a subtlety though: yield does not just put a value on a "preferred" channel, it also stops the computation -- yielding has no continuation. You can express that by turning any X value in a [Return X]0 computation, with (Return X := return : X -> 0), but are X and not-not-X really the same thing? We already know that intuitionistic logic can be generalized into classical logic by moving from "a value is returned" to "one of the output ports may be called", yet there remain relatively fundamental differences between the two -- for example we don't really know how to have a graceful dependent type theory for classical logic.

I would thus say that I don't understand the difference enough to tell whether this is just a question of style (one presentation being more familiar than the other to some audience, or maybe more convenient to program in the common case) or whether this apparently-small difference has deep consequences. Those consequences may not be the fault of either choice (I would bet that the thing we don't understand enough is dependent types, not classical logic), but in a world of partial understanding prudence is still useful.

Your encoding works fine. You can then write:

run: [Return X]0 -> X
run <return x -> k> = x

I don't think this is really the same as equating X and not-not-X.

But note that this encoding is back in Frank where you already have a distinguished value port. I think an argument can be made that things are nicer and more symmetric if we hadn't done that and just worked with processes. For example, look at the state example from the paper that I copied into my first post here. It handles the yield port and does nothing but pass it along. It didn't need to handle that port at all!

It seems like most of the papers I find have in mind concurrency when they speak of Processes and session types are often pi calculus. I wonder if there's anyone using the using the term the way I've been using the term? Namely:

Process = Message -> (Process, Message)

Lately I've been splitting this into two types, S (sender) and R (receiver) and have been writing A↑B for (A, B) and A↓B for B -> A. So we have:

S = R ↑ M -- A sender is a receiver that has emitted a message
R = S ↓ M -- A receiver is a sender that is waiting for a message

Then receivers are what I originally called process but I also have the name 'sender' for the result of sending a message to a process.

That's the basic idea semantically, but then the trick is labeling messages with ports and only allowing the construction of processes with certain rules that prevent snooping on hidden ports (even counting messages passing back and forth, which can be done generically on any protocol, should be prevented).

Does that sounds familiar at all? Is anyone else looking at effects this way?

The syntax of Frank proposed in the paper actually restricts effectful operations (such as open, write in your example above) to a "pure" interface (A1 -> ... -> An -> B) instead of an arbitrary computation type (A1 -> ... -> An -> [Sigma]B). So your proposed (String -> [Logging]Handle) is not supported for now: catching an operation always gives a value, and handling it cannot add new effects to the ambient ability. (I asked the authors, and) Extending this is future work.

Do you know if the theoretical foundation for this extension is already laid?

With the Process encoding of algebraic effects, there is a subtlety. Consider this fragment:

interface B 
   b : Int -> Int

interface A
   a : [B] Int

handleB: [B] Int -> [A] Int
handleB x = x
handleB <b n -> k> = handleB (k (a + n))

handleA: [A] Int -> Int
handleA x = x
handleA <a -> k> = handleA (k (b 1 + b 2)) -- b is in scope when handling a

foo: [A] Int
foo = handleB a 

bar: Int
bar = handleA foo

EDIT: Forgot to add recursive call to handler

In this example, the computation foo produces an A while it's handling the B response from A. So what should happen? Is this simple non-termination? A run-time error? Something else?

Using Processes as a model for this situation, the correct behavior is error upon attempting to re-enter the A handler while it's in a bad state (still fielding the original query).

Does the category theory that motivated algebraic effects suggest an answer here?

I vote for non-termination. Here is the reduction sequence I have:

handleA foo
= handleA (handleB a)
= handleA <a -> μx . handleB x>
= handleA (handleB (b 1 + b 2))
= handleA (handleB <b 1 -> μx. x + b 2>)
= handleA (handleB ((a + 1) + b 2))
= handleA (handleB ((a + 1) + b 2))
= handleA <a -> μx. (handleB ((x + 1) + b 2))>
= handleA (handleB (((b 1 + b 2) + 1) + b 2))
= handleA (handleB <b 1 -> μx. (((x + b 2) + 1) + b 2)>)
= handleA (handleB ((((a + 1) + b 2) + 1) + b 2))
= ...

Nitpicking P.S.: in the handleA <a -> k> comment you wrote "b is in scope while handling a". I think this is not completely true: b is "in scope" (in the ambient capability) under the calls to the continuation k, that consumes a <B>Int and returns a [A]Int.

This reduction sequence and that nitpick were what I needed to read!

This is different than what I've been doing, but I think it's probably better and I can do it with processes, too. I have been working with processes that send and receive messages, but the discpline here is asymmetric. Processes send messages and receive back computations to run. I'd thought of this possibility, but it didn't click.

So to encode this in processes, we just introduce a special process # that runs the messages it receives, producing any side-effects. Then m! is shorthand for # ↑ m [r: \x k. k' x] where k' is the continuation expression in which m! appears. So, in words, we send up m and then wait to receive a computation back which we will run. And we'll run it with a handler that responds to a return message by continuing with the expression k' (discarding k – the computation that issued the return). All other messages before return will be handled by the environment.

Note this convention is more verbose than Frank which just puts ! on nullary operations, but since I use messages as values in the reduction sequence below, I think it's useful to be more verbose. I assume ! binds as tightly as juxt so that you can always stick ! on to the end of an application chain without adding parens.

handleB (b n) k = (k ↓ {ret (a! + n) !}) [b: handleB]

handleA a k =  k ↓ {ret (b 1 ! + b 2 !) !} [a: handleA]

bar
= a! [b: handleB] [a: handleA]
= # ↑ a [b: handleB] [a: handleA] -- I cheated here.  a! should technically catch r and resend it
= # [b: handleB] ↑ a [a: handleA]
= handleA a (# [b: handleB])
= # [b: handleB] ↓ {ret (b 1 ! + b 2 !) !} [a: handleA]
= # ↓ { ret (b 1 ! + b 2 !) ! } [b: handleB] [a: handleA]
= ret (b 1 ! + b 2 !) ! [b: handleB] [a: handleA]
= # ↑ b 1 [r: \x k. ret (x + b 2 !) !] [b: handleB] [a: handleA]
= # [r: \x k. ret (x + b 2 !) !] ↑ b 1 [b: handleB] [a: handleA]
= (handleB (b 1) (# [r: \x k. ret (x + b 2 !) !])) [a: handleA]
= # [r: \x k. ret (x + b 2 !) !] ↓ {ret (a! + n) !} [b: handleB] [a: handleA]
= # ↓ {ret (a! + n) !} [r: \x k. ret (x + b 2 !) !] [b: handleB] [a: handleA]
= ret (a! + n) ! [r: \x k. ret (x + b 2 !) !] [b: handleB] [a: handleA]
= ...

Using a return port (r above) instead of treating the value port specially seems like it might be cleaner. Though I think we really want a different return port for every expression. Also I've been sloppy about ports, just assuming that messages are on a particular port, because I treat port names differently than Frank. Hopefully you get the idea.

There are still a couple of things nagging at me that I seem to lose from my old approach. Maybe I can figure out how to salvage the good stuff.

It occurs to me that the algebraic effect approach of singling out the return port misses out on one simple feature we get for free if we don't distinguish the return port: mid-procedure return. If return is an ordinary port, we can raise return early and it works just as imperative programmers would expect.

Thanks Oleg for the links. I can believe that the idea of effectful computations as processes is quite old. This was one of my first ideas for what I wanted in my own programming language, ~20 years ago. (It looked much different back then).

But I wonder whether anyone has studied a setup with ports the way I'm discussing. It seems very close (perhaps identical) to algebraic effects. I can sketch it pretty simply here. I'll use variable r for a receiver, which is a function from a message to a sender, which is a (message, receiver) pair.

Two simple operations that we expose are r ↓ m and r ↑ m. The former sends a message into a receiver and the latter pairs an upward message to a receiver that will receive the response. Both of these constructions produce senders. Rather than naming senders, I will generally pattern match on r ↑ m (a pair).

Then we have handlers that wrap processes. We allow upward handles, written p [a↑: f], that catch messages arising from the nested process p, and downward handlers, written p [a↓: f] that catch messages coming downward from above. And here p can be either a sender or receiver. So we have four cases (sender/receiver and up/down), but the rules for the semantics of handlers are simple:

(r ↑ m) [a↑: f] = f r m   if m is on port a
                = r[a↑: f] ↑ m  otherwise -- message passes up

r [a↑: f] ↓ m = (r ↓ m) [a↑: f] -- downward messages pass by up-handler
                
(r ↑ m) [a↓: f] = r [a↓: f] ↑ m -- upward messages pass by down-handler

r [a↓: f] ↓ m = f r m   if m is on port a
              = (r ↓ m) [a↓: f]  otherwise -- message passes down

When an upward handler gets a message from below, it handles it if it's on the correct port, otherwise passes it up. When an upward message handler receives a downward message, it always passes it downward without handling it. And so on.

Just to emphasize, the rules above define the semantics of handlers, but then we have to use only these handlers (and r ↓ m and r ↑ m) to build up processes. We're not allowed to pattern match an arbitrary sender with r ↑ m as above, because that would require knowing about messages on hidden ports. Care was taken so that handlers only get to see messages that arrive at their port, and then the result of the handler function should be a process that preserves expected protocol on the hidden ports.

To that end, we can type handlers with a schema like this (other cases are similar):

r : R e    f : R e -> m -> S (e' + a::P.m)    e' > e
----------------------------------------------------
              r [a↓: f] : R (e' + a::P)

Some notes on what this means:
- R ps and S ps represent receivers and senders on a set ps of ports with protocols
- Addition is type level set append.
- a::P means port a follows protocol P
- P.m is the protocol remaining to be followed by P after a transition of message type m (or a type error if that message type isn't allowed as the head of the protocol).
- e' > e means e' has at least the ports of e with the same protocols.

Is this clear? Is this interesting to anyone? I have a paper in the works on how to use this construction in an effect system, but is this core construction described somewhere?

I personally think that you should look in more details at the work on session types. Unfortunately, I'm not super familiar with them myself so I cannot precisely comment on where to look. But I know that a list of messages (or effectful operations) one expect to receive, or send, with a static description of the interaction protocol, all that has been described in the session type literature. Another aspect of session types is that you can often compute, from a static protocol description, the "dual" protocol corresponding to the other corresponding entity, by inverting inputs and outputs -- I suppose you could do this here as well.

One the other hand, the use of session types that I know of do not have the "pass more in depth" behavior on messages that they don't understand; in typical process calculi, people waiting on a given message will typically block, but you have a set of such processes that are parallel to each other and you expect that one of them will consume the message. The behavior of accepting several messages simultaneously, as with effect handlers, is in fact more actor-like, although there more structure on the receiver hand (not just a list of accepted messages, but an ordering between the various handlers that can restart computation at different points).

Everywhere I look, session type means pi calculus. Is that always true? I've commented a bit here about the relationship I see between my processes and pi calculus. I think the main difference is that I focus on the state of the port, whereas pi calculus focuses on the state of the process. I'm not an expert (by any means) on pi calculus, but it seems very powerful (e.g. able to encode concurrency) and very complicated for use as an effect system. Compare to what a protocol for me might look like with my style processes:

protocol State a
    get: Yield a (State a)
    set: b -> Yield () (State b)

protocol Yield a P
    yield: a -> P 

Protocol declarations would serve a purpose very similar to interface declarations in Frank. They explain the messages that can travel over a port in a given protocol and tell which protocol comes next. The above is a type state protocol for interaction with a mutable cell. (I'm assuming a notation here that implicitly inserts alternation -- otherwise you might expect to see a minus sign before those uses of Yield to indicate that the messages of yield go the other way. I think this might be useful sugar since alternation is the common case).

So I don't really see session types as a viable alternative for direct use in a practical effect system. The notion of process I have in mind seems more akin to algebraic effects. And from my present understanding, it seems to both generalize and simplify the algebraic effects approach. That makes me think people just aren't aware of this construction. I'll try to clean up my paper and put it on Arxiv this week. (Anyone can feel free to harass me if I don't.)

It depends on how "global" you have in mind. Resources, if I understand correctly, allow you to store some state on the stack at the place where the handler is installed (in this regard they are similar to Racket's "stack marks"). But once this stack frame is popped, the resource is gone -- unlike a heap in a ML language that lives independently of control. Besides, someome between you and the handler may install a more local handler to catch these operations.

On the other hand, resources in Eff are somewhat bundled with "instances", which let you dynamically create a new set of operations (a new instance of a given effect signature) whose identity is generative: it is incompatible with all previous instances of the same operation. This lets you create private operations that nobody else can raise/handle (unless you let them); so, in particular, if you set a handler for them at the top of the stack, you can pass down values that raise them and that you know will never be intercepted by some other handler, letting you have a sort-of-global effect.

If you look at section 6.3 (state example), there is this text:

An even bigger problem is that the reference may propagate outside the scope of its
handler where its behaviour is undefined, for instance encapsulated in a λ-abstraction.
The perfect solution to both problems is to use resources as follows:

let ref x =
  new ref @ x with
    operation lookup () @ s -> (s, s)
    operation update s’ @ _ -> ((), s’)
  end

I interpreted this to be saying that they want the reference to outlive the handler that you might install there where you create the reference. And the fact that the 'with' clause is attached to the syntax of 'new' suggests to me that there maybe isn't any way to handle these references. It's a way to generate a reference that uses global state and doesn't need to be handled.

Based on that reading, it seems easy enough to extend this approach to not use global state. Rather than allocating references from a global heap, you could make heap access (new) itself an effect. Then you can allocate from a heap (or several heaps) and put each heap somewhere on the handler stack - nothing global.

But I want to make sure I'm not missing the point. Maybe the resources already are somewhere on the stack and I've missed their & your point. (BTW if you know of any other references that explain resources, that would be great).

Indeed it seems that I misunderstood: your snippet seems to suggest that handlers are attached to the operations in this case, and will be used when the operation reaches "the top" of the stack, making it more convenient to use them as global state. (But again it seems to be more a property of "dynamic effect" / instances than of the idea of resources themselves, which just tracks state across the activations of a given handler.)

It seems to me the behaviour can be split into type-class dispatch, and a cofunction to maintain the state. The cofunction is a simple loop (tail-call) that receives the commands and returns the results. With this model the commands themselves would be simple datatypes.

Edit: I will add an example of a cofunction,where 'yield' returns its argument to the caller of the current function (like "return"), and accepts the next call to the cofunction (JavaScript like language).

data Op<A> = Lookup | Update(A)

ref(x : A) =>
   refLoop(x, yield(null))
   where
      refLoop(x, op : Op<A>) =>
         match (op)
            Lookup => refLoop(x, yield(x))
            Update(y) => refLoop(y, yield(null))

test() =>
    ref(0)
    ref(Update(27))
    ref(Update(13))
    ref(Lookup)

Test would return "13". The cofunction allows state to be expressed as a tail call, which can be optimised away. Effectively the the closure behaves like an abstract datatype. The interesting thing is an ADT is a simple recursive cofunction, but more complex protocols are possible.

A further thought is that it is not far from this to stateful objects, where the methods are the commands, and the object state is passed recursively. The question is then are simple objects (no inheritance) easier to use? They are certainly easier to type because the accepted set of commands cannot change depending on the internal state of the cofunction. You would end up with something like a 'neater' version of JavaScript :-)

This approach requires you to manually thread the reference state through the program, though, so it's not really behaving as a reference but more like a single object container. I think if you try using this as a reference in a larger example then you'll see the problem. Also, if you haven't looked into algebraic effects yet, I would recommend it! I think this Frank paper is a good place to start.

Notice algebraic effects = type classes + cofunctions. The cofunction above is more like an abstract datatype than an object, as it only has one instance. "ref" has one state shared by all uses of the cofunction, so you do not need to create a new instance of it. Take the example above and add a typeclass to make dispatch implicit and you get:

typeclass Ref
   lookup() => ref(Lookup)
   update(x) => ref(Update(x))

test() =>
   update(13)
   update(27)
   lookup()

It only has one instance, so default implementations are used.

Edit: I am not sure you have understood the original example, "ref" does not have to be threaded as it's a top level function/cofunction. You can do:

test1() =>
   ref(0)
   ref(Update(27))
   test2() // note no threading

test2() =>
   ref(Lookup)

Sorry, I thought the consecutive lines of ref were function application doing the threading. I see what you mean. I agree that this scheme seems roughly equivalent.

One initial reaction I have is that it seems to require co-functions, which involve spooky action at a distance, to be woven into the fabric of values. One nice thing about algebraic effects (or my processes) is that they make sense as "values" that emit messages to be handled. If you have an effectful computation, that should be reflected in its type. If you can cook up a scheme to keep track of which co-functions a given computation interacts with, I suspect it will look very much like algebraic effects.

It just occurs to me that this concern about typing might equally apply to resources. I wonder if Eff tags computations with "uses global state" if they've used resources.

Type-classes would track the co-functions, so a function that uses them would have those type-classes as constraints. By default functions are polymorphic in type-class bounds (if we have type-class inference), so functions behave like Frank "A -> []B" types. If you supply type-class bounds, then obviously they don't get inferred, so "(Ref A) => A -> A" would behave like Frank "A -> [Ref]A".

Typing cofunctions is not straightforward, and seems to require dependent types. When you first call "ref" it has the type (using Int for simplicity although it is polymorphic in the above definitions): "Int -> ()", however next time you call it you need to pass an "Op", and what you get back depends on the value of Op. Notice also you can think of calling the cofunction as passing a message of type "Op" to the resource (IE a cofunction behaves like a resource) so "Op.Lookup -> Int" and "Op.Update -> ()", the loop above then stays in the state expecting another "Op".

If we promote the "Op" messages to types then we can avoid dependent types, but we then need to introduce type-cases to the language.

data Lookup = Lookup
data Update<A> = Update(A)

ref(x : A) =>
   refLoop(x, yield(null))
      where
         refLoop(x, op : Op<Lookup \/ Update<A>>) =>
            typematch (op)
               Lookup => refLoop(x, yield(x))
               Update(y) => refLoop(y, yield(null))

Now I am not really sure how to write the type, but the first call to "ref" has type "Int -> ()" and then every subsequent one has the type "Lookup -> Int /\ Update Int -> ()". Perhaps we could represent this sequence of types as a list:

ref : [Int -> (), Lookup -> Int /\ Update Int -> (), ...]

It becomes like typing a protocol at this point. Has any work been done on typing protocols?

Well sure, Hoare did in CSP. You're basically saying the type of a process is the set of all possible event sequences the process can engage in.

I am currently looking at CFG's (and indeed regexps) as reasonably simple ways to express such sets in the simpler CSC (communicating sequential coroutines) system. For example a coroutine implementing a partial function of a stream goes read, maybe write, go back for more, and the type is given by regexp (R+W)+ where postfix + means repetition. Obviously the notation gets messier for multi-channel coroutines and its not clear to me what "type checking" a composition such as a pipeline of transducers actually means.

As I think about this a bit more, the big problem I'm having is trying to figure out where your co-functions live. "Globally" is not a good answer! Relatedly, with algebraic effects you have a type for a computation with unhandled effects. But once you've handled an effect, you generally want it removed from the type - locally handled effects are nobody's business. So it seems like you don't want to type interaction with a (locally bound) co-function. You just want to type interaction with a named but unbound co-function.

Also, I don't think you need dependent types or type-case. You can use GADTs to keep track of what the message does to the protocol state as part of the message type.

You are right about GADTs, I had thought that, then forgot about it :-)

Also functions/cofunctions are first class, so you can pass them as arguments, its just convention that top level things are global.

I'm lost trying to figure the semantics of your first Ref example. How does the second call to Ref interact with a co-function instead of creating a new reference? Also, would you mind doing an example where a function creates a local reference and uses locally?

The semantics are like a coroutine, but always with function call semantics. So when you call 'ref' you pass arguments like a normal function, when 'ref' yields it returns the parameter of yield to the caller, but also saves the re-entry point. When 'ref' is called again, it continues from where it left off, returning the arguments passed to 'ref' as the result of 'yield' so from inside 'ref' yield behaves like a function call. Its probably easiest to explain the control flow in the first example (We can interpret the newline the same as Frank with snd(x, y) = y):

data Op<A> = Lookup | Update(A)

ref(x : A) =>
   refLoop(x, yield(null)) // 1
   where
      refLoop(x, op : Op<A>) =>
         match (op)
            Lookup => refLoop(x, yield(x)) // 2
            Update(y) => refLoop(y, yield(null)) // 3

main() =>
    ref(0)
    ref(Update(27))
    ref(Update(13))
    ref(Lookup)

Assuming we start at 'main' the control flow is:

- calling 'ref(0)' passes 0 into 'ref' as x
- 'ref' gets to 'yield(null)' (labelled '1'), returns the null, and internally saves the continuation.
- main calls 'ref(Update(27))' which re-enters 'ref' by returning 'Update(27)' from the yield, and passing this along with the value of 'x' to 'refLoop'
- 'refLoop' matches on 'op' and takes the 'Update' branch.
- gets to 'yield(null)' which returns null from the call to 'ref(Update(27))'
- 'main' calls ref(Update(13)) which returns from the 'yield(null)' (labelled '3') with the value 'Update(13)' which is passed to refLoop in the tail-call along with the value of 'y'
- the match takes the 'Update' branch.
- returns from call 'ref(Update(13))' with null
- main calls 'ref(Lookup)'
- returns from call to 'yield(null)' (labelled '3') with the value 'Lookup'
- calls 'yield(x)' (labelled '2') which returns from 'ref(Lookup)' with the value '13'.

Does that make sense?

I get the idea, but the syntax doesn't make sense to me yet and I think it may have bugs. Does the => syntax install a process in an environment and give it state? It seems to with the ref() declaration, but not with the refLoop() declaration (why doesn't the yield in refLoop yield back to ref?)

Also, the fact that the initialization is treated the same way as message passing seems kind of ugly to me.

I think you could maybe clean up both issues by letting 'run c expr' install and run a co-routine with body exp in an environment under name c?

-- These are just *functions* at this point:
ref x:A = refLoop x (yield null) where
  refLoop x op = ...

main =
    run r (ref 0) -- binds r to the continuation, evals to the first yield (null in this case)
    r (Update 27)
    ...

This has the nice effect that r always has the same continuation type, because we didn't try to type the "initial coroutine" -- we only need to type it at the first encounter of yield. It's now practical to skip complicated protocol typing if you want to, since you can do practical things with a uniform interface type.

It also makes explicit where the co-routine boundary is (it's at run). But you also need to explain what the behavior is when 'r' escapes this lexical environment.

'=>' is just regular function/cofunction definition. There is no state apart from the cofunction 'continuations'.

I can use a more Haskell like syntax, so the above would be:

data Op a = Lookup | Update a

ref x = refLoop x (yield ())
   where
      refLoop x Lookup = refLoop x (yield x)
      refLoop x (Update y) = refLoop y (yield null)

test = let _ = (ref 0) in
   let _ = (ref (Update 27)) in
      let _ = (ref(Update 13)) in
         ref(Lookup)

A better way to define it which does what you want without introducing a magic 'run' keyword would be:

ref(x : A) => (op) : Op<A> =>
   match (op)
      Lookup => ref(x)(yield(x))
      Update(y) => ref(y)(yield(null))

Which you would write Haskell style as:

ref x = \op -> case op of
    Lookup -> ref x (yield x)
    Update y -> ref y (yield null)

let r = ref 0 in 
   let _ = r (Update 27) in
      let _ = r (Update 13) in
          let z = r (Lookup)

What does yield do (precisely)?

yield returns control to the caller with the value of its arguments as the result, but it also updates the function entry point, so the arguments of the next call to the function are returned from that yield.

In terms of implementation, the function call would have to indirect via a pointer that initially points to the start of the function, but gets updated by yield. You could view this as a small single element stack where on function entry it pops the current address and jumps to it, and on yield it pushes the 'return' address to jump to the next time you call the function.

... of what?

helper x = ... yield null ...
ref x = ... helper x ...
foo x = ... ref 0 ...

yield returns control to the caller of the cofunction in the same way that in C a return returns control to the caller of a C function: the return address (continuation) is saved somewhere implicitly (such as on the machine stack).

This limits what cofunctions can do (form trees of control) compared to general coroutines which do read/write on channels, where the channels explicitly hold the peer continuation. However the advantage is simplicity and syntactic unification.

What I like about it is that there is a single thread of control and you cannot get deadlocks, which I don't think is the case with general coroutines.

Where "return" would return to :-) Consider JavaScripts "return" statement, it is imperative because it is not a function. In my example "yield" looks like a function to the callee, but it serves the purpose of "return". So "yield null" returns "null" from the call to "helper x".

I guess your point is what happens with nested functions and cofunctions? In the syntax above a thing that "yields" is a cofunction, so that issue does not arise.

Edit: An orthogonal point which might be confusing is how you distinguish the value of a function from a reference to the function. Frank does this by treating an unapplied function as a reference to the function, and only as its result value when all the arguments have been supplied. This leaves an anomaly with zero argument functions, hence the need for the "!" postfix to indicate execution of a zero argument function (without the "!" it is a reference to the function). If we use '()' for argument lists in the style of 'C' then we do not need anything else because:

f() => 27 -- define a function that returns 27

f   // reference to the function
f() // execute the function (like Frank's "f!")

This distinction applies equally to multi-argument functions.

Also where Frank uses "let g = {f x}" to defer execution, you can use a lambda in the same way. For example this could be written"

let g = () => f(x) // equivalent to Frank's "let g = {f x}"

This is semantically the same, as in Frank 'g' would be executed with "g!" and in this syntax "g()"

Edit2: You can also program with only cofunctions, as a normal function is a special case of a cofunction that looks like this:

id x = id (yield x)

Is this standard terminology? Google didn't turn up much interesting for "co-routine vs. co-function". I'm familiar with Python generators... I'd suggest you not copy them (for example, in python nested functions can't close over yield). I'm also not sure why you think co-routines would be multi-threaded or suffer deadlocks.

If your language already supports mutable bindings, I can understand why you want to keep the continuation state in the environment. I still think you're not thinking clearly about where yield is supposed to go. You gave this example:

ref(x : A) => (op) : Op<A> =>
   match (op)
      Lookup => ref(x)(yield(x))
      Update(y) => ref(y)(yield(null))

Apparently this yield is supposed to resume control to the caller of the nested function. Earlier control was apparently passing to the caller of the top-level function. It seems to have "do what I mean" semantics.

It seems to me that you're going to want all of these cases:
- nested helper functions that yield back to their parents (like refLoop)
- functions that help construct co-functions (like the example here)
- functions that construct and use co-functions locally

To accommodate these cases, I think you need some kind of syntax that indicates where a new yield-scope is introduced. Thus the 'run' I proposed. I made it an expression to remove the asymmetry between the initial continuation (an explicit function) and subsequent (implicit continuations of yield), but if that doesn't bother you there are lots of choices. I think you need something, though.

Some final notes: in order to have the same expressive power as algebraic effects, you'll need to support capturing a co-function in its mutated state as a value (you already have a syntax for that -- naming it without parens).

You also need to figure out if you're going to support passing access to co-routines of the environment into a co-routine and what the syntax for that would look that. In effect language this corresponds to my initial discussion with gasche in this thread about passing effects from a handler back to the initial effect-raising environment.

I would embed functions into co-functions by:

nocontinue: (forall a. a) -> ()
return x = nocontinue(yield x)

Good luck!

Cofunctions is not standard terminology, but it came up in discussion with John Skaller.

Regarding deadlocks, generalised coroutines can suffer deadlocks as a function can be waiting on a queue that is waiting on that function to output something. John's generalised coroutines can deadlock I think, so don't get too distracted by my reply to him which does not apply to simple co-routines like Python's yield.

Apparently this yield is supposed to resume control to the caller of the nested function. Earlier control was apparently passing to the caller of the top-level function. It seems to have "do what I mean" semantics.

That's a good catch, I think the earlier version would not have worked. It was a bad translation from an imperative loop.

To accommodate these cases, I think you need some kind of syntax that indicates where a new yield-scope is introduced. Thus the 'run' I proposed. I made it an expression to remove the asymmetry between the initial continuation (an explicit function) and subsequent (implicit continuations of yield), but if that doesn't bother you there are lots of choices. I think you need something, though.

I don't mind it - I think an alternative is to mark the co-function definition somehow. The problem with allowing nested functions is you will need a stack for the cofunction.

I think it may be simpler to say I wrote the first example too quickly and it should not work. Of your three cases I think you need (2) and (3), but I think you can do without (1), as we want the cofunction state to be fixed size. Maybe there is a better solution with more thought.

In effect language this corresponds to my initial discussion with gasche in this thread about passing effects from a handler back to the initial effect-raising environment.

That's why I mentioned it, there seemed to be similarities to your discussion.

You also need to figure out if you're going to support passing access to co-routines of the environment into a co-routine and what the syntax for that would look that. In effect language this corresponds to my initial discussion with gasche in this thread about passing effects from a handler back to the initial effect-raising environment.

I thought I would just pass a reference to a cofunction like passing a function.

test1() =>
   let x = ref 0
   x(Update 13)
   test2(x)

test2(y) =>
   y(Update 25)
   y(Lookup)

...will be fairly limiting compared to algebraic effects. It means you can't take a computation that generates some effects and handle some of them by yielding. e.g. suppose you have a computation that generates "print" effects, and you want to convert that into a generator that enumerates the printed things.

The issues with passing co-function references are 1) syntax and distinguishing it from passing the captured co-function value and 2) typing and/or dealing with escaping references.

I would imagine that print is a cofunction that encapsulates the state of the IO stream. Assuming I want to avoid dynamic scoping, and we allow shadowing of variables we can do:

print(s) => ... // do IO
   myScope() =>
      print(s) => .. // log
      
      print("hello")
      print("world")

The idea is there is no global state, any state has to be encapsulated in a cofunction. This means the state of the IO streams is wrapped-up inside of 'print'.

Responding to your edit, I'm still not sure that you're being careful about where the state lives. From everything you've said thus far, I'd expect this behavior:

test1() =>
   let x = ref 0
   let y = ref 0
   x(Update 13)
   let z = y(Lookup) -- z = 13 (!)

Yes, I think so too, that is why I said it was more like an abstract data type rather than an object.

Edit: I think simple objects probably present a more understandable model of state. We could get something easily modeled by cofunctions that looks like a simple object. You would have methods that have immutable local variables, and all mutable state would have to be object properties.