Comment by cousin_it | Hacker News Reader

Comment by cousin_it | Hacker News Reader

Parent Full thread

> back-to-the-basics take on what "is" computing... to build your CS (of whatever brand you like) atop

I feel that we've given many years of attention to functional programming, and it's been disappointingly unfruitful in most areas of CS, such as computational complexity, cryptography, machine learning, or computer graphics. Most new ideas coming out of the FP camp are applicable only to FP itself, like monads. We've discussed that before: https://news.ycombinator.com/item?id=8563817

Part of the mismatch is that many interesting algorithms are impure and cannot be easily made pure. I'd like the "foundation" of CS to give a faithful mathematical description of what computers can and cannot do. Is that too much to ask?

But the bigger problem is that FP treats functions as black boxes, and that's just not enough to prove interesting results in most areas of CS. A better "foundation" would try to describe computational behavior and reason about it, instead of abstracting it away. I admit that's a very vague idea, but I'm not smart enough to make it concrete :-)

> I'd like the "foundation" of CS to give a faithful mathematical description of what computers can and cannot do. Is that too much to ask?

http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis

> A better "foundation" would try to describe computational behavior and reason about it, instead of abstracting it away

A lot of interesting research does exactly this, and a lot of it has found its way into ML-family languages. The starting point (or "foundation") in every case is a typed lambda calculus. Machine models, like turing machines, are just annoying to reason about and not extensible in any meaningful way.

Alas, the Church-Turing thesis doesn't say that every imperative algorithm can be translated to lambda calculus while keeping the same time and space complexity. The two main culprits are in-place mutation and O(1) array indexing.

Sorry for the glib answer. I'm not arguing for programming in the pure, untyped lambda calculus.

My point was that it's possible to systematically extend (or restrict) the lambda calculus and associated techniques. You can add effectful operations and give them semantics (e.g. as functions on stores), define a cost semantics and prove whatever you want while being completely formal.

Try extending RAMs with dynamic allocation, call stacks, or anything to make it more natural to write down a whole algorithm. Try proving something about the composition of RAM programs. I don't think you'll get very far.

Maybe we're talking about slightly different things?

There are many interesting algorithms that are usually analyzed in an imperative setting, like in-place quicksort, Knuth-Morris-Pratt, or Gaussian elimination. There doesn't seem to be any benefit to analyzing them in an FP setting, because it's not easier and doesn't yield new insights.

It seems to me that the FP approach only really shines on algorithms that are "naturally tree-like". For example, I'm a big fan of Okasaki's work on purely functional data structures, and of Blelloch's work-depth model. But let's not oversell FP techniques as the foundation of all algorithm work.

Yes, we're talking about different things. I took the parent comment to mean that talking narrowly about "FP" as programming with pure functions isn't very useful any more. It may have made sense in the 90s when few widely-used languages had h.o.f, but that fight has pretty much been won.

The field that gave rise to FP has a lot to say about how we specify languages and their properties and how we prove things about programs in general. That includes languages with all kinds of effects: state, exceptions, concurrency, etc, and equally as imporant, mechanisms for abstraction and modularity. There's currently no other "foundation" for computation that lets us define these ideas formally.

In discussions of FP, the contributions of the field get reduced to "programming with functions".

It doesn't even say that any imperative algorithm can be translated---merely Turing Machine algorithms which also don't happen to have O(1) array indexing, e.g..

Elsewhere mafribe mentions parallel processing... which is also clearly in another class.

I think pure FP gives a better foundation for mutation, too. It's very straightforward to use something like a pure FP language to make very clear the choice of semantics involving mutable slots.

Reply on news.ycombinator.com