Lambda the Ultimate

Mario B.: A producer coroutine applies put to a sink with a value, a consumer gets values from a source.

That's what I'm doing again right now, revising a lightweight process model under trampolines. Typing pipes seems simpler than typing coroutines. I prefer doing dataflow with pipes, so scheduling is driven as a side effect; a put need not force a context switch until bounded buffer limits kick in. (I'm doing this in naked low level C, so it's not a language I can describe, at the moment anyway.)

If coroutines need to be typed per values used in yield and resume, this seems to require coroutines have pipe-ness built into their semantics. Every time I bind together two concepts this way, when they might be independent, it causes surprising unintended complexity somewhere downstream.

Maybe that's how coroutines are defined (passing dataflow values between one another), as opposed to merely being independent fibers that happen to use a pipe. But I'd rather have fibers that happen to use pipes in order to effect coroutine behavior. You can always force a rendezvous style context switch on every put with a pipe permitting only one write in the bounded buffer semantics.

If you keep the two ideas separate, you can have fibers return a typed value on exit, which put and get typed values on pipes, without those being the same type.

Pipes might be easier to type if the I and O of the coroutine are separable, but would seem to greatly complicate using types to capture: When a coroutine signals "GetX", it's now in a state where it's waiting for "Return".

Or am I missing something?

Without specifying a developer visible model of time with respect to coroutine behavior, it's hard to talk about them being in one state and then another. I was tempted to ask Scott about his time model, but decided my remarks could just assume my own model. :-) I think a potentially concurrent model is implied by talking about fibers.

If I assume fibers (lightweight green threads), then on get a coroutine either keeps going because the next X is there, or it blocks until a producer signals X is in the pipe to awaken the consumer. So a consumer only indicates interest in getting an X because you can see it blocked on whatever primitive it expects to signal (a lightweight condition variable in my case). Here a pipe is like an on-demand future for a stream of X's, and looks like a generator or memoizing cache depending on whether the buffer is empty.

I can also imagine a coroutine definition with no real time element except as metaphor: it looks like two indendent continuations handing off data, but it's actually just a formal model in the language, implemented with unspecified time behavior. Here you'd ask a developer to imagine time behavior to grasp the model, then you'd say you weren't actually doing that and refuse to pin down details.

I'm particularly interested in semantics of starting and stopping, especially stopping that expresses failure. Will coroutine types imply what happens in producer or consumer failure? Or does the model define failure as impossible? (I know this is funny, but folks do that.)

I know this doesn't help analyze whether typing coroutines is simpler or not. But in the absence of a progress guarantee, or a way to examine coroutine status to make runtime decisions, I'm not sure what to make of a coroutine type in a contract -- except it means when you do get a value, it will be of the sort specified. I guess I'm vaguely curious whether types ever encompass time semantics, or whether they tend to address only timeless qualities.

I've been assuming Scott wants a producer coroutine to awaken a consumer as cheaply as possible so there's no performance criticism, and that strong typing helps them contract whether data put and gotten is acceptable to both. But that he doesn't want to specify time and progress behavior, which I'd like, or how either end disengages (like closing a pipe). Out-of-band behavior like "close" can be hard to union with type of content in the channel.

I'm particularly interested in semantics of starting and stopping, especially stopping that expresses failure. Will coroutine types imply what happens in producer or consumer failure? Or does the model define failure as impossible? (I know this is funny, but folks do that.)

I know of no truly satisfactory answer to this. I can offer two designs I've tried personally. They both turned out to work well in practice. You may consider this as good news, if you're practically inclined, or otherwise as an affront that demands a third solution to encompass both.

The low-level EDSL I linked above relies on Haskell's Maybe (in case of get) and Bool (for put) types to communicate if the peer coroutine has died. I was at first worried that checking the result all the time would be too cumbersome, but as it turns out that was mostly delegated to higher-level operations like putList.

OmniMark uses a different approach. The consumer always runs first, and the producer waits until it's asked for data. If the producer dies first, the consumer continues running normally; it can see that its source is at EOF. If the consumer dies first, the producer gets killed; only its always blocks will be run, and if they try to write anything into the sink a run-time error is raised. This story had a few refinements before we got it right.

I wouldn't call things any more complicated, really. It is quite possible for an untyped coroutine to be in a state where it expects something done before it resumes. As one example, Lua's untyped coroutines raise an exception in this situation.

Don't get me wrong. Your objection is valid, you've just overstated it a bit. It's similar to saying that typed value-returning functions are more complicated than untyped procedures because a call to a function expects a value.

You need at least three coroutines to cause the problem. You may have, for example, two producers P1 and P2 feeding one consumer C. When C suspends to P1, if P1 may resume P2 rather than yield a value to C, you hit the problem: the values P2 yields may be of a different type.

There are ways of resolving this issue. The one I've settled on is to simply disallow P1 from switching directly to P2, because it has no handle to it. The above configuration can be represented like this:

pipe
  (\sink-> P1 sink)
  (\source1->
    pipe
      (\sink-> P2 sink)
      (\source2-> C source1 source2))

Note that the only handles P1 and P2 are given are one sink each, both of them leading to C. The consumer picks from which source to get the next value, which resumes the appropriate producer.

I put some thought into this exact issue a while back (I was hacking together a little coroutine library in C#). This was indeed the best solution I could think of. Instead of allowing an open-ended top-level yield construct, make it a method on some typed object that knows the yielded and resumed types. If you don't have that object, you can't yield:

void DoStuff(Coro<int, string> coro) {
    // do stuff...
    string result = coro.Yield(1234);
    // more stuff...
}

I believe this problem is similar to supporting non-local returns in closures. (I.e. if a return inside a call to a closure should cause the outer calling method to return, how do you ensure it returns the right type?)