How helpful is knowing lambda calculus? [closed]

To all the people who know lambda calculus: What benefit has it bought you, regarding programming? Would you recommend that people learn it?

Solution 1:

The benefit of lambda calculus is that it's an extremely simple model of computation that is equivalent to a Turing machine. But while a Turing machine is more like assembly language, lambda calculus is more a like a high-level language. And if you learn Church encodings that will help you learn the programming technique called continuation-passing style, which is quite useful for implementing backtracking search and other neat tricks.

The main use of lambda calculus in practice is that it is a great laboratory tool for studying new programming-language ideas. If you have an idea for a new language feature, you can add the new feature to the lambda calculus and you get something that is expressive enough to program while being simple enough to study very thoroughly. This use is really more for language designers and theorists than for programmers.

Lambda calculus is also just very cool in its own right: just like knowing assembly language, it will deepen your understanding of computation. It's especially fun to program a universal turing machine in the lambda calculus. But this is foundational mathematics, not practical programming.

Solution 2:

If you want to program in any functional programming language, it's essential. I mean, how useful is it to know about Turing machines? Well, if you write C, the language paradigm is quite close to Turing machines -- you have an instruction pointer and a current instruction, and the machine takes some action in the current state, and then ambles along to the next instruction.

In a functional language, you simply can't think like that -- that's not the language paradigm. You have to think back to lambda calculus, and how terms are evaluated there. It will be much harder for you to be effective in a functional language if you don't know lambda calculus.

Solution 3:

To be honest, learning lambda calculus before functional programming has made me realize that the two are as unrelated as C is to any imperative programming.

Lambda calculus is a functional programming language, an esoteric one, a Turing tarpit if you like; accidentally it's also the first.

The majority of functional programming languages at all do not require you to 'learn' lambda calculus, whatever that would mean, lambda calculus is insanely minimal, you can 'learn' its axioms in an under an hour. To know the results from it, like the fixedpoint theorem, the Church-Rosser Theorem et cetera is just irrelevant to functional programming.

Also, lambda-abstractions are often held to be 'functions', I disagree with that, they are algorithms, not functions, a minor difference, most 'functional languages' treat their functions more in the way classical mathematics does.

However, to for instance effectively use Haskell you do need to understand certain type systems, that's irrespective of lambda calculus, the System F type system can be applied to all 'functions' and requires no lambda abstractions at all. Commonly in maths we say f : R^2 -> R : f (x) = x^2. We could've said: f (x) = x^2 :: R -> R -> R. In fact, Haskell comes pretty close to this notation.

Lambda calculus is a theoretical formalism, Haskell's functions are really no more 'lambda abstractions' than f : f(x) = x^2 really, what makes lambda abstractions interesting is that it enables us to define what are normally seen as 'constants' as 'functions', no functional language does that because of the huge computational overhead. Haskell and alike is just a restricted form of System F's type system applied to functions as used in everyday classical maths. Functions in Haskell are certainly not the anonymous formally symbolic reduction-applicants as they are in lambda-calculus. Most functional programming languages are not symbolic reduction-based re-writing systems. Lisps are to some degree but that's a paradigm on its own and its 'lambda keyword' really doesn't satisfy calling it lambda calculus.