Following Hutton, we can define a fold function on lists by means of the following properties. For sets α and β, define the set of all functions f:β×α→β which we'll call right actions of α on β and denoted by Aβ,α . Also when the function f is clear from the context, we'll just write b⋅a for f(b,a). The fold function can be defined as
such that, for a given b∈βthe following properties hold:
where xˉ:x is the list obtained as conjunction of a list xˉ with an element x of α (in Clojure(conjxˉx)).
Now for fixed b, (u1) and (u2) form indeed a universal property, i.e. if such a function exists then it's unique and fold is fully caracterized by these properties. Unicity is proven by means of induction: assume there's functions f and f′which satisfy (u1) and (u2) but which disagree i.e. ¬f(f,b,x^)=f′(f,b,x^) on some list x^=xˉ:x. Now by (u2) they also need to disagree on xˉ, hence x^ must have length zero contradicting (u1).
We can also restate (u2) by saying that for all f,b then as a function of [α] in β the partial application foldfb commutes with :x and ⋅x, that is:
Existence of a fold function is proved by implementation in the context of the majority of programming languages. In Clojure, fold is the reduce function, but the universal property (u1) and (u2) can actually provide a constructive definition:
Since fold above satisfies (u1) and (u2) by definition, and we can easily prove it forreduce, then they have to be the same function, but we can build some cheap function-equality check on integer vectors
to get a hint our definition is sound, trying out some concrete example
Expressing List Operations in Terms of Fold: Transducers
It is possible to express a lot of functions on lists in terms of fold, amongst the most popular are filter and map:
Vector(5) [1, 3, 5, 7, 9]
Vector(9) [1, 2, 3, 4, 5, 6, 7, 8, 9]
where (filter′π) and (map′ϕ) are actions of natural numbers on lists of natural numbers. Clojure transducers bring this pattern one step further: they incapsulate list-like operations independently of the reducing function. Formally, transducers are transformations of actions i.e. functions
which behaves functorially with respect of folds, this will be explained later.
Functions like filter and map in Clojure, when given a single argument, return a transducer. For instance, loot at
and let's see it applied to theconjfunction at first
Vector(3) [1, 3, 5]
Vector(9) [1, 2, 3, 4, 5, 6, 7, 8, 9]
and later to the + function
The strong point for using transducers in practice is that they offer stack reducing operations in a composable way in which the input list will be visited just once. Take for instance:
At each step above a whole list is returned and fed the next computation which iterates through it again and again. With transducers this won't happen, the following snippet of code reads the input collection just once, encoding the transformations in a single action:
which in clojure is (almost) the same of the simpler form
Later you'll also see the reason for this contravariant behaviour in the order of the function composition which is not the natural right-to-left order.
Fusion Property and the Composition of Folds
Having shown that many functions on lists can be expressed in terms of fold, when can we actually assert that a composition of folds is expressible in a fold of a single action? One step in this direction is given by the fusion property.
Given right α-actionsf:β→α→β and g:β′→α→β′we we call a function ϕ:β→β′ a morphism from f to gif ϕ(f(b,x))=g(ϕ(b),x) holds for every b∈β,x∈α.
We can prove that fold is stable under the application of morphisms, i.e. given a morphismϕ of actions like the one above, then we have:
To prove the above equality we appeal to the universal property: if we can prove (u1) and (u2) of ϕ∘foldfb, then the equality above must hold for every list in[α]. While it's trivial to see (u1), (u2) follows by combining commutative diagrams:
Now, if we want to compose folds as functions of lists we have to restrict to some specific class of actions. We say that an action on lists f:[α]×α→[α]splits if there exists some functionf′:α→α, such that xˉ⋅a=xˉ:f′(a) for all a∈α. Note that the actions defined in the examples above all split (with some formal imagination in the filter case). Given a splitting α-action f and an action g of α on β we define a function of actions tf:Aβ,α→Aβ,αdefined by
We can now state a transducing property for folds of splitting actions in terms of: for every splittingfand g we have:
To prove the transducer lemma it's enough to show that foldgb is a morphism between the actionsfandtf(g):
Let's apply the lemma above to a simple Clojure case wheregis+andfis((mapinc)conj), thenfsplits (by definition) andtf(g)is((mapinc)+):