Lambda the Ultimate

OK, I am going to argue eventually that most of these syntactic conveniences are only convenient for writing bad programs.

Agreed, but I'm arguing that the ability to write bad programs is a requirement for a language that will be used by programmers who are not perfect.

You can write bad programs in the best language in the world, so I think we will not run into many problems there.

I think what you really wanted to claim is that we need to perpetuate programmers' existing bad habits. So what are you saying, then? That we need to choose our battles to win the war?

Another aspect to it is that sometimes, the quick and dirty solution really is the most appropriate. If a language doesn't support the development of such solutions, that will hamper its acceptance. People will often try Q&D first, and get serious later, perhaps when they're forced to. If you don't cater to that, you will be ignored by many people.

Sure, but I don't think the sorts of things I have in mind are such a big hindrance to quick-and-dirty solutions.

That's a real cheap shot, Anton.

I hope you don't mean you took that personally.

No, don't worry.

I agree with you about the reasons that features get accepted or rejected in languages like ML. But what I'm saying is that sometimes, such niceties may be ignored in the commercial world; this might even have a cost, perhaps a significant one. Java, for example, is full of such things, although they can mostly be defended as compromises necessary to achieve security goals.

Despite which, Java remains a very popular language...

I think there are lots of design decisions in conventional languages like C that typical users don't understand, yet never complain about, simply because they can't imagine anything else. They just swallow it, because it's there. I'm sure that when you learned geometry in high school, you never asked yourself, "Yeah, but what if we're talking about a non-Euclidean space, where the angles of a triangle don't sum up to 180 degrees?"

One of my themes in this discussion has been exactly this sort of idea. Programmers are more comfortable with conventional languages than FP languages, not because FP languages are more mathematical or difficult, but because they aren't conventional! If FP was something most programmers learned as beginners, and if most of the open source projects, etc., that they saw while browsing the web were FP, I don't think they would be bothered by design decisions they don't understand.

Of course, most schools don't teach FP to beginners, and most open source code is in an imperative language, but my point is that that is something which can be changed, albeit slowly. In short, the problem with FP is not its intrinsic difficulty, or the "formulas" in ML, but just the lack of popularity. It's a catch-22 sort of issue now, but not beyond hope.

On the other hand, you may be right that the situation is so severe right now, that to make an FP language popular now, you have to make large concessions on popular issues which have no technical motivation.

I'm talking about programmers, but not scientific programmers. I think this may be one of the biggest reasons for the impedance mismatch we seem to have going here. I work a lot in the financial services industry, for example - securities, reinsurance, stuff like that. Many of the people I work with, if they have degrees at all, were arts majors, including subjects like drama, English, history etc.

What kind of programs do these people write? For people with this sort of background, I would change my design goals drastically, as I said, to make the language much more declarative. Frankly, they aren't my target audience at the moment.

Anyway, this sword has two edges. If these sorts of people can pick up imperative programming, which is nothing they were ever taught, then I'm sure they could pick up FP with the proper training resources. Maybe they will never learn to write good FP programs, but I doubt they write good imperative programs now.

I'll use Slash as an example again - do you honestly think the author(s) of the original Perl version of Slash would be able to tell you anything about calculus? (I'd be stunned.)

You mean Slashcode? I think the Slashdot editors are mainly EE majors, so I would be surprised if they didn't know some calculus.

(Totally off-topic, but I can't resist adding that I discovered this week that differentiation is actually useful for programming FP. The idea is that the derivative of a datatype is a `functional' path into a value of that type; it's a small variation on Gerard Huet's Zipper idea. You can read about it in Conor McBride's paper, The Derivative of a Regular Type is its Type of One-Hole Contexts. I find this very cool. I think that the day is not so distant when we will be able to talk about FP programs as geometric objects, which will make it hugely more accessible, and to use the language of topology to describe software engineering. Can you imagine doing Dahn surgery on a program?! :) Actually, my work is headed in this direction also, since the semantics is strongly related to a generalization of higher-dimensional simplices.)

Ah, but I think you have to understand [formulas] better in ML, or something. The algebraic turn of mind, the topiary bush I mentioned. We need some of the cognitive research Ehud talked about to address this, since it seems to be one of our real points of disagreement.

Yeah, or something. :)

OK, let me get a little nostalgic (correction: a lot, considering how much this section has ballooned) and tell you something which may explain my insistence on this issue. It seems that many people (pixel at the very least :) on this board think of me as some kind of pure mathematician with his head stuck way up there in those clouds. But the terrible truth is that when I was in high school, I was terrible in math. English was always my best subject. I never really got math until the second semester of my last year in high school, when I took calculus.

I remember that in seventh grade, my math teacher made me take our school's internal math placement test, which mostly involved arithmetic on fractions, three or four times because I kept failing it. Our school had 3 levels of math curricula---"bonehead", normal and advanced. ("Bonehead" is not my choice of words; people in bonehead math would describe it that way.) Miraculously, I made it into the "normal" class despite my poor performance, but I think I never pulled anything higher than a B in math until that last semester, and mostly it was in the C range.

Calculus somehow worked for me though, eventually. When I look back on it now, I think it must have been the rules for differentiation: they are defined by induction on the structure of formulas. I guess I had never grasped the relation between syntax and semantics until then. I think that differentiation taught me to see both how they are different, and how they relate. And integration was a revelation too, in its own way. My teacher, Mr. Carlson, taught us the rules for it, of course, but I will never forget the most important piece of Zen he imparted to his students: the fastest way to integrate a function is to forget those silly rules and just "pull it out of your ass"! (His words; he was also a football coach. :) He's right, though; there is a lesson about non-constructivity in there somewhere...

Of course I was still good in computer science, which I also took in senior high school, but I never saw any useful relationship between CS and math until long after that, in fact not until after I had graduated college and been working for a year or two (see below).

Still, I had much fewer difficulties in school with pure math after taking that calculus class. In college, differential calculus and linear algebra was a breeze for me, but conversely I had problems with data structure complexity in my CS curriculum. On the other hand, I never could see past the syntax in my physics classes (I was a physics major for three years out of five). I think this is because college-level pure math and complexity theory in CS are so abstract that, if you can think about them at the level of symbol-pushing, you're OK, but in physics you need to be able to see the larger picture.

Anyway, eventually I graduated. When I graduated, I was as pure a corporate hacker as you can imagine: I wanted to be a corporate salaryman; I wanted to `architecture' object-oriented programs in the Gang-of-Four style; and above all, I was convinced that CS is a completely new field unto itself and had no relation at all to all that mathematical crap they were trying to stuff down our throats in school. No, I thought, CS is about sitting down in front of your keyboard, and telling that goddamn processor to listen to you and listen good, because if it doesn't, it's going to get a royal thrashing from this-here assembly hacker!

So I got a job. I tried to apply this stuff. It didn't really work. I was able to do the small stuff---printer drivers, etc.---easily, but I didn't need OO for that. Then they gave me a truly massive project: implement the DSSSL (Document Style & Semantics Specifications Language, IIRC) standard for formatting SGML (XML precursor) documents. Hah! Yeah, I tried the typical OO methodology stuff, but it was hopeless---for me, at least. But the unique thing about DSSSL is that the spec language is based on a pure functional subset of Scheme.

I guess it was in this connection that I once saw a Usenet posting about Haskell. At first I didn't know what it was, because it was just an obscure reference to a name. Eventually I found out that it was a programming language, and I thought, "Hah, just another one of those silly useless research languages." I don't remember exactly what happened after that, but I guess I got interested, and soon I was reading technical papers by Philip Wadler. I saw this lambda-calculus thing, and lots of stuff I didn't understand, but it was obviously quite deep, because he was drawing these far-reaching conclusions about Haskell from it. So I knew I had to find out about it.

What happened next, I remember very clearly. I bought a book, "Lambda Calculus" by Chris Hankin. It's a thin (<200 pages) yellow book, mostly about untyped lambda-calculus. It has a fair amount of equational stuff in it, but I took it on my trip to Korea (to get my Japanese visa---I was working in Tokyo, and you have to leave the country once for some reason to get a working visa) and was amazed that I could understand it. Obviously I thought it was pretty cool. It gave me enough confidence to buy another book, "Semantics of Programming Languages" by Carl Gunther. This one was much more intimidating, but I was careful to read it from the beginning, without skipping proofs and making sure that I understood what he was talking about. Remarkably, it made sense to me.

After that, I was able to read most of the programming language theory literature, and I read TONS, and tons of it. I seriously couldn't get enough, and what I marvelled at was that you could actually make indisputable statements about programs this way, provided your language had a formal semantics. It was no longer a fuzzy thing, you see; it relieved me of a great burden, in a way, because I no longer had to subscribe to a "methodology" which relied on some unsubstantiated relation between real world-"objects" and programs. I came to understand that certain things have to be true, provably, incontrovertibly and forever, if your programs can be translated easily into mathematical terms. This was a huge step for me.

After that I gobbled up Ocaml and Standard ML and Scheme and I dug into category theory; lambda-calculus got me interested in polymorphic lambda-calculus and the Calculus of Constructions and F-omega; monads and combinators and Krivine machines got me interested in algebra and category theory; monads also got me interested in classical linear logic, and that got me interested in classical logic. And then I was unstoppable!

So you see, I am an under-average mathematical student who is now a Ph.D. student in computer science doing original research in computational interpretations of higher-dimensional category theory, with applications to higher-dimensional topology and mathematical foundations.

I'm a poster-child for functional programming. If I can learn FP, anyone can. I'm reasonably smart and I'm over-educated, true, but I'm no over-achiever and I'm no genius. The biggest difference between me and other programmers is not that I'm smarter than them, it's that I'm not as ignorant as them. It's not the nature, it's the nurture.

In business, programming languages alone can't cure the disease, instead, they get used to mitigate the symptoms.

That's what I'm saying, and it doesn't just hold in business: it's not the language (the syntax), it's the semantics.

This gets me into another thing I've been wanting to discuss. But I will leave it for my next message, since I spent so much space (selfishly, I admit) on my biography above. Part duex follows soon. Let's get this message up first...

Practical Theory

Been enjoying the discussion, though I consider myself to fall well within the domain of practical programmers that picked up programming on the side - as opposed to an academic environment. My degree was in Economics, not comp-sci, though I did have to take lots of math for that degree (think econometrics).

On the subject, I have two points. First, most software developers are overworked. I don't know that the solution is for these developers to work harder and learn more. Any real solution would have to be geared towards programmers working smarter, as opposed to longer hours learning an ever increasing amount of knowledge. The quantity of knowledge should be less important than the quality.

Along similar lines, we don't really have good lines to demarcate specialties in software engineering. To be a good software engineer these days requires an immense amount of knowledge and experience. What with new API's coming out everyday for J2EE and .Net, it's impossible to tread water, much less get ahead of the curve.

Anyhow, that's just my two cents worth. I enjoy hearing people that are passionate about their chosen field. Sometimes I get the impression that I know less-and-less about programming. I would say, though, that the one thing I'd like to see is for the theory people to make the concepts more accessible. Having programmed for years, I find that I understand this stuff somewhat, but I usually haven't gotten around to learning the specific terminology. The jargon for those not immersed in the theory can lose one real quick, as the experts tend to assume quite a bit more - which makes perfect sense when speaking to other experts as it is great at reducing the amount of time required to convey the new ideas - as opposed to the ones that have been around since Turing and Church defined the field.

I think one reason for the gap between theory and practice as regards CS is simply that CS is a young field, and things are still being worked out. Theory sometime comes from trying to reason about things invented without a solid theoretical basis (think OO).

The result is that there is no good structure that connects the different pieces into a coherent whole. This is what being a discipline is all about.

It will take a few more years, but we'll get there.

Now think how this effects CS education. Most universities offer a set of courses, that don't really connect to each other (unless they all use C, or some such triviality). There is no gradual buliding of theoretical insights and practical methods.

I think this is also one of the reasons there are so many diffeent approaches to introductory courses: we each have a different mental model of what CS is all about.

That's one of the reasons I was interested in the Beseme project. It tries to teach programming, while building solid foundations.

I'd love to see a college level SE course, that makes use of the theory we have been discussing (coalgebras, category theory etc.) But I am not aware of anyone coming to close to the ideal I have in mind (maybe I should look at The Algebra of Pgramming by Bird et. al? I admit I haven't seen it yet).

Notice, that I am not talking about teaching category theory. I want to teach practical SE - where the students are required to program various sorts of programs and components - while gradually leading to the insights that can (only) be learned from theory. I think this is also a good way to learn the theory itself, but that's a different issue.

I'm a poster-child for functional programming. If I can learn FP, anyone can. I'm reasonably smart and I'm over-educated, true, but I'm no over-achiever and I'm no genius. The biggest difference between me and other programmers is not that I'm smarter than them, it's that I'm not as ignorant as them. It's not the nature, it's the nurture.

Regardless of which of these is true, the fact that teachers don't seem to be very successful in flipping this switch in the majority of the population, is the reason that I'm saying that FP will remain the domain of those who are mathematically inclined, and that this is a relatively small subset of all programmers.

I believe that if you want to change this, you're going to have to figure out how to start flipping those mathematical switches.

There's an aspect of this which is difficult to test: until such time as functional programming is inculcated into children before any other methodology, we won't really know what the effects will be. My hypothesis is that even if that does come to pass, that what is likely to happen is that many children will simply be turned off programming, and then like a mirror image of you (Frank), will one day discover Perl 9 (which by then, will have type inferencing ;) and be as happy as a clam with it.

I may respond further, later on Saturday or Sunday. I appreciated the autobiography; it mirrors my own experience in some respects, although I spent much longer as an "ordinary" programmer before discovering lambda calculus and functional programming. My reaction to these subjects has been very similar - it has changed my programming life - but I haven't yet decided to abandon my secular life to pursue a PhD, nor do I expect to anytime soon...

I think that with the current state of the theory of OO, trying to teach it to newcomers would be a sure way to make FP popular (or at least destroy the popularity of OO).

One of the nice things with the Teach Scheme! approach is their attempt to build graphical tools, and a useful IDE.

Of course, in my experience if this IDE is not a copy of Visual Studio, students are going to complain...

I believe that if you want to change this, you're going to have to figure out how to start flipping those mathematical switches.

With that in mind, I would say that programming code represents a notation for formal logic. Although much more rigorous, mathematical forumalae are another form of notation for formal logic. Bottom line is that there should be a predisposition in the programmer community for formal notation. The question is not whether they are capable of formal reasoning, but what form of notation is best to think and write programs in.

With that in mind, I would say that programming code represents a notation for formal logic.

Bottom line is that there should be a predisposition in the programmer community for formal notation. The question is not whether they are capable of formal reasoning, but what form of notation is best to think and write programs in.

I've come across numerous programmers who operate on exactly this basis: they don't seem to have a strong model in their heads of what the computer will do in a given situation - for them, when they encounter a bug, there's nothing for it but to break out the debugger and trace through line by line until something jumps out at them. The idea that they could model in their heads what might be happening, and identify or at least narrow down the problem without laborious line-by-line debugging, seems to escape them.

I also see here a strong correlation between how people interact with other people in the business world (and elsewhere). When you ask someone in another department to do something for you, and they do the wrong thing, you talk to them to find out where the error in communication was, and debug the problem. Several iterations of this may be required in order to obtain the desired results. If you pay attention to this sort of thing, you'll notice that "bugs" in such communications and the resulting activity are the normal order of things - they happen all the time, and people simply react to them as they see fit, and move onwards towards their goal.

My point is that average people - including average programmers -interact with each other in a similar way to which they interact with a computer. They attempt to communicate their intentions, and often fail to a greater or lesser degree; they then enter a debugging phase in order to get the answer they want. It's also important to note that in both human/human and human/computer interactions, the final answer may not in fact be "correct", if the problem is carefully analyzed; however, if it's correct enough for the initiator, that's all that matters, until such time as the process gets debugged further up the chain. Sometimes, debugging may be deferred until it's too late - the Mars lander lost due to metric/imperial unit conversion would be an example of that. Presumably, at least some NASA programmers are capable of formal reasoning - although I knew one, at JPL in Pasadena, who clearly didn't seem to be - I know, because I inherited a failed attempt at a system from this person.

So far from formal reasoning, I'm saying that most communication processes seem to happen on an ad-hoc, trial and error basis; that humans are used to this, and intuitively comfortable with it; that wrong answers may not be detected early on in a process, and that while not "OK", that's accepted as being a "cost of doing business". Not surprisingly, people commonly bring this modus operandi to their interactions with a computer.

Seen in this context, formal reasoning is simply an optimization technique - someone who's good at it might, in theory, be able to get the job done quicker, other things being equal. Of course, there are problems that can't easily be solved on an ad-hoc basis; I have firsthand knowledge of this, having been called in to advise on systems development efforts which have been foundering for years on end with no useful results - the one involving the NASA programmer was one of them. In some of these cases, the problems being tackled were simply not tractable enough to solve on an ad-hoc basis, and required stronger reasoning ability to solve.

I can't say for sure that all this isn't just lack of proper education and training. My impression, though, has been that computers enable just the opposite of what is being suggested here: they can act as an assist to limited logical reasoning skills, and allow people to achieve things, even if more slowly and with more trial and error than might otherwise be the case.

Many people get into software development now not because they have a passion for it, but because they perceive it as a good career. I'm sure than can think logically to some degree, otherwise they would probably fail at it completely. However, the question is how good their logical reasoning skills are, and how much they depend on the machine to help them get things right.

I can see an argument for saying that if such people were trained in how to use typed FP languages, that this would actually help them in this process. I'm skeptical, though. I'm not sure if I can put my finger on the exact problem, but I'll take a stab at an aspect of it: FP languages can be very concise, saving many lines of code over an equivalent program in an imperative language - and that can be a problem. It's like a connect-the-dots picture - show someone only the dots, even if that is all that's needed to specify the picture, and they may need to connect the dots anyway, in order to be able to deal with it. If you are able to connect the dots in your mind, and reason about the relationship between stated rules, types, recursive functions, etc., then typed FP languages can provide enormous leverage. We like them because of that leverage. I think there are large numbers of programmers in the "real world" that aren't capable of doing that, and they will not like these languages, because their experience with them will be the opposite of leverage.

To be a good software engineer these days requires an immense amount of knowledge and experience. What with new API's coming out everyday for J2EE and .Net, it's impossible to tread water, much less get ahead of the curve.

J2EE and .NET are not inventing new things all the time. Rather, they're simply providing new APIs to do what amount to the same old things. That's not to say there aren't improvements in what's being produced, but the new semantic content is pretty minimal. This is even clearer when you have something more powerful to compare it to, a context in which to fit it. It's a lot easier to learn "new" things when you already understand the underlying concepts. Formal methods provide a way of getting ahead of the curve.

Sounds interesting. On first reading, I agreed with this statement. But can you give a specific example?

if you have formal frameworks with which to evaluate things, I find it becomes much clearer, and easier to see good solutions.

Sounds interesting. On first reading, I agreed with this statement. But can you give a specific example?

One example off the top of my head, related to Java, would be centralizing of exception handling. Most Java texts you read will explain how to write try/catch blocks. Once you've written a few of these, it becomes obvious that they're all pretty similar. The problem is, Java doesn't provide an obvious way of centralizing this repetitive code. If I were doing this in a language with true closures, I might use closures to achieve genericity. Happily, Java's (anonymous) inner classes are closure-like enough to be able to serve the same purpose. In Java, it turns out to be quite easy to write, for example, classes to serve as frameworks for transactions, "map"-style operators for database result sets, or adapters which generically wrap database resultsets in iterators which are specific to an object type. So you end up with code like:

SomeClass result = (SomeClass) new Transaction() {
protected Object body() throws Exception() {
// perform transactional stuff here; if an exception occurs,
// it is handled, logged, etc. from the run() method in the
// Transaction class, which calls this body() method.
return objectOfSomeClass;
}
}.run();

It isn't obvious to most Java programmers that you can or should do this sort of thing with inner classes. There aren't many public examples of it in the official frameworks. Certainly, you should be able to infer that it's possible, from reading the Java language specification; but the possibilities become a lot more obvious if you're already familiar with the use, and consequences, of closures.

Another, related example: because of Java's static typing, and single inheritance, reuse is hampered when you have the same "pattern" which you want to repeat in unrelated classes. It helps to be aware of parametric polymorphism, just so you know that there is a solution, even if it's not directly usable in standard Java at the moment. And again, inner classes can be used in some cases, to mitigate this.

I was familiar with quite a number of languages before I got into functional programming, so it wasn't as though I hadn't heard of any of the above concepts, and it certainly always helps to know more than just the language and tools you're currently working with. But I've found that having a more formally-based understanding - or even an awareness that formal underpinnings exist, and that research is available that can be looked up if necessary - compounds the benefit of this knowledge.

I think the difference between a formal and informal understanding of a topic is the same in most fields - the informal understanding tends to be based on assumptions inferred from limited data sets, and may suffer from various kinds of problems, unrecognized by the person with the informal understanding. Formal understanding gives the benefit of understanding not only that something is a certain way, but why it should be that way, and how you can test your ideas to be sure that they're correct.

You can certainly read about the topics I've mentioned above, e.g. in JavaWorld, and books about patterns; but to internalize them and use them creatively, and create new, useful patterns yourself, I think you need a comfort factor with certain concepts which is difficult to achieve from within (in this example) Java, because its limitations have a tendency to constrain one's thinking.

If you've used these concepts in languages like Scheme, ML, Haskell etc. and have some kind of understanding of their relationship to formalisms such as the typed and untyped lambda calculus, you're much better equipped to see a pattern and immediately recognize it and say: "Aha! I really need a parameterized type here, what is the best way to achieve that in this case?", while other people are floundering aimlessly, not having really recognized anything fundamental about the nature of the problem they are grappling with.

P.S. The above are micro examples, which are easier to describe concretely without getting into a lot of background; but I think the situation at the macro level is similar. Designing abstractions well requires a good understanding of multiple approaches to problem solving - to avoid having "everything look like a nail". Anyway, if I have to pick a hammer, I'd rather it be one that can be proved mathematically correct, than one which was designed as the latest salvo in a marketing war...

For other purposes (where returing a function is needed) I use objects to simulate closures.

I would argue that this knowledge alone would be enough to make a big difference in one's abilities as a software developer.

Yeah, I do that too. I use generic programming facilities in Ada (which allow passing routines as generic parameters) to be able to introduce students to high order functions (fold etc.) For other purposes (where returing a function is needed) I use objects to simulate closures.

That sounds familiar. That's exactly what I do in C++. And not only me, the whole STL algorithm facility is based on this technique. Not surprisingly, the lack of closures is one of the things I miss most when working in C++. The extra typing is horrendous. And the code is significantly less clear. If that is not motivation to use FP, than I don't know what is.

Maybe the solution then is to add FP constructs and facilities to standard computer languages. I mean, this has been very successful for OOP. Actually, to and extent I think this is already happening.

A nice touch (?) in C++ is that you can overload the () operator. That makes function objects more sexy...

Maybe the solution then is to add FP constructs and facilities to standard computer languages. I mean, this has been very successful for OOP. Actually, to and extent I think this is already happening.

At the same time, I expect the language cores will get increasingly functional - compilers, and runtime environments like the JVM and .NET. That's also already happening - for example, an "advanced" technique for optimizing compilers, Static Single Assignment (SSA), basically involves converting an imperative program into a functional form, in which no variable is assigned more than once, which then allows much easier analysis and subsequent translation.

Yeah, BeyondJS

I was actually thinking about Ruby (closures, unnamed functions), new Python features (iterators, generators), C++ STL algorithms I had previously mentioned, and yeah also BeyondJS ;)

A nice touch (?) in C++ is that you can overload the () operator. That makes function objects more sexy...

Overloading the function call operator is more than just syntactic suger. Indeed, STL algorithms depend on this feature. Using generics, it allows the use of both regular functions and function objects as arguments.

If it was decided to replace () with a regular function called Eval, wouldn't it be possible to achieve the same functionality (with a bit more effort, of course)?

But then the same higher order functions could not be used for regular functions, only for function objects. Consider the implementation of the for_each algorithm (taken from the STL version that comes with VC++):

The _Op argument (don't you just love the name) can be either a function, as in:

or a function object:

This would not have been possible without overloading the function call operator. So STL makes what was purely syntactic sugar before truly useful. Also, while the PrintFactoredNumber is obviously contrived it does reflect much of the type of code I write using for_each. It thus demonstrates why I miss closures so much when I program in C++.

I've been known to say that syntactic sugar can be real sweet...

Frank modestly claimed:

I'm a poster-child for functional programming. [..]

There are two possibilities here: either you are kidding yourself completely, [..] or, there is some missing mathematical switch present in everyone which somehow, teachers have just been failing to flip to the "on" position.

I exaggerated the situation in my fervor to reach a climactic crescendo. My point is that I was a salaryman and an OO hacker-wannabe who became an "academic" and an FP convert, so if it can happen to me, then it can happen to many others who think they are "safe". :)

As for the mathematical switch: you may be on to something. For me, once I realized that high school mathematics is 90% algorithmic, I was in the clear. There is something more to this. I use mathematics to shed light on programming, but this can go the other way too: we can use programming to teach (constructive) mathematics. And it's not impractical. One of my favorite references is a book which takes this tack, namely Paul Taylor's "Practical Foundations". (See the HTML version at my site.)

I appreciated the autobiography; it mirrors my own experience in some respects,

Indeed, I suspected as much, which is part of what motivated me to post it.

With that in mind, I would say that programming code represents a notation for formal logic.

That's more or less what the Curry-Howard isomorphism says... ;) Programs are proofs, and types are formulae. (Couldn't find a concise web reference for it though.)

Ehud posted the one by Sørenson and Urzyczyn recently, but there is a shorter more accessible introduction by Philip Wadler, which was printed, of all places, in Dr. Dobb's Journal!

Finally, two more loose ends I want to tie up.

First, I had an exchange with pixel here which continued in email. Ehud made a post recently about code examples, and my reply to pixel in email contained some code which may clarify some bits about folds, algebras and traversals. If pixel gives me permission, I will post it here. Do I have permission, pixel?

Second, I think (it was) Bryn (who) asked me to clarify a remark I made about metalanguages and reflection. I haven't had the opportunity to do this, as I am working on a talk I have to give in a week, but my talk is related indirectly to the topic so, instead, how about I just promise to put the slides up on my web site and invite you all to read them? The topic is intensional type semantics.

The human mind is a funny thing. I know this paper, it was linked from LtU, I remembered the title and author, but I completely forgot what it is about...

(Note to readers: Manila does some funny business on the following preformatted text, like dropping backslashes and turning some dashes into <hr>'s.)

> Just a small note about foldl/foldr.
> My definition of foldl/foldr is simply what it *does*. 


Mine too! That's the beauty of constructive mathematics: properties define
an algorithm.

> I mainly learn by example.


Most people do, including me.


> foldl f z []      = z
> foldl f z (x:xs)  = foldl f (f z x) xs
> foldr f z []      = z
> foldr f z (x:xs)  = f x (foldr f z xs)


> this can defined as far as you can iterate on a data structure, aka:
>
> -------------------------------------


> class Data_structure ce e | ce -> e where
>     to_list :: ce -> [e]
>
> data Tree a = Leaf a | Node(Tree a, Tree a) deriving Show
>
> instance Data_structure (Tree a) a where
>     to_list (Leaf a) = [a]
>     to_list (Node(left, right)) = to_list left ++ to_list right
>
> ffoldl f e ce = foldl f e (to_list ce)
> ffoldr f e ce = foldr f e (to_list ce)
> -------------------------------------


> so for me, foldl vs foldr is really a left-to-right vs right-to-left pb, for a
> given iterator.


If you want to define foldl and foldr that way, that's fine with me.

What I am saying is that there is a generic function, called a fold, which can
be defined for every datatype, and that for the case of "List a", that
function is the one you call "foldr".


However, for "Tree a" it is not your ffoldr above, but rather:


foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b
foldTree leaf node (Leaf a) = leaf a
foldTree leaf node (Node(t,t')) = node (foldTree leaf node t)
                                       (foldTree leaf node t')


I think if you examine this carefully, you will see how to define an analogous
function for every datatype.


Notice that your ffoldr cannot distinguish between the trees:


  Node(Node(Leaf a0, Leaf a1), Leaf a2)


and


  Node(Leaf a0, Node(Leaf a1, Leaf a2))


since they both get transformed to the same list:


  [a0, a1, a2]


by to_list. In other words, to_list throws away some information in trees, and
identifies the ones which might be regarded as different if it had kept that
information.


In fact, you can define to_list in terms of foldTree:


  to_list = foldTree (a -> [a]) (++)


and indeed you can define both ffoldr and ffoldl in terms of foldTree, without
even using lists:


  ffoldr f e t = f (foldTree f (.) t) e
  --- same as: = f (foldTree (a -> f a) (g g' -> g . g') t) e


I will let you figure out how to do it for ffoldl yourself.


On the other hand, you cannot define foldTree using ffoldl and ffoldr because
they have both already destroyed some information about their inputs because
of the problem I mentioned with to_list.


Therefore, foldTree is strictly more general than ffoldl and ffoldr.


If you want to learn more about this, you might read this paper:


  Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional Programming
    with Bananas, Lenses, Envelopes, and Barbed Wire. In Proc. FPCA'91, volume
    523 of LNCS. Springer-Verlag.


  http://research.microsoft.com/~emeijer/Papers/fpca91.pdf


It's difficult, but doesn't use anything a Haskell programmer wouldn't
know. And it explains what algebras, homomorphisms, catamorphisms and things
are.


Hope this clears things up a bit! There's nothing too magical here.

Shouldn't the real question be, why can't you have a generic function, called a dlof, which can be defined for every datatype, and that for the case of "List a", that function is the one you call "foldl"?

Seems to me this is the question that started this debate.

(Thanks for sharing..)

Shouldn't the real question be, why can't you have a generic function, called a dlof, which can be defined for every datatype, and that for the case of "List a", that function is the one you call "foldl"?

In one sense, there is such a function "dlof", but it is just the same as "fold", i.e., they become identified. This is because the types we use to build an algebraic datatype in conventional functional programming languages are sums-of-products, and both sum and product are commutative (up to isomorphism). You can imagine using a different basis of types, though, which are not commutative, and then you would get one or more analogues to fold.

That doesn't really answer the question, though, since foldl and foldr are definable and "different" for lists. But, really, they are not different if you consider that, for every input to foldr (respectively foldl), I can give you an input to foldl (resp. foldr) which produces the same output. In that sense, they are isomorphic functions, and there is no reason to prefer one over the other.

Of course, I can produce functions isomorphic to the "obvious" fold for other datatypes too. For example, I can permute their arguments, etc., but there is no canonical pair of folds for them, because they generally have many more symmetries (arising from the fact that their types include more products and sums); so there are more than just two choices for fold. I think that the "obvious" fold is just the one that we humans think of first, since we like to avoid inserting unnecessary isomorphisms, but because humans are conditioned to noticing the duality in linear structures, in the case of lists both foldl and foldr seem "obvious" to us.

So, in conclusion, I guess I was wrong to say that foldl is not the fold for lists. Still, foldr is the more obvious way to write fold in FP languages...

Shouldn't the real question be, why can't you have a generic function, called a dlof, which can be defined for every datatype, and that for the case of "List a", that function is the one you call "foldl"?

A paper by Tim Sheard and Leonidas Fegaras, "A fold for all seasons," (see below for a reference) shows how to define such as generic fold that applies to _any_ "algebraic type definable in languages such as Miranda and ML, i.e., mutually-recursive sums-of-products with tuples and function types". In case if such datatype a list, this generic fold is just foldr.

BTW, for trees such as

data Tree a = Leaf a | Nd [Tree a]

the generic fold becomes the following tree fold foldt:

foldt:: (a -> b) -> ([b] -> b) -> Tree a -> b
foldt f g (Leaf x) = f x
foldt f g (Nd kids) = g (map (foldt f g) kids)

Coming back to foldt: unfortunately, it's often not good enough to express many useful traversals (and even when it is expressive, it may not be efficient). Note that 'map (foldt f g) kids' in the definition of foldt implies that all the branches of a node are traversed independently (in parallel, so to speak). But what if we want to operate on nodes in a way that depends on the history of a traversal? For example, we want to compute an MD5 digest of nodes in the tree. The digest has to be accumulated serially; the md5accumulator is not associative. Well, foldt can still be of use (when it is treated as a second-order or a continuation-passing fold). However, in that case the run-time efficiency usually really suffers.

This problem and its possible solutions have already been discussed at LtU:
http://lambda-the-ultimate.org/classic/messagx1595

[there is a] generic fold that applies to _any_ "algebraic type

Indeed, this is what I have been saying. Your function foldt is the fold for finitely branching finite trees. (And, just to be clear, this fact was known long before the Sheard and Fegaras paper, though Sheard is certainly one of the people most responsible for popularizing it in FP circles.)

But what Ehud was asking, or at least what I understood him to be asking, is "if foldr is the fold for lists, why isn't there a function analagous to foldl for other algebraic datatypes". And my answer was that foldl and foldr are isomorphic, so they are really in a sense the same function.

But what if we want to operate on nodes in a way that depends on the history of a traversal? [...] Well, foldt can still be of use (when it is treated as a second-order or a continuation-passing fold). However, in that case the run-time efficiency usually really suffers.

Also, you can use monadic folds, though they amount to about the same thing as CPS. See:

E. Meijer and J. Jeuring. Merging monads and folds for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming , LNCS 925, pages 228--266, Springer-Verlag, 1995.

Honestly, I am not satisfied with monadic folds, though. The paper mentions it:

A disadvantage of monadic folds is that they are in some sense too specific and hence not all functions of type [a] -> m b [in the case of lists] can be written as a monadic fold.

I wasn't really asking this, since I know the answer, but this is indeed what I meant. I was trying to help clarify the real issue here, and it worked: I think that Frank's dlof message pretty much explains the "mystery".