# Functional Programming and Input/Output.

Andrew D. Gordon.
Distinguished
Dissertations in Computer Science. Cambridge University Press, 1994. ISBN 0
521 47103 6 hardback. Publication dates 29 September 1994 (UK) and 27 January
1995 (USA).

A PDF version is available online since August 14,
2007, as permitted by Cambridge University
Press, who own the copyright.

##
Table of Contents

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

There is an extensive bibliography and a Preface that discusses developments
since the submission of the dissertation. An abridged
version of Chapter 7 appeared in the FPCA'93 conference in Copenhagen.
##
Summary

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.
The first half develops the operational theory of a semantic metalanguage used
in the second half. The metalanguage **M** 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 **M**---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.

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

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 **H** to include the other three mechanisms and
prove that the three are equivalent to each other in expressive power.

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.