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

  1. Introduction
  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
  9. 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.