@phdthesis{gordon1992functional,
author = {Gordon, Andy},
title = {Functional Programming and Input/Output},
organization = {Cambridge University Press},
year = {1992},
month = {August},
abstract = {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.



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.},
url = {http://approjects.co.za/?big=en-us/research/publication/functional-programming-input-output/},
}