CS seems overburdened with jargon and trendy crap (IMO) so is this just the latest thing coming down the pike that everyone needs to give lip service to in order to seem smart to their peers?
CS seems overburdened with jargon and trendy crap (IMO) so is this just the latest thing coming down the pike that everyone needs to give lip service to in order to seem smart to their peers?
Lambda calculus was created by Alonzo Church in the 1930s. Alongside the work of Alan Turing, it forms a large part of the mathematical basis for modern computer science[0][1], and the implementation of many, if not most, modern programming languages.
> 80 year old concept that has spanned dozens of programming languages.
I don't even disagree with you, the "throwback to the roots" thing is not very useful most of the time, except for intellectual curiosity.
lambda calculus is still extremely useful for Prog lang theory, though, because that's the simplest thing you can imagine. If you want to prototype your fancy new type system or weird new execution model, you always design it on the lambda calculus first.
I did some follow-up work after that paper to implement binary arithmetic in the lambda calculus, and using that, of course, you can compute "real" factorials. Here it is computing the factorial of 100 in under a second:
? (time (pbn (bn_fact (bn 100))))
(PBN (BN_FACT (BN 100)))
took 942,269 microseconds (0.942269 seconds) to run.
64,791 microseconds (0.064791 seconds, 6.88%) of which was spent in GC.
During that period, and with 4 available CPU cores,
878,343 microseconds (0.878343 seconds) were spent in user mode
111,475 microseconds (0.111475 seconds) were spent in system mode
759,285,088 bytes of memory allocated.
504 minor page faults, 0 major page faults, 0 swaps.
93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000
This is he expanded code: ((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ n
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n)
(λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t))))
(λ dummy
(((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ (n1 n2 r)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n1) (λ dummy r)
(λ dummy
(f
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ s (λ (_t e) _t))) (λ dummy ((λ p (p (λ (l r) r))) l)))
(λ x x))))
n1)
((λ (l r s) (s l r)) (λ (_t e) e) n2)
(((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n1)
(((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ (n1 n2 c)
(λ nil
(((λ (c _t e) (c _t e))
((λ (p q) (p q (λ (_t e) e))) ((λ p (p (λ (l r) (λ (_t e) e)))) n1)
((λ p (p (λ (l r) (λ (_t e) e)))) n2))
(λ dummy
(c ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t)))
(λ s (λ (_t e) _t))))
(λ dummy
((λ (l r s) (s l r))
((λ (b1 b2 c)
(b1 (b2 c ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c))
(b2 ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c) c)))
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n1)
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n2)
c)
(f
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ s (λ (_t e) _t)))
(λ dummy ((λ p (p (λ (l r) r))) l)))
(λ x x))))
n1)
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ s (λ (_t e) _t)))
(λ dummy ((λ p (p (λ (l r) r))) l)))
(λ x x))))
n2)
((λ (b1 b2 c) (b1 (b2 (λ (_t e) _t) c) (b2 c (λ (_t e) e))))
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e))
(λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n1)
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e))
(λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n2)
c)))))
(λ x x))))))
n2 r (λ (_t e) e))
r))))
(λ x x))))))
n
(f
(((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ n
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n) (λ dummy n)
(λ dummy
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) l))) n)
(λ dummy
(((λ p (p (λ (l r) (λ (_t e) e)))) ((λ p (p (λ (l r) r))) n))
(λ s (λ (_t e) _t))
((λ (l r s) (s l r)) (λ (_t e) e) ((λ p (p (λ (l r) r))) n))))
(λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (f ((λ p (p (λ (l r) r))) n)))))
(λ x x)))))
(λ x x))))))
n))
(λ s (λ (_t e) _t)))))
(λ x x))))))"
I didn't write that all by hand, of course. I built it up in pieces and my "compiler" assembled it for me. But start to finish that took be about an hour.Are you telling me that the most efficient means of generating factorials is via LC? That no other method can touch it in terms of real time?
My goal was to dispel the myth that the lamdba calculus is nothing more than an intellectual curiosity. It is much, much more than that, not because you can use it to compute factorials, but because the techniques that you use to compute factorials in LC are generally applicable. If you really want to master the craft there are a few things you really need to know how to do: write your own compiler, your own editor, your own implementation of the Hindley-Milner type system. Writing an efficient factorial in LC is like that. It's not useful in and of itself, but for what you learn simply by going through the process.
I'm sorry to say that your factorial example just seems painful and pointless to me, and doesn't encourage me to expand my mind via LC at all.
It is, because it is a standard model for computation. To put it in layman terms, every programming language is lambda calculus in disguise. You have absolutely no idea of computability theory. That is the theory in which the P=NP conjecture is formulated, which has massive implications e.g. on cryptography.
You seem frustrated for not understanding at all what's going on here and you try to provoke answers. I know what I'm talking about, because I don't grok LC either and I get furious quickly when I'm hungry, tired or overworked. You are paranoid.
So as recently as now, it might be argued that the Lambda Calculus has helped waste time reading this here comment. Whether that's something it's done for anyone or undone is a matter of perspective.
- Knowledge that is implicitly contained in larger objects or concepts, but there is no need for users of those larger objects/concepts to know them. That is the vast majority of all knowledge and encompasses the things we don't even know we don't know yet. You can use a hammer on a nail without knowing anything about what is holding that hammer together or about Newton's laws.
- Explicit knowledge that you use directly. The comment is about this. Meaning, a response that lambda calculus is with us here and now implicitly falls into the first category above and is not what is meant, but why would you be better off knowing the concept directly apart from intellectual curiosity - which we can fulfill on only an insignificantly tiny fraction of the things we do.
Each time people want to add to the curriculum "you absolutely must know this!" they seem to be missing this distinction.
Given the incredibly amount of knowledge and how each and every piece of it is somehow important - but almost always only implicitly - I prefer a mindset that strives to reduce the amount I want other people to learn. Saying "no, you don't have to know/learn this" seems to be a better goal than trying to list ever more stuff. Also, the "need to know" should be much more targeted - "every programmer needs to know" is probably wrong for a lot of (most?) stuff that is labeled thus.
Looking into LC I was led to Curry's Paradox, the natural language version being "If this sentence is true, then Germany borders China" which (again, I'm probably just an idiot) doesn't strike me as paradox material.
This isn't some random reverse snobbery rant, I'm all for digging deep and really understanding things (I do this all the time, probably more than most engineers). But I can't see the Emperor's clothes everyone seems to be admiring, and it isn't for lack of looking.
I think it's clear that this is a paradox in the field of logic - but only there. Few people not trained and/or thinking of "logic" (that math thing) will find this sentence paradoxical, more like "useless/meaningless". Normal people use paradox more for things like the "French paradox" (the French are health despite eating "unhealthily"). Which isn't a paradox in any logical sense, and even on a human level I myself see the paradox more in the fact that some people see a paradox at all instead of just admitting that what they think is true about nutritional science just isn't (that French phenomenon can be shown to be true in statistics, it's not just imagination).
Maybe. Certainly, common use (and traditional use, e.g. Zeno's Paradox) include things that are not strictly a logical paradox. But I think that most people (and certainly overwhelmingly most programmers) consider "this sentence is false" to be a paradox - which is part of why I picked it as a point of reference.
JavaScript historically has no way to do namespacing. In most languages this would be a deal breaker. But because JavaScript has lambda functions, closures and first class functions a solution could be crafted from scratch! Immediately-Invoked Function Expressions (IIFE) were one of the most powerful early techniques to create scopes on the fly in JavaScript. Without these tools from the lambda calculus you would normally have to rely on language level changes to allow these problems to be fixed.
The other early challenge of JavaScript was the need for asynchronous callbacks. Often these require passing around data that you might not have access to when a function is written. Lambda functions allow programmers to quickly write ad hoc logic. First class functions allow programmers to pass around this logic. And most importantly closures allow you to create functions on the fly based on data that is not known until an asynchronous callback is applied. Again without the core ideas of the lambda calculus in place this type of power would require significant language-level design changes.
10 years ago JavaScript was a hideous language, with many major issues. But because in this mess was contained the power of the lambda calculus the language was able to be salvaged and extended to a wide range of uses.
You think that's why Javascript is widely used? I think it's widely used because it was already useable within the browser and people just kept going with it.
But what I'll say is that LC has done a lot for you lately. It, alongside Turing Machines, formed the basis for pretty much all of CS research and programming language design since the beginning of the 20th century. It has heavily influenced the design of probably every programming language you've ever used.
LC pretty much defines the notion of lexical scope. It pretty much defines the notion of constant and nearly defines the idea of variable as used in most languages. It gives a quick proof that recursion arises naturally even in very simple linguistic situations. In fact, it even gives the name of the very website you're reading right now.
LC is a huge force for how people are have been forming new ideas around Functional Programming over the last few decades and how they continue to now.
LC is hugely important. You don't have to learn it because it's already been pre-digested into everything you do in programming. But to not know it is to miss out on seeing the core of how your tools work.
However, if you want to do research, it is an invaluable model of how computation works. It's simplicity allows for reasoning about complex ideas while minimizing the cognitive overhead of the model.
It may also help you understand why certain functional styles behave the way they do or how to better implement programming languages.
If none of those things interest you, then yes, it is not useful. But a large crowd here IS interested in computer science theory and programming language theory and functional programming so they are interested.
As a final analogy, you might consider this the 'Standard Model' of computation much like there is the Standard Model in particle physics. If you are a civil engineer, it will never be useful. If you are a chemist, it might be useful only in passing. But if you are the physicist, it is invaluable.
That's a super interesting question. Pretty much the entire challenge of LC is coming to understand why it's interesting. From our perspective, so far past the consequences of this discovery, it will all seem too obvious to state. The interestingness of LC comes out of it being so austere and so powerful.
Frankly, this page's intro to it is sort of terrible. Clojure is too powerful and clunky to point directly at LC and show why it's interesting.
LC is a language with three constructors
var[x] reference a name
lam[x](...) create a scope where x is *known*
app(f, v) when f is lam[x], give
meaning to x within its body
Forget ideas of functions or anything else you know from CS. Just think about what these three constructors mean. To give them real meaning we have to define one more thing: the reduction step. It's what you think it is app(lam[x](body), value) ==> body{x -> value}
where the right side means that we replace all instances of "x" within "body" with "value".So imagine that to be the definition of a programming language---the whole thing. It seems a bit silly. It doesn't obviously have any of
- numbers
- if-the-else
- for loops
- recursion
- mutation
- data types
It doesn't even seem to have any way of talking about how it instructs a machine on what to do. It's truly austere.So the magic, of course, is that it actually does have all of the above. Those 3 constructors and one rule are powerful enough already to generate all of that.
That's what's remarkable.