State in functional languages

The following four related papers, all on the topic of mutable state in
non-strict functional languages, are available by FTP.  The first two are as
yet unpublised; the last two are published.  

I'm posting this to the types mailing list as well as the functional
programming ones because there is an interesting use of rank-2 polymorphism
to ensure safe encapsulation of state; this shows up mainly in the
first-mentioned paper.  The other point of interest from a typing point of
view is that the usual unfortunate interaction of polymorphism with
assignment doesn't occur (see the last-mentioned paper)

All can be got from the FTP site ftp.dcs.glasgow.ac.uk.


		Lazy Functional State Threads
	J Launchbury and SL Peyton Jones, Glassgow University

	FTP: pub/glasgow-fp/drafts/state.ps.Z

Some algorithms make critical internal use of updatable state, even
though their external specification is purely functional.  Based on
earlier work on monads, we present a way of securely encapsulating
such stateful computations, in the context of a non-strict,
purely-functional language.  

There are two main new developments in this paper.  First, we show how
to use the type system to securely encapsulate stateful computations,
including ones which manipulate multiple, named, mutable objects.
Second, we give a formal semantics for our system.

(Submitted to Programming Languages Design and Implementation, 1994.)

	Lazy Depth-First Search and Linear Graph Algorithms in Haskell
		DJ King and J Launchbury, Glasgow University

	FTP: pub/glasgow-fp/drafts/linear-dfs.ps.Z

Depth-first search is the key to a wide variety of graph algorithms.
In this paper we explore the implementation of depth first search in a
lazy functional language. For the first time in such languages we
obtain a linear-time implementation.  But we go further.  Unlike
traditional imperative presentations, algorithms are constructed from
individual components, which may be reused to create new
algorithms. Furthermore, the style of program is quite amenable to
formal proof, which we exemplify through a calculational-style proof
of a strongly-connected components algorithm.

(Submitted to Lisp & Functional Programming 1994.)

		Lazy imperative programming
		J Launchbury, Glasgow University

	FTP: pub/glasgow-fp/papers/lazy-imperative-programming.ps.Z

In this paper we argue for the importance of lazy state, that is,
sequences of imperative (destructive) actions in which the actions are
delayed until their results are required. This enables state-based
computations to take advantage of the control power of lazy evaluation.
We provide some examples of its use, and describe an implementation
within Glasgow Haskell.

Proc ACM Sigplan Workshop on State in Programming Languages, Copenhagen,
June 1993 (available as YALEU/DCS/RR-968, Yale University), pp46-56.

		Imperative functional programming
	SL Peyton Jones and  PL Wadler, Glasgow University

	FTP: pub/glasgow-fp/papers/imperative.ps.Z

We present a new model, based on monads, for performing input/output in a
non-strict, purely functional language.  It is composable, extensible,
efficient, requires no extensions to the type system, and extends smoothly
to incorporate mixed-language working and in-place array updates.

ACM conference on Principles of Programming Languages, Charleston, Jan 1993