Editing The I/O problem (section)

== On being denotative ==

While the [https://okmij.org/ftp/Computation/IO-monad-history.html prevailing] approach to I/O is based on combining the imperative and functional programming styles:

<blockquote>
The special claim of <tt>ISWIM</tt> is that it grafts procedural
notions onto a purely functional base without disturbing
many of the desirable properties.

:<small>[https://dl.acm.org/doi/pdf/10.1145/365230.365257 The Next 700 Programming Languages], Peter J. Landin (page 8 of 10).</small><!-- 1966 -->
</blockquote>

<blockquote>
We need the concept of a ‘process’ as opposed to a function. Intuitively a
process is something that (in general) is geared towards continuation while a
function is geared towards termination. Processes have an input channel on
which an input stream (a potentially infinite sequence of tokens) is coming
in and an output channel on which an output stream is coming out. A
typical process is the control of a traffic light system: it is geared towards
continuation, there is an input stream (coming from the pushbuttons for
pedestrians) and an output stream (regulating the traffic lights). Text editing
is also a process. In fact, even the most simple form of I/O is already a
process.

:<small>[https://repository.ubn.ru.nl/bitstream/handle/2066/17274/13362.pdf The impact of the lambda calculus in logic and computer science], Henk Barendregt (page 21 of 36).</small><!-- 1997 -->
</blockquote>

which is achieved in Haskell [https://dl.acm.org/doi/pdf/10.1145/319838.319848 by using types]:

<blockquote>
The main program
(function <code>main</code> from module <code>Main</code>, which
we write <code>Main.main</code>) has type <code>IO ()</code>, that is, it
is a computation which performs some I/O and
returns an uninteresting result. The "trivial"
type <code>()</code> has only one value, the unit value, which
is also written <code>()</code>.

:<small>[https://web.archive.org/web/20080325064317/http://www-fp.dcs.st-and.ac.uk/~kh/papers/io-tutorial/section3_2.html#SECTION0002000000000000000 Monadic I/O in Haskell 1.3], Andrew D. Gordon and Kevin Hammond.</small><!-- 1996 -->
</blockquote>

...there has also been interest in using denotational semantics or models due to the advantages they provide:

<blockquote>
For example, there
are several simple variations on the model for processes [[https://dl.acm.org/doi/pdf/10.1145/322123.322134 <span></span>]].

In the face of such an abundance, it is best to recall the motivation for seeking
such models. They provide a useful mathematical framework for the analysis of
programs, and for developing logical systems for proving their properties.

:<small>[https://www.scss.tcd.ie/Matthew.Hennessy/pubs/old/HMjacm85.pdf Algebraic Laws for Nondeterminism and Concurrency], Matthew Hennessy and Robin Milner (first page).</small><!-- 1985 -->
</blockquote>

But there is an important prerequisite that needs to be observed when attempting to use such models:

<blockquote>
[...] if either the mathematics or the logic is to have any relevance, a link must be made
between the denotational model and the behavior, or operational semantics, of the
programs.
</blockquote>

So while only having an operational semantics for <code>IO a</code> might 
[http://conal.net/blog/posts/is-haskell-a-purely-functional-language#comment-625 not]
be ideal,
[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.13.9123&rep=rep1&type=pdf only having a denotational model]:

<blockquote>
<small>(page 19 of 60)</small>

<haskell>
          type IO a = World -> (a, World)
</haskell>

<haskell>
          type IO a = (a, Set Trace)
          type Trace = [Event]
          data Event = PutChar Char | GetChar Char | ...
</haskell>
</blockquote>

...would be <i>insufficient:</i>

<blockquote>
It is all very well to aim for a more "abstract" and a
"cleaner" approach to semantics, but if the plan is to be any
good, the operational aspects cannot be completely ignored. The
reason is obvious: in the end the program still must be run on a
machine - a machine which does not possess the benefit of
"abstract" human understanding, a machine that must operate with
finite configurations.

:<small>[https://www.cs.ox.ac.uk/files/3222/PRG02.pdf Outline of a Mathematical Theory of Computation], Dana Scott (page 8 of 30).</small><!-- 1970 -->
</blockquote>

<blockquote>
[...] The meaning of a conventional computer program, as far as
a user is concerned, is just the mathematical function it evaluates. But we users
are <i>inside</i> our interactive systems; we care about what continually goes on. The
meaning surely lies in the whole conversation, not just its end-result. (Indeed there
may be no end-result, since there may have been no goal.)

:<small>[https://perso.ens-lyon.fr/daniel.hirschkoff/dea/papers/milner-infomatics.pdf Turing, Computing and Communication], Robin Milner (page 8 of 12).</small><!-- 1997 -->
</blockquote>