Lambda the Ultimate - Comments

There might be a certain

Kay Schluehr — Sat, 11 Feb 2012 03:39:05 -0500

There is a certain composting of logic languages. I encountered "logic engines" two times in my career. In one case it was about filling action tables within an Excel sheet that was compiled via VB into a "fact base" of some test tool. Those facts were then used by the tool to verify response data of a system-under-test. Half of the team used it, the other half tried to work around it. The other time it was a simple "reasoning engine" which was fed with facts written in an "in-house" XML language designed by some guy who left the company. It was very semantic web or so - I don't remember exactly the rhetoric packaging used to sell it to the engineers. There was one fan in the team who kept it alive. In neither case it was used for anything sophisticated like solving NP complete problems declaratively, but even the little it could do, was done badly or cumbersome. So the experience curve goes like this: very sophisticated rule based engines usable by only a minority of trained expert programmers are replaced by dumbed down versions of such engines which are meant to be used by average programmers for occasional use which gets replaced by nothing like that at all. The final backtracking step was to dump the backtracking engines into the dustbins and track back to a mixture of procedural / OOP approaches. This could be seen as an entirely negative result but there was at least a desire for declarative programming methodologies and moving from step 1 to step 2 and becoming "mainstream" if only within an organization, something which is quite a lot.

The last lecture to my first

Philip Wadler — Fri, 10 Feb 2012 17:36:38 -0500

The last lecture to my first year students (Informatics 1 Functional Programming---taught in Haskell) covers Boole, Frege, Church, Gentzen, and Curry-Howard. Slides are here.

Nice example!By

sigfpe — Fri, 10 Feb 2012 12:55:49 -0500

Nice example! By coincidence, John Baez just posted an article in which he discusses why you don't want to eliminate dimensions even though you can. Much the same argument applies to types.

Sure, but...

Matt Hellige — Fri, 10 Feb 2012 12:22:44 -0500

Sure, but while map is usually pretty intuitive, 'flatten' is often non-obvious. But I do see your point. I guess I don't know whether it's easier to understand or not. In the case of the IO monad, at least, I think bind is a lot more intuitive than join. I guess I feel it's easier to see how bind generalizes beyond "collections", while "join" (and thus "flatMap") has a very collection-centric intuition. But, point taken... maybe it's just me.

The for comprehension acts

AlecZorab — Fri, 10 Feb 2012 12:21:53 -0500

The for comprehension acts as sugar for a chain of flatMap, filter and map calls, so no, there isn't.

Actually you can define map

Jules Jacobs — Fri, 10 Feb 2012 11:30:10 -0500

Actually you can define map and flatten for any monad. Whether that is more easy to understand than bind I leave to the psychologists.

Strange advocacy

renox — Fri, 10 Feb 2012 10:55:33 -0500

Strange advocacy: each example with "flatMap" was immediately followed by the same example with "for" instead, and IMHO the example with "for" was more readable. Is-there some use of "flatMap" where "for" cannot be used?

Except it's not true

Matt Hellige — Fri, 10 Feb 2012 09:33:51 -0500

"Map, then flatten" is not a good description of the bind operation for all monads (although I agree it's a nice intuitive place to start). So if you rename bind to flatMap, you may end up with a bunch of things called flatMap that seem to have extremely obscure semantics.

flatMap

AlecZorab — Fri, 10 Feb 2012 07:02:12 -0500

I've found that explaining it to people as mapping and then flattening the nested structure is enormously easier to understand what's actually happening. I think that to someone seeing them for the first time, "bind" is about as useful as "monad" in explaining the structure of the computation.

Too heavyweight

Charles Stewart — Fri, 10 Feb 2012 05:00:53 -0500

This is meant to be an intro lecture in a course to students who have met the simply-typed and polymorphic lambda calculus, but not yet dependent types. As a general point, this is the right way around. Dependent type theory features complex inference rules that are much easier to grasp if you understand the formulae-as-types correspondence. Adam Chlipala's book was mentioned in the answers to a relevant Cstheory question, What is the most intuitive dependent type theory I could learn?

FWIW

Paul Snively — Thu, 09 Feb 2012 17:50:31 -0500

Adam was hugely patient with me when I sat next to him at the POPL '08 Coq tutorial. I'm currently working through his CPDT, and am enjoying it tremendously.

Chorded Keyboard

dmbarbour — Thu, 09 Feb 2012 15:33:01 -0500

Douglas Engelbart's chorded keyboard via multi-touch might be an interesting possibility for the cases where developers need text.

Adam Chlipala

dmbarbour — Thu, 09 Feb 2012 14:53:43 -0500

Adam Chlipala is teaching courses and writing a textbook in this vein. Follow the links, maybe approach the man for advice.

No Worries

Paul Snively — Thu, 09 Feb 2012 13:04:32 -0500

It was actually a helpful reminder that those of us who have read TAPL, use Coq, and follow mechanized metatheory developments religiously are an even rarer breed than I had realized. :-)

Done

Paul Snively — Thu, 09 Feb 2012 13:03:28 -0500

Thanks!