Last Modified On Thu Feb  2 16:09:39 1995 By Andy Gordon

<title>
Functional Programming and Input/Output.
</title>

<h1>Functional Programming and Input/Output.</h1>

Andrew D. Gordon.<p>

<a href="http://www.cs.man.ac.uk/fmethods/dds/dds.html"> Distinguished
Dissertations in Computer Science</a>.  <a
href="http://www.cup.cam.ac.uk/">Cambridge University Press</a>, 1994.  ISBN 0
521 47103 6 hardback.  Publication dates 29 September 1994 (UK) and 27 January
1995 (USA).  UK net price 25 pounds.  Ring +44 1223 325970 or fax +44 1223
325959 at any time to order by credit card from Cambridge.  In USA ring
toll-free 1-800-872-7423.

<h2>
Table of Contents
</h2>

<ol>
<li> Introduction
<li> A Calculus of Recursive Types
<li> A Metalanguage for Semantics
<li> Operational Precongruence
<li> Theory of the Metalanguage
<li> An Operational Theory of Functional Programming
<li> Four Mechanisms for Teletype I/O
<li> Monadic I/O
<li> Summary
</ol>

There is an extensive bibliography and a Preface that discusses developments
since the submission of the dissertation.  An <a
href="ftp://ftp.cl.cam.ac.uk/papers/adg/index.html#fpca93">abridged
version</a> of Chapter 7 appeared in the FPCA'93 conference in Copenhagen.

<h2>
Summary
</h2>

A common attraction to functional programming is the ease with which proofs
can be given of program properties.  A common disappointment with functional
programming is the difficulty of expressing input/output (I/O) while at the
same time being able to verify programs.  In this dissertation we show how a
theory of functional programming can be smoothly extended to admit both an
operational semantics for functional I/O and verification of programs engaged
in I/O.<p>

The first half develops the operational theory of a semantic metalanguage used
in the second half.  The metalanguage <b>M</b> is a simply-typed
lambda-calculus with product, sum, function, lifted and recursive types.  We
study two definitions of operational equivalence: Morris-style contextual
equivalence, and a typed form of Abramsky's applicative bisimulation.  We
prove operational extensionality for <b>M</b>---that these two definitions
give rise to the same operational equivalence.  We prove equational laws that
are analogous to the axiomatic domain theory of LCF and derive a co-induction
principle.  <p>

The second half defines a small functional language, <b>H</b>, and shows how
the semantics of <b>H</b> can be extended to accommodate I/O.  <b>H</b> is
essentially a fragment of Haskell.  We give both operational and denotational
semantics for <b>H</b>.  The denotational semantics uses <b>M</b> in a case
study of Moggi's proposal to use monads to parameterise semantic descriptions.
We define operational and denotational equivalences on <b>H</b> and show that
denotational implies operational equivalence.  We develop a theory of <b>H</b>
based on equational laws and a co-induction principle.<p>

We study simplified forms of four widely-implemented I/O mechanisms:
side-effecting, Landin-stream, synchronised-stream and continuation-passing
I/O.  We give reasons why side-effecting I/O is unsuitable for lazy languages.
We extend the semantics of <b>H</b> to include the other three mechanisms and
prove that the three are equivalent to each other in expressive power.<p>

We investigate monadic I/O, a high-level model for functional I/O based
on Wadler's suggestion that monads can express interaction with state in a
functional language.  We describe a simple monadic programming model, and give
its semantics as a particular form of state transformer.  Using the semantics
we verify a simple programming example.<p>

<ADDRESS>
<a href="http://www.cl.cam.ac.uk/users/adg">Andrew Gordon</a>, adg@cl.cam.ac.uk
</ADDRESS>