This paper offers two things:
The argumentation applies to virtually all functional languages. The code examples are in Haskell, with some names inspired by Scheme.
Warning: The provided software has only been proven correct and not been tested. Feedback and patches are welcome. (Especially if someone uses QuickCheck to check the algebraic laws and the different implementations for the same thing.)
The bread and butter data structure of the functional programmer is the list. And this it already imprecise, since actually the so-called "lists" in functional languages are an implementation of sequences with functional stacks (since access happens at one end only). Functional languages provide a lot of very useful operations (like map, filter, elem, ++) on those data type and thus make us forget that we are precisely working with functional stacks.
But this illusion has its contradictions. For example, it is hard to explain why the operations last and init (aka but_last) do have infinitely worse performance than head and tail (aka first and but_first)! Not only do they need more time, they also need more space of an order of magnitude.
tails = scanl1 tail xs -- Needs linear time and space. inits = scanl1 init xs -- Needs quadratic time and space.
Although functional languages are not genuinely popular for their efficiency we can easily manipulate lists of some million elements. (If the calculation takes long just take a coffee while the imperative programmer is still coding and debugging...) But the bad space performance of inits may mean that the result will not even fit in the computer's memory! And there is no better way to implement inits with the standard lists!
Fortunately there is a solution for that problem of yelling insymmetry and injustice. Chris Okasaki's functional deque data structure is like the functional stack, only that it implements init, last, and snoc in the same constant time and space as head, tail, and cons (aka (:))
My Deque Module implements these data structures and to use it, you just have to write on top of your Haskell Program:
import Deque import Prelude hiding ( head, tail, last, init, null, length, reverse, (++) )
The features hidden from the Prelude are imported from Deque and due to the overloading they can now be used on Deques and the classical (functional stack) lists alike. For example, if xs is a Deque, both of the lists inits and tails above will only need linear time to calculate. (And therefore also occupy at most linearly much memory, since you need time to fill the memory.) For example:
inits_list = scanl1 init [1..i] inits_deque = scanl1 init $ deque [1..i]
Choose a large i such that [1..i] still can be evaluated. inits_deque can then be evaluated, too, but probably not inits_list.
Deques put an end to the tyranny of one end of the sequence over the other. They even allow both take and drop to share their result with the structure instead of copying it (as classical take does). However, this can't be done for append (aka (++)), and furthermore all three functions need linear time, although they just "cut and glue" sequences apart and together. The same problem holds for the function at (aka (!!)) which just delivers one single element, but needs linear time.
Mathematically, Sequences are a function from the integers 1 to N. (Or from 0 to N-1, but this contradicts the notion of a "first" (aka 1st) element.) Therefore it should be legitimate to use all kind of index-based operations on them. So I specified a list of useful operations on Sequences and then I noted that all of them could be implemented optimally in logarithmic time. The first challenge of this project was to make sensible groups of those operations so one doesn't get lost in details. The type class definition in the Sequence Module does exactly this.
Furthermore I thought a bit about balancing and without having it expected I discovered an astonishing simple balancing algorithm. Besides implementing the algorithm I have also written up my derivation which makes much use of simple goal-driven reasoning instead of guesswork or creativity or looks into text books.
Since the tree implementation of Sequences in any case needs a size or length field in every node, I had the idea to construct a simple balancing algorithm which uses this data to check the balancing condition. This algorithm was easily written, only I had problems with the proof which was after some time explained by a simple test of the program which failed.
Incidentally I read Stephen Adams paper on the subject (I had found the reference in the GHC sources when looking for something different, but similar: FiniteMap implementations). But his solution was not better than mine: he jocularly called a function without verifying that its very strict precondition holds. Furthermore I don't like his proof at all, and his program is ugly :->.
So I developed a new program from scratch and this is really, really nice and short. The proof is still relatively long and works with a lot of cases, which I treated only formally without caring for intuitive explanations, but at least the proof is part of the program and used to derive some parts of it, so that we don't need to think much, and know why things are as they are. So the program is not really an example of a complete formal derivation, but still a nice example of a pragmatical approach of development. (And the first correct proof and program with this algorithm although it might already be in the paper of Nievergelt and Reingold which Adams cites, but which I couldn't yet read. Anyway, in 1973 they didn't write as nice, abstract programs as we can do now. :-)
Compared with Stephen Adams' program, I also gain simplicity, because I use Leaf Trees and for those the contained elements "don't get in the way" when rebalancing. It also allows to use binary Constructor Functions for Nodes, which can be written infix and that makes it really readable like a short story. But thanks to a transformation pointed out by Ralf Hinze the algorithm can also easily be ported to the Internal Trees used by Binary Seach Trees. We could even go so far and make the rebalancing algorithm independant of the concrete data structure which we acces only be functions. This, however, is too easy in functional programming as to merit special research. (Only C++ Programmers need that.)
In this section I want to explain the difference between my Sequences (according to the Dessy Approach) and those usually constructed by algorithm researchers. In functional languages it does perhaps not suffice to say "Dessy is for prototyping", since even when functional programmers implement an efficient algorithm, they might state that this is only a very succinct prototype of the more complicated (and more efficient) imperative version.
However, Okasaki provides as first example in the User's Guide of his Edison library, a linear-time breadth-first tree traversal (using the Functional Queue), which is very much like Dijkstra's algorithm -- the first example of most imperative algorithm libraries.
Dessy, on the other hand, is not made for algorithm prototyping, but rather for specification prototyping. For example there exists a (non-trivial) linear-time algorithm to calculate the "Largest Rectangle under a Histogram" of a Sequence (the problem is isomorphic to Tournament Construction). But what is the Largest Rectangle under a Histogram? Well, here is the specification:
rectangle_area xs = length xs * minimum xs largest_rectangle_specification = maximum . map rectangle_area . segments segments = concat . map inits . tails
Viewn as an algorithm, this specification has quadratic running time (since there are quadratically many segments of a list). And here apply just the same arguments as seen above: regarding the time you could wait, but with Sequences as functional stacks, you might run out of memory. The Functional Deque, however, let's you execute your specification. Indeed we can go one step further in developing the algorithm:
-- We want to exploit the law that
-- provided (xs!!i) = minimum xs
-- then lra xs = lra (take (i-1) xs) `min` lra (drop i xs) `min' (xs!!i * length xs)
-}
lra_simple xs =
let i = head $ findIndizes (==(minimum xs)) xs
in lra_simple (take i xs) `min` lra_simple (drop (i+1) xs) `min` (xs!!i * length xs)
This has expected NlogN running-time on random input, but with a sorted sequence it will still use quadratically much memory, if Sequences are Functional Stacks, not with the Queues. The final algorithm however, does only a single pass over the sequence and doesn't do any take or drop any more. So it works with any Sequence implementation. Only to execute the specification and the intermediate forms was it necessary to have a Sequence implementation which doesn't "arbitrarily punish" the use of some operations.
Another very simple example is the standard way to transform a tree into a list:
inorder Empty = [] inorder (Node l x r) = inorder l ++ [x] ++ inorder r
Again we have quadratic running time, since ++ traverses and copies all of its left argument. Perhaps the reader is trained to transform that code to make it faster: one can use an accumulator to replace ++. But the simpler solution is to use a better Sequence implementation. The beauty of the program is preserved, and the program becomes asymptotically optimal. It's a pity that students are usually thaught the other way. How then should they learn Reuse and Abstraction?
TODO: Add an example on prototyping / specification, possibly stolen from the Z context. Since I open up a new field here, I want to have more examples than the other guys and gals.
The focus of the Deque module is to give a symmetric optimal performance to the standard list functions. It is completely compatible with the features of Prelude and can easily be used in their place.
The Sequence module, on the other hand, builds up a whole new abstraction from basic principles. It does also provide an efficient and useful implementation, but due to different type class definition this can't be used exchangeably with the classical (stack) lists or the Deques.
Basically Deques they fix a simple performance problem, while Sequences are a whole new design. I consider it an open problem to design a Sequence class that could be part of a standard library standard.