Resumption-based IO systems?

Question

I've been playing around with resumptions lately, mostly from Abramsky's classic paper Retracing Some Paths in Process Algebra. They are quite slick (basically solutions to the domain equation $R = I \to (O \times R)$), and very reminiscent of Kahn networks.

Of course, this observation is not original to me --- they form a traced monoidal category, and this fact was used by Abramsky and Jagadeesan to give semantics to linear logic. At any rate, note that if you feed a resumption $r$ an input of type $I$, you get an output of type $O$ and an updated resumption $r'$, which is what lets you model the fact that a dataflow node can change as it sees inputs come in.

As a result, it seems like they could give a nice API for building I/O transducers in a higher-order language like ML or Haskell, but I can't seem to find any papers describing such a thing. But they've been around for decades, and Gordon Plotkin invented them, so it's not like they've languished in obscurity. So I was wondering if anyone had seen them put to such use.

Answer 1

This looks a lot like the I/O API described by Felleisen et al in A Functional I/O System (or Fun for Freshman Kids). Basically, you write (in the simpler, non-distributed setting), a series of event handlers, each of which accepts the current state, and returns an updated state. Finally, there's a to-draw handler, which produces the "output" for each state.

If we recast this API slightly, we can package up the handlers and the current state together, and each time a handler returns both a new state and a new set of handlers. We might call this package of state and operations an "object". :) If we then make the result a pair of this object, and the "output", then we have exactly the type of resumptions.

Interestingly, in the paper, Felleisen et al do exactly this when moving to the distributed setting -- every operation returns a pair of new state and "output" in the form of messages to be sent to the other participants in the system.

Answer 2

Just came across this post.

Do go back to the early 1980s. Friedman et al @ Indiana invented the concept of 'engines' in the context of Scheme 84 (not Scheme 48). An engine is roughly an element of this type:

E = Unit x Nats -> E + O

You can also use I instead of Unit and the x Nats part is optional. You can think of these as a form of resumptions, and depending on context engines are more practical than resumptions.

Answer 3

See also the various papers by Hancock and coauthors about interactive programs in type theory, and stream processing (and hence back to the original stream-based IO models of Landin, KRC, Miranda(TM), precursors to haskell, as well as the underlying data and control model of Jackson Structured Programming (JSP)), esp.: Representations of Stream Processors Using Nested Fixed Points

UPDATED: the reference offered analyses the following two scenarios/specifications: those of

• a continuous (ie., computable)function from Stream I to O, for inputs of type I, and outputs of type O (the paper uses A and B, sorry)
• a continuous function from Stream I to Stream O

By somewhat 'elementary' (philosophical) considerations (plus allusions to the Bar Theorem of Brouwer), the first situation is shown to reduce to considering well-founded I/O trees, with leaves in O, and branching factor I, ie to T(I,O) = mu X. O + (I -> X): at each step of the computation, either immediately return the answer o : O, or else continue by polling the input stream for an additional input i : I...

The second is (only a bit) more subtle, and perhaps can best be understood as asking how to build results in Stream O =def nu Y. O x Y by coinduction, ie by showing how to compute the first output observation o : O, and then how to compute the rest of the output stream. The first part reduces to the first scenario, so roughly you end up with Stream I -> Stream O represented by non-well-founded processes P(I,O) built out out of finite well-founded trees, as P(I, O) =def nu Y. mu X. (O x Y) + (I -> X))

The T(I,O) abstraction corresponds to the well-founded part of the resumption domain equation, and the P(I,O) abstraction to an iterated/nested fixed-point, rather along the lines (I think) of Andy Pitts' analysis (following Freyd) of mixed variance domain equations.

Hancock, Setzer, Hyvernat and others explored the rich algebra of the T(I,O) construction (under the name 'interaction structures' or 'command-response interfaces')) in the case where at each input i : I, the range of possible outputs O i is allowed to depend on i. The type of such trees was first introduced by Petersson and Synek in (1989) as an indexed/dependent generalisation of W-types in Martin-Lof's type theory and has a rich theory in modern times via indexed/dependent containers/polynomial functors.

The relationship between JSP and the T(I,O)/P(I,O) constructions is discussed in various places, but most recently to my knowledge in Oleg Kiselyov's slides on stream fusion from a recent IFIP WG2.1 meeting, as well as in earlier work.