Whenever I'm hanging around the Snap! folks, I hear a lot about lambda calculus. There's a lambda in the Snap! logo, and the concept seems to be on everyone's mind. But after taking a look at the wikipedia page, I'm struggling to understand what makes it exciting.
Trying to make sense of Lambda Calculus has been like learning geometry without ever seeing the shapes. Sure, it's technically possible to solve a geometry problem using only definitions, but without ever seeing how those definitions manifest themselves in the real world, it's hard to extract any real meaning from the answers.
(For example, let's say there's an object called a guzzle. Every guzzle has two polywhacks which are obstrated. Two polywhacks are obstrated when their sniffles sum to 145. If you have a guzzle with a polywhack of sniffle -56, one could determine that the sniffle of the second polywhack of the guzzle is 201. However, the answer means nothing without context.)
What I currently understand about lambda calculus:
Every function is anonymous (no named functions, which makes recursion very difficult)
Every function takes only one input (functions have to be strung together instead)
Lambda Calculus can be used to simulate any single-taped Turing Machine (I've always lacked a bit of understanding as to what makes Turning Machines interesting either)
So essentially... Why should I care about lambda calculus?
Hi, Josh. There are two different answers to what makes it useful, and a third to what makes it interesting.
Pretty much any programming language can be viewed as procedure calling with a lot of syntax wrapped around it, and understanding how lambdas and procedure calls are evaluated in the abstract helps organize practical interpreters or compilers. See for example this course on programming languages at Berkeley.
Although you wouldn't want to use a really minimal language for actual work, such languages are easy to prove theorems about. (This is also true about Turing machines.) In particular, we can prove that procedure calling is universal -- you don't need any other features to perform any computation that can be done at all; we can prove that there are uncomputable functions; we can gain insights into naming and scope. And so on. You can get @hardmath123 to teach you about how the development of "typed lambda calculus" gave programming language scholars insight into the difficulties of getting typed variables to work adequately in real languages.
It's historically interesting that lambda calculus predates Turing's work -- lambda was the first provably universal computer. As such it's an important moment in math history, the first solution to one of Hilbert's problems. (And it's interesting to think about why Turing's more sequential model became more popular!)
There are named functions; it's just that you have to be clever about the naming, because lambda-binding (associating actual arguments with formal parameters) is the only naming mechanism. Hence the importance of the Y combinator, which makes recursion possible.
The thing about all functions being single-argument is just a simplification to make proofs easier. Practical languages based on lambda (e.g., Snap!) allow multi-arg functions as a little piece of syntactic sugar.
In our community, hardly anyone has actually studied lambda calculus formally. Rather, the lambda in the logo and in a bunch of people's icons is there to emphasize the importance of procedures in our programming style. This includes ordinary named procedures, but naturally extends to anonymous ones, particularly in the context of higher order functions such as MAP. And from there we get to understanding object oriented programming as just another vocabulary for closures -- the result of invoking a procedure and thereby giving values to all its variables.
The best way to understand all this is to read SICP, the best computer science book ever written. It's a dense text, not something you'll finish over a weekend, but it's really what marks the difference between muggles and wizards in CS.
Everything you said is making a lot of sense. I'll try to read the book linked as well. I've never been especially good at handling dense material though. We'll see how it goes.
Crazy late reply, but seriously, do read as much of SICP as you can (and do the exercises!). You almost won't need a university CS degree if you do all of it
Can I necropost if the topic is still on the front page?
I would like to add that there are multiple lambda calculi. When people say "lambda calculus," they usually mean the untyped lambda calculus, the one with ABS, APP, and VAR. Here are some others:
System F features parametric polymorphism (AKA generics).
System F omega adds higher-kinded types (AKA type constructors. functions from types to types). Haskell is based on System F omega, but has a bunch of type system extensions, so I'm not sure how much System F omega it really is.
There are dependently typed lambda calculi, which mix types and terms.
The untyped lambda calculus is Turing-complete, so it has nontermination. For soundness as a logic, that's a problem! Some other lambda calculi are strongly normalizing, meaning that the programs always halt. (https://en.wikipedia.org/wiki/Typed_lambda_calculus)
For an example of the lambda calculus in practice, GHC compiles Haskell to a minimal "Core" intermediate representation based on System F. This design fits with what @bh said about how the LC helps people design compilers and interpreters.
EDIT: Whoops, I necroposted more than I thought; I thought that this topic was made on August 16, 2018, not August 2016...
Sorry about the lack of activity in the last two years. We just got some funding that will allow us to bring the social site to a publishable state and will make this forums visible to everybody, so we can all expect things to move a bit quicker now
We'll see how it goes.
