Bibliography: Functional Programming

Monadic State: Axiomatization and Type Safety

Type safety of imperative programs is an area fraught with difficulty and requiring great care. The ML solution to the problem, originally involving imperative type variables, has recently been simplified to the syntactic-value restriction. In Haskell, the problem is addressed in a rather different way using explicit monadic state. We present an operational semantics for state in Haskell and the first full proof of type safety. We demonstrate that the semantic notion of value provided by the explicit monadic types is sufficient to avoid any problems with generalization.

Parametricity and Unboxing with Unpointed Types

In lazy functional languages, bottom is typically an element of every type. While such "pointedness" provides great flexibility, it also comes at a cost. In this paper we explore the consequences of allowing unpointed types in a lazy functional language like Haskell. We use the type (and class) system to keep track of pointedness (and hence recursion also), and show the consequences for parametricity and for controlling evaluation order and unboxing.

Warm Fusion: Deriving Build-Catas from Recursive Definitions

Program fusion is the process whereby separate pieces of code are fused into a single piece, typically transforming a multi-pass algorithm into a single pass. Recent work has made it clear that the process is especially successful if the loops or recursions are expressed using catamorphisms (e.g. foldr) and constructor-abstraction. In this paper we show how to transform recursive programs into this form automatically, thus enabling the fusion transformation to be applied more easily than before.

Structuring Depth First Search Algorithms in Haskell

Depth-first search is the key to a wide variety of graph algorithms. In this paper we express depth-first search in a lazy functional language, obtaining a linear-time implementation. Unlike traditional imperative presentations, we use the structuring methods of functional languages to construct algorithms from individual reusable components. This style of algorithm construction turns out to be quite amenable to formal proof, which we exemplify through a calculational-style proof of a far from obvious strongly-connected components algorithm.

Lazy Functional State Threads

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 stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language. The security of the encapsulation is assured by the type system, using parametricity. Intriguingly, this parametricity requires the provision of a (single) constant with rank-2 polymorphic type.

A Natural Semantics for Lazy Evaluation

We define an operational semantics for lazy evaluation which provides an accurate model for sharing. The only computational structure we introduce is a set of bindings which corresponds closely to a heap. The semantics is set at a considerably higher level of abstraction than operational semantics for particular abstract machines, so is more suitable for a variety of proofs. Furthermore, because a heap is explicitly modelled, the semantics provides a suitable framework for studies about space behaviour of terms under lazy evaluation.

Lazy Imperative Programming

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 a possible implementation within Glasgow Haskell.