Lambda the Ultimate

Hi Darin,

Thanks for you response.

I have never seen "reduce" called "filter". Can you please point me somewhere on the web where the terms "reduce" and "filter" are used to mean one another?

I realize that foldl and foldr are specifically order dependant by their very definition in Haskell. My issue is that as a programmer, I would rather define a function such as "sum" without specifying whether to use foldl or foldr since they both will end up with the same result. The idea being that if I don't specify the order, then the compiler can theoretically optimize and parallelize the code more easily.

Maybe I am barking up the wrong tree here.
:-)

They don't necessarily give the same result in Haskell - foldl never terminates given an infinite list for input, whereas foldr can. Consider folding (&&) over an infinite list with a False in it, for example, or using the fold to build a data structure not all of which is evaluated.

Good point, thanks for bringing it up.

I think of filters as stateful processors of streams, e.g. low pass filters, etc. Thus I think a better name for "filter" is "sieve" since it eliminates things from the stream (Smalltalk calls it "select"). When writing stream processors that can also be signal processors, using the name "filter" is confusing to people who are more familiar with signal processing than functional programming.

When I've used an unspecified fold, I've called it "fold", i.e., neither l nor r. But using this function carries a proof obligation, since the implementation can assume that the operator is associative, and that cannot be machine checked (in general).

BTW, the "sum" function is the same with foldl and foldr if you add up Int, but certainly not Double. (For Double you should really use http://en.wikipedia.org/wiki/Kahan_Summation_Algorithm)

How about operations are typed so the fold knows what kind of associativity they respect? Then fold does the right thing based on that? Sorta like Monads, they aren't proven by the compiler, whoever makes one has to make sure to not blow up the contract.

You could have a type of associative operators, and ways to combine them that maintains associativity. And then some way to inject functions into this type where you have a proof obligation. It could be helpful.

But the comparison with the Monad class isn't quite right. As far as I know, no Haskell compiler uses the (unproven) monad laws for any transformation. So if you lie to the compiler about something being a monad then nothing bad happens (which is lucky since many types in the monad class aren't. :) )

Close, but not quite. It's rather perverse that these two forms of the same word have rather different technical meanings. You seem to be getting these meanings confused.

First, if you talk about the "associativity of subtraction," most mathematicans would take that to mean "subtraction is associative," which means that for all x, y, and z:

x - (y - z) == (x - y) - z

You seem to understand that this is not the case. In fact, it's easy to use elementary algebra to prove that this equality is true if and only if z = 0. (Although this isn't the case in group theory.) Therefore, there is no "associativity of subtraction," at least when you are talking to a mathematician.

On the other hand, there are the conventions that define standard order of operations. Sombody will say that "subtraction associates to the left" to mean that when we write

x - y - z

we actually mean

(x - y) - z

This is purely convention, no more and no less. "associates" has nothing to do with fold-left vs fold-right.

On the other hand, "associativity" is quite relevant to fold-left and fold-right. Namely, when passed an associative operator, fold-left computes the same value as fold-right when at least one of these additional conditions are true:

1. the initial element is the identity element for that operation
2. the operation is also commutative.

If the operation is not associative, it all depends. Fold-left probably does not compute the same thing as a fold-right.

I've generally found it easiest to explain by calling associative operations "fully" associative instead of "left" or "right" associative. People seem to get that pretty easily.

(Although this isn't the case in group theory.)

Depends on the point of view really:

(a) If one considers '-' as a binary operation [over a set of integers], then the the structure is not a group but rather a quasigroup without identity (similarly, nonzero rationals under division).

(b) If one considers '-' as a notation for the inverse element, then we have a group [of integers] under addition where the '+' operation is implied:

a-b-c a + (-b) + (-c)

So does this mean it is a good area for research? One solution, might be to allow programmers to provide attributes for functions with regards to their properties (i.e. associative, commutative, etc).

I'm sure it's worth researching for your own benefit, and you just might come up with something. :) I really don't know what has or has not been done with your question, but I can offer generic advice.

It's pretty well known that you can use associativity and commutativity properties to optimize folds, especially really large folds across multiple machines. As you suggest, you could declare something to be associative and commutative, though I certainly would not trust a hurried programmer to create these declarations.

Tim's right. Associativity and commutivity are undecidable properties in general. Unchecked declarations might be the way to go if you are looking to get something done, but this probably isn't a viable line of research.

There are interactive theorem provers that help humans generate a machine-checkable proof of associativity and commutativity. This a possible application of proof-carrying-code, as a means of safe optimization instead of a means of security. (Though the two are interrelated.)

Another tactic for dealing with undecidablity is to restrict your language. Can you find a restricted language that produces only associative and commutative operations, and is still sufficient to efficiently express most or all operations of interest? Can you restrict your language so that a fully automated theorem prover can decide whether or not something is associative and commutative?

Regular expressions, SQL, HTML, CSS, PDF, are examples of languages that sacrificed turing-completeness in order to gain something else. (Such languages also have the tendancy to creep back to turing-completeness.)

Finally, you may decide that you don't really need associativity and commutivity, that your conceptual domain and range are actually a quotient type. Then you should prove that functions you define are in fact well-defined.

A language which supports declaring associativity and commutativity of a operators in a non-trivial way is OBJ3 and presumably other members of the OBJ family. It is covered in section 2.4.1 of Introduction to OBJ3 (the correct link to the PDF there is also a link to a PS on the page). In general, the OBJ family is interesting.

Leon's remark at the end makes me again bring up Constructing Polymorphic Programs with Quotient Types. A function accepting an unordered pair would be a commutative function.

(Thread necromancy.)

The typical PLT approach would be to define an algebra of symmetric functions, enabling you to build up any symmetric function from a set of primitive symmetric functions. Then the primitive symmetric functions could be certified to be symmetric by the compiler and off you go.

It turns out there's a much simpler approach that works in many cases.

Suppose we are dealing with numerically-valued functions; or more generally, functions taking values in an integral domain. Let f be such a function. We say that f is symmetric when f(x,y) = f(y,x). Note that this is equivalent to 1/2(f(x,y) + f(y,x)) = f(x). For any function f, symmetric or not, 1/2(f(x,y) + f(y,x)) is called the symmetrization of f since it is always symmetric in x and y. But only in the case where f is symmetric does f equal its symmetrization.

Underlying the symmetization construction is the symmetrize combinator, which we could define in Haskell as

symmetrize f x y = ((f x y) + (f y x))/2

Suppose that this symmetrize combinator was provided by a language's standard library and certified to only produce symmetric functions. (Not unlike how the memoization function in the Standard Prelude is assumed to be side-effect free from the outside.) Then there could be a neutral fold only taking folders produced by symmetrize. The programmer's burden shifts to proving that f = symmetrize f externally to the type system.

You can play similar tricks for associative functions using so-called associators.

So if I understand you, aggregate atomic operations, are mostly ignored in many functional languages? In the Google map/reduce framework do they parallelize the reduce function I wonder?

So if I understand you, aggregate atomic operations, are mostly ignored in many functional languages?

I'm not sure I understand this question. Anyway, I think the deal here is that most functional languages use lists as their most common data structure. Fold right is a very natural operation over a list, since it essentially performs a recursive computation that's isomorphic to the list it's given (the good old "replace cons and nil with your choice of function and value" description of fold right).

Aggregation, on the other hand, is an operation over sets or multisets (a.k.a. "bags"), a data structure that functional languages have not tended to emphasize as much as lists. Relational query languages, on the other hand, have the relation, a set of tuples, as their fundamental data type.

So I think one approach to what you're interested in would be to for the language to provide abstract set and multiset datatypes, and higher-order aggregation combinators over these. The contract here is that if you're using the set or multiset datatypes, while there may be a way to construct a set recursively, when you deconstruct the same set, you can't necessarily recover the order in which you constructed it (which is what makes sets and lists different). Then, your underlying concrete data structures, and your implementation of the aggregation combinators, can be such that the operation parallelizes.

So I think one approach to what you're interested in would be to for the language to provide abstract set and multiset datatypes, and higher-order aggregation combinators over these.

If I recall correctly, Kleisli took this approach, including primitive structural recursion operators for lists, sets and bags. These primitives were also exposed via comprehension syntax for each type of collection.

I think Kleisli deserves a bit more attention for its efforts to bridge databases and programming languagues.

In the Google map/reduce framework do they parallelize the reduce function I wonder?

googles map/reduce requires the user to supply a custom partitioning function. the partitioning controls the distribution of the data before the reduce step. it has to be intelligent enough to guarantee that the distribution before reduce does not break associativity.

besides that, reduce operations that are both commutative and associative are optimized through an additional interface called combiner.

i guess that such decisions are deliberately burdened onto the user because a generic solution (that might be transparently implemented ontop of fold[lr]) cannot automatically decide distributability.

That is indeed useful. I want to write an introductory programming text at some point, and I find this a useful way to think about fold/reduce.

That is indeed useful. I want to write an introductory programming text at some point, and I find this a useful way to think about fold/reduce.

Isn't this how everyone explains foldr? That is, you think of foldr f a applied to a cons list as replacing the conses by f and the nil by a. This then motivates how to define a foldr equivalent for other algebraic data types.

The J-style way of thinking about the 'over' adverb is only correct when the verb you're using is associative. But I don't think the usual functional programming explanation of foldr (as described above) is any less intuitive than James's explanation.

...performs n-1 binary operations on an array of size n while fold performs n binary operations on a list of size n. Of course they turn out to be equal for some choices of binary operation.

In reality, both work from the left, as dictated by the structure of lists, ...

For that matter, some of the inherent assymmetry is already in the structure of the lists. There is an intuitive, pre-theoretic understanding of a list as neither left- nor right-recursive, but more symmetrically just an (ordered) collection. Think of an array rather than a cons- or snoc-list. Or better, picture a list as a row of cells, rather than as a left-recursive "tree" built from cons cells.

I came from an APL background and had that intuition about arrays when I first started using ML and Miranda; the need to commit to a left- or right-recursive understanding of lists was a difficult part of the transition for me. Of course, now it's hard to get back to that other way of thinking; now I find it hard to even think of the structures without thinking of the traversals as an inherent part of them.

The problem with a non-specific fold is that, for it to be well-defined, it must be over an operation + that is associative; and for that to be well-typed, it must be an endomorphism: (a + b) + c = a + (b + c) requires that the type of the outer +'s match, which demands that the types of both operands be the same, hence + : S x S → S. You cannot lift Cons to an endomorphism, since both its arguments are different: Cons : α x List(α) → List(α).

However, you can morph the structure of nonempty lists built from the singleton constructor and list concatenation:

• [_] : α → List(α)
• ++ : List(α) x List(α) → List(α)

Now define fold as

fun fold (+) [x] => x
    fold (+) (m ++ n) => (fold (+) m) + (fold (+) n)

Then fold (+) is a semigroup endomorphism whenever (A, +) is a semigroup. It is clear that the source of the "non-specificity" in the fold is the indeterminate choice of where exactly deconstruct a list l into a catenation m ++ n.

Thanks to everyone who has responded, it is much appreciated. These are very illuminating posts.

No, it's not just taking arguments in a different order.

foldl c n = foldr (flip c) n . reverse

foldr isn't quite definable in terms of foldl (in a lazy language).