Lambda the Ultimate

This must be well-know amongst functional programming researchers, but I kind of stumbled upon it by accident when studying Joy.

Consider the following program to count even numbers:

define count_evens = [2 mod 0 neq] filter 0 [inc] reduce

So for those new to Joy, every program/function takes it parameter on the stack, and pushes its results onto the stack.

Here is a brief explanation of the operators:

2 = push the value two onto the stack
[] = push the contents onto the stack without evaluating them
mod = modulo
inc = increment the top item of the stack
neq = not equals

The program I showed takes a list on the stack, filters the list for only even numbers, and then counts them using a reduce function.

Assuming you are following me so far, this program can be rewritten as follows (caveat: I'm doing this off the top of my head so I could have made a mistake in syntax):

  def count_evens_1 = 0 [2 mod 0 eq [inc] [] if] reduce

What I've done here is eliminate the unneccessary filter operation and "folded" it (pun intended) into the reduce operation.

My observation when working with Joy is that this optimization is trivial to automate.

So my question to the group is: is this a well known optimization, and if so, is it as easily applied in other functional languages?

For those whose curiosity has been piqued, I'm researching the viability of using a Joy dialect as an intermediate language.

In a similar vein to John Carter's recent submission, here's an attempt to attack the complexity problem: Out of the tar pit

Abstract: Complexity is the single major difficulty in the successful development of large-scale software systems. Following Brooks we distinguish accidental from essential difficuly but disagree with his premise that most complexity remaining in contemporary systems is essential. We identify common causes of complexity and discuss general approaches which can be taken to eliminate them where they are accidental in nature. To make things more concrete we then give an outline for a potential complexity-minimizing approach based on functional programming and Codd’s relational model of data.

They basically advocate minimising mutable state, moving any mutable state that remains into relations, and specifying the behaviour (i.e. manipulation of relational data) in a declarative/logical/purely-functional language.

Pros: the first half of the paper is a reasonable review of the types and causes of complexity in software.

Cons: lack of any implementation, other than a Scheme prototype of the relational bits, I think (see footnote 25). No source code. Lack of detail about interfacing with external systems.

Here's a link to Ben Moseley's FRP page, where you can find the paper, plus presentation slides and a discussion group.

Proofs are Programs: 19th Century Logic and 21st Century Computing

As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same thing is a story that spans a century, a chase with as many twists and turns as a thriller. At the end of the story is a new principle for designing programming languages that will guide computers into the 21st century.

This paper by Philip Wadler was a Dr Dobbs article in 2000 and has a matching a Netcast interview.

This nifty paper starts with Frege's Begriffschrift in 1879 and goes to Gentzen's sequent calculus, Church's untyped and then typed lambda calculus, and then brings it all together to describe the Curry-Howard correspondence. For the grand finale, Wadler connects this to Theorem Provers and Proof Carrying Code and gives commercial examples where it all pays off.
This is an enjoyable story and a fun introduction to type theory and the Curry-Howard correspondence.

For more of Wadler's writings along these lines check out his History of Logic and Programming Languages paper collection.

edit: fixed the dr dobbs article link