Lambda the Ultimate

Jeremy Gibbons and Bruno C. d. S. Oliveira (2006). The Essence of the Iterator Pattern. Submitted for publication.

The Iterator pattern gives a clean interface for element-by-element access to a collection. Imperative iterations using the pattern have two simultaneous aspects: mapping and accumulating. Various functional iterations model one or other of these, but not both simultaneously. We argue that McBride and Paterson's idioms, and in particular the corresponding traverse operator, do exactly this, and therefore capture the essence of the Iterator pattern. We present some axioms for traversal, and illustrate with a simple example, the repmin problem.

The core of the solution is from McBride and Paterson's paper Applicative programming with effects, which wasn't posted to the home page before, but which was mentioned a couple of times in the LtU forum.

The context of this reseach is previous attempts to capture functional analogues of OOP design patterns:

Recently we have argued that pure datatype-generic maps are the functional analogue of the Iterator design pattern. It was partly while reflecting on that argument that we came to the (contradictory) position presented here.

More goodness appears to be in store for GHC, the Haskell compiler:

We introduce a variant of System F that uses a single mechanism to enable the type preserving translation of generalised abstract data types (GADTs), type classes with associated types and functional dependencies, as well as closed type functions. The core idea is to pass around explicit evidence for type equalities, just like System F passes types explicitly. We use this evidence to justify type casts encoding non-syntactic type equalities induced by the mentioned source language features. In particular, we don't need special typing rules for pattern matching on GADTs, we can easily combine GADTs with type classes, and we can relax restrictions on programs involving associated types or functional dependencies.

From SPJ: "I intend to change GHC to use FC as its intermediate language."

Looking at it, from the very, very limited understand I have, it seems that the whole coercions being witnesses to type constraints looks similar to how proof witnesses are used in Epigram. Maybe someone more knowledgeable can explain the similarity?