Every functional programmer knows the technique of “replacing failure by a list of successes” (Wadler, 1985), but wise programmers are aware also of the possibility that the list will be empty or (worse) divergent. In fact, the “lists of successes” technique is equivalent to the incomplete depth-first search strategy used in Prolog.

At heart, the idea is quite simple: whenever we might want to use a ‘multi-function’ such as ‘f’ [ratio ][ratio ] α [Rarr ] β that can return many results or none, we replace it by a genuine function f [ratio ][ratio ] α → β stream that returns a lazy stream of results, and rely on lazy evaluation to compute the answers one at a time, and only as they are needed. For the sake of clarity, I will distinguish between the types of finite lists (α list) and of potentially infinite, lazy streams (α stream), though both may be implemented in the same way. Following the conventions used in ML, type constructors follow their argument types.

One well known algorithm is the Fast Fourier Transform (FFT). An efficient iterative version of the FFT algorithm performs as a first step a bit-reversal permutation of the input list. The bit-reversal permutation swaps elements whose indices have binary representations that are the reverse of each other. Using an amortized approach, this operation can be made to run in linear time on a random-access machine. An intriguing question is whether a linear-time implementation is also feasible on a pointer machine, that is, in a purely functional setting. We show that the answer to this question is in the affirmative. In deriving a solution, we employ several advanced programming language concepts such as nested datatypes, associated fold and unfold operators, rank-2 types and polymorphic recursion.

We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete. The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of independent interest, this paper can be read as a tutorial on this proof technique for reasoning about relations between type theories.

Since its inception in 1987, Haskell has provided a focal point for research in lazy functional programming. During this time the language has continually evolved, as a result of both theoretical advances and practical experience. Haskell has proved to be a powerful tool for many kinds of programming tasks, and applications in industry are beginning to emerge. The recent definition of Haskell 98 provides a long-awaited stable version of the language, but there are many exciting possibilities for future versions of Haskell.

The fourth Haskell Workshop will be held as part of the PLI 2000 colloquium on Principles, Logics, and Implementations of high-level programming languages in Montreal, 17th September 2000. Previous Haskell Workshops have been held in Paris (1999), Amsterdam (1997) and La Jolla (1995). Following on from these workshops, a special issue of the Journal of Functional Programming will be devoted to Haskell. Possible topics include, but are not limited to:

* Critiques of Haskell 98;

* New proposals for Haskell;

* Applications or case studies;

* Programming techniques;

* Reasoning about programs;

* Semantic issues;

* Pedagogical issues;

* Implementation.

Contributors to any of the Haskell workshops are invited to submit full papers to the special issue on Haskell, but submission is open to everyone. Submissions should be sent to guest editor (address below), with a copy to Nasreen Ahmad ([email protected]). Submitted articles should be sent in postscript format, preferably gzipped and uuencoded. In addition, please send, as plain text, title, abstract, and contact information. The submission deadline is 1st February 2001. For other submission details, please consult an issue of the Journal of Functional Programming or see the Journal's web pages.

This pearl is about some functions whose definitions seem to require a language with dependent types. We describe a technique for defining them in Haskell or ML, which are languages without dependent types.

Consider, for example, the scheme defining zipWith in figure 1. When this scheme is instantiated with n equal to 1 we obtain the standard function map. In practice, other instances of the scheme are often useful as well.

Figure 1 cannot be used as a definition of a function in Haskell because of the ellipses ‘...’. More importantly, the type of zipWith is parameterized by n, which seems to indicate the need for dependent types. However, as mentioned above, Haskell does not allow dependent types.

We present our experience in implementing a group communication toolkit in Objective Caml, a dialect of the ML family of programming languages. We compare the toolkit both quantitatively and qualitatively to a predecessor toolkit which was implemented in C. Our experience shows that using the high-level abstraction features of ML gives substantial advantages. Some of these features, such as automatic memory management and message marshalling, allowed us to concentrate on those pieces of the implementation which required careful attention in order to achieve good performance. We conclude with a set of suggested changes to ML implementations.

It is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-one map, which causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (λN) and the other to sequent calculus (λL). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a ‘cut-free’ fragment (λLcf). This fragment generates exactly the typeable lambda terms in normal form. The cut elimination theorem becomes a simple consequence of the fact that typed lambda terms possess a normal form.

Logical frameworks and meta-languages are intended as a common substrate for representing and implementing a wide variety of logics and formal systems. Their definition and implementation have been the focus of considerable work over the last decade. At the heart of this work is a quest for generality: A logical framework provides a basis for capturing uniformities across deductive systems and support for implementing particular systems. Similarly a meta-language supports reasoning about and using languages.

Logical frameworks have been based on a variety of different languages including higher-order logics, type theories with dependent types, linear logic, and modal logic. Techniques of representation of logics include higher-order abstract syntax, inductive definitions or some form of equational or rewriting logic in which substitution is explicitly encoded.

Examples of systems that implement logical frameworks include Alf, Coq, NuPrl, HOL, Isabelle, Maude, lambda-Prolog and Twelf. An active area of research in such systems is the study of automated reasoning techniques. Current work includes the development of various automated procedures as well as the investigation of rewriting tools that use reflection or make use of links with systems that already have sophisticated rewriting systems. Program extraction and optimization are additional topics of ongoing work.