Functional Programming and Input/Output
The following newly published book may be of interest to TYPES subscribers.
It is a study of the semantics of I/O in functional languages. Perhaps the
most original aspect is its use of a typed form of Abramsky's applicative
bisimulation together with co-induction to yield an entirely operational
theory of a functional language and its I/O mechanism.
It is a revised version of my PhD dissertation. Chapter 8, on monadic I/O, is
largely new, and in a Preface I discuss developments since submission of the
dissertation. There is an extensive bibliography of I/O mechanisms for
I enclose a summary of the book, also available at URL
Phone: (+44) 223 334411 University of Cambridge Computer Laboratory,
Fax: (+44) 223 334679 New Museums Site, CAMBRIDGE CB2 3QG, UK.
Functional Programming and Input/Output.
Andrew D. Gordon.
Distinguished Dissertations in Computer Science. Cambridge University Press,
1994. ISBN 0 521 47103 6 hardback. Publication date 29 September. UK net
price 25 pounds. Ring +44 1223 325970 or fax +44 1223 325959 at any time to
order by credit card.
Table of Contents
2. A Calculus of Recursive Types
3. A Metalanguage for Semantics
4. Operational Precongruence
5. Theory of the Metalanguage
6. An Operational Theory of Functional Programming
7. Four Mechanisms for Teletype I/O
8. Monadic I/O
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
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
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.