[Prev][Next][Index][Thread]

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
functional languages.

I enclose a summary of the book, also available at URL

	http://www.cl.cam.ac.uk/users/adg/fpio.html

Andrew Gordon.

Phone:	(+44) 223 334411	University of Cambridge Computer Laboratory,
Fax:	(+44) 223 334679	New Museums Site, CAMBRIDGE CB2 3QG, UK.
Email:	adg@cl.cam.ac.uk
Web:	http://www.cl.cam.ac.uk/users/adg/

---------------------------------------------------------------------------

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 

 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 

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.