<p>This looks a lot like the I/O API described by Felleisen et al in <a href="http://www.ccs.neu.edu/racket/pubs/icfp09-fffk.pdf"><em>A Functional I/O System (or Fun for Freshman Kids)</em></a>.  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 <code>to-draw</code> handler, which produces the "output" for each state.</p>

<p>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.  </p>

<p>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.</p>

CC BY-SA 3.0
2012-11-28T07:33:15.447Z
2012-11-28T07:33:15.447Z
Sam Tobin-Hochstadt
<p>Just came across this post. </p>

<p>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: </p>

<p><code>E = Unit x Nats -&gt; E + O</code></p>

<p>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. </p>

CC BY-SA 3.0
2012-12-03T09:53:49.327Z
Thanks! Google found me Haynes and Friedman, "Abstracting Timed Preemption with Engines" (ftp://www.cs.indiana.edu/pub/techreports/TR178.pdf), and Dybvig and Hieb's "Engines from Continuations" (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.6124) Are there any other refs I've missed?
Neel Krishnaswami
CC BY-SA 3.0
2012-12-01T17:21:40.507Z
2012-12-01T17:21:40.507Z
Matthias
<p>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.:
<a href="https://lmcs.episciences.org/713" rel="nofollow noreferrer">Representations of Stream Processors Using Nested Fixed Points</a></p>
<p>UPDATED: the reference offered analyses the following two scenarios/specifications: those of</p>
<ul>
<li>a <em>continuous</em> (ie., computable)function from <code>Stream I</code> to <code>O</code>, for inputs of type <code>I</code>, and outputs of type <code>O</code> (the paper uses <code>A</code> and <code>B</code>, sorry)</li>
<li>a continuous function from <code>Stream I</code> to <code>Stream O</code></li>
</ul>
<p>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 <code>O</code>, and branching factor <code>I</code>, ie to <code>T(I,O) = mu X. O + (I -&gt; X)</code>: at each step of the computation, either immediately return the answer <code>o : O</code>, or else continue by polling the input stream for an additional input <code>i : I</code>...</p>
<p>The second is (only a bit) more subtle, and perhaps can best be understood as asking how to build results in <code>Stream O =def nu Y. O x Y</code> by coinduction, ie by showing how to compute the first output observation <code>o : O</code>, 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 <code> Stream I -&gt; Stream O</code> represented by non-well-founded processes <code>P(I,O)</code> built out out of finite well-founded trees, as
<code>P(I, O) =def nu Y. mu X. (O x Y) + (I -&gt; X))</code></p>
<p>The <code>T(I,O)</code> abstraction corresponds to the well-founded part of the resumption domain equation, and the <code>P(I,O)</code> abstraction to an iterated/nested fixed-point, rather along the lines (I think) of Andy Pitts' analysis (following Freyd) of <a href="https://www.cl.cam.ac.uk/%7Eamp12/papers/relpod/relpod.pdf" rel="nofollow noreferrer">mixed variance domain equations</a>.</p>
<p>Hancock, Setzer, Hyvernat and others explored the rich algebra of the <code>T(I,O)</code> construction (under the name 'interaction structures' or 'command-response interfaces')) in the case where at each input <code>i : I</code>, the range of possible outputs <code>O i</code> is allowed to <em>depend</em> on <code>i</code>. 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 <em>containers</em>/polynomial functors.</p>
<p>The relationship between JSP and the <code>T(I,O)/P(I,O)</code> constructions is discussed in various places, but most recently to my knowledge in Oleg Kiselyov's <a href="https://okmij.org/ftp/Computation/oxford-seminar.pdf" rel="nofollow noreferrer">slides  on stream <em>fusion</em></a> from a recent IFIP WG2.1 meeting, as well as in <a href="https://okmij.org/ftp/continuations/PPYield/yield-pp.pdf" rel="nofollow noreferrer">earlier work</a>.</p>

CC BY-SA 4.0
2023-04-26T11:23:19.323Z
Could you develop the answer described in the link?
J.y B.y
CC BY-SA 4.0
2023-04-25T16:04:42.270Z
2023-05-18T16:00:24.757Z
2023-05-18T16:00:24.757Z
James McKinna
<p>I've been playing around with <a href="http://homepages.inf.ed.ac.uk/gdp/publications/Powerdomain_Construction.pdf">resumptions</a> lately, mostly from Abramsky's classic paper <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.7024"><em>Retracing Some Paths in Process Algebra</em></a>. They are quite slick (basically solutions to the domain equation $R = I \to (O \times R)$), and very reminiscent of Kahn networks.</p>

<p>Of course, this observation is not original to me --- they form a traced monoidal category, and this fact was used by <a href="http://www.cs.ox.ac.uk/samson.abramsky/nfgoi.ps.gz">Abramsky and Jagadeesan</a> 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. </p>

<p>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 <em>Gordon Plotkin</em> 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. </p>

CC BY-SA 3.0
2012-12-01T17:51:16.420Z
As I was reading the question I thought to myself "I bet Neel will answer this one".
Andrej Bauer
CC BY-SA 3.0
2012-12-01T17:52:45.077Z
This might be a nice use-case for Eff-style opearations and handlers.
Andrej Bauer
CC BY-SA 3.0
2012-12-01T22:04:51.700Z
@AndrejBauer: I always think that for Neel's questions.
Dave Clarke
<reference-request><pl.programming-languages><functional-programming>
Resumption-based IO systems?
Neel Krishnaswami
# Resumption-based IO systems?

(Asked by: username_0 on 2012-11-26)

I've been playing around with [resumptions](http://homepages.inf.ed.ac.uk/gdp/publications/Powerdomain_Construction.pdf) lately, mostly from Abramsky's classic paper [*Retracing Some Paths in Process Algebra*](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.7024). 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](http://www.cs.ox.ac.uk/samson.abramsky/nfgoi.ps.gz) 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.

**Tags:** reference-request, pl.programming-languages, functional-programming

> **Comments:**
> **username_1**: As I was reading the question I thought to myself "I bet Neel will answer this one".  
> **username_1**: This might be a nice use-case for Eff-style opearations and handlers.  
> **username_2**: @AndrejBauer: I always think that for Neel's questions.  

---

## 3 answers

### Answer by username_3 on 2012-11-28. Score: 8 | Accepted answer

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)*](http://www.ccs.neu.edu/racket/pubs/icfp09-fffk.pdf). 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 by username_4 on 2012-12-01. Score: 6

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.

> **Comments:**
> **username_0**: Thanks! Google found me Haynes and Friedman, "Abstracting Timed Preemption with Engines" (ftp://www.cs.indiana.edu/pub/techreports/TR178.pdf), and Dybvig and Hieb's "Engines from Continuations" (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.6124) Are there any other refs I've missed?  

---

### Answer by username_5 on 2023-04-25. Score: 2

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](https://lmcs.episciences.org/713)

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](https://www.cl.cam.ac.uk/%7Eamp12/papers/relpod/relpod.pdf).

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*](https://okmij.org/ftp/Computation/oxford-seminar.pdf) from a recent IFIP WG2.1 meeting, as well as in [earlier work](https://okmij.org/ftp/continuations/PPYield/yield-pp.pdf).

> **Comments:**
> **username_6**: Could you develop the answer described in the link?  

---

