[dewster]

I'm probably showing my profound ignorance, but what has lambda calculus done for me lately? It seems to be an abstract formalism of some sort, but I've yet to see any real use of it, the examples are baby step type stuff with obfuscated syntax.

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?

[krapp]

>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.

[0]https://en.wikipedia.org/wiki/Lambda_calculus

[1]https://en.wikipedia.org/wiki/Church-Turing_thesis

[Drup]

> trendy crap

> 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.

[lisper]

Here is how you can use the lambda calculus to compute factorials in non-geological time:

http://www.flownet.com/ron/lambda-calculus.html

[viebel]

There is also this article about Y-combinator implemetation in clojure: http://www.viksit.com/tags/clojure/practical-applications-y-...

[dewster]

OMG, that's insane (in a bad way). Stacks exploding, hours of optimization, all for a simple factorial (toy problem). Exciting I suppose for a few souls in academia who spend their lives writing papers about theoretical stuff (not that there's anything wrong with that).

[lisper]

Oh dear, I have failed. The whole point of that paper was supposed to be that all this theory stuff actually has practical applications. The same techniques that worked on that toy problem can be used on real problems and produce similar results.

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.

[dewster]

If we were playing the Hot and Cold game you would be getting colder.

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?

[lisper]

No, of course not. Factorial are just an illustrative example.

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.

[dewster]

Your initial words were "Here is how you can use the lambda calculus to compute factorials in non-geological time" which led me to believe you were claiming LC was a very (the most?) efficient route to factorial calculation. Which would make me sit up and take notice were that the case.

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.

[brudgers]

Hacker News, was written in a Lisp. Lisp was developed as a language for more closely describing programs in the manner Lambda Calculus describes algorithms in contrast to languages for describing programs more closely to the manner in which Turing Machines describe algorithms.

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.

[Noseshine]

I think there are two interpretations and @dewster probably wants to refer to only one of them:

- 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.

[dewster]

Thank you for expressing that better than I could ever do. Outside of JS sucking but being saved by extensibility, and academic interests, I've never heard a concrete reason why LC is important in a practical sense to most programmers. Can't swing a dead cat on the internet without hitting an LC article lately, and I really don't get the sudden interest and insistence that we all must learn it.

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.

[dllthomas]

"If this sentence is true, <false thing>" is a paradox like "this sentence is false". Implication is trivially true when the condition is false. But that would make the condition true and the sentence false.

[Noseshine]

So once again I try to interpret OP:

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).

[dllthomas]

> Normal people use paradox more for things like the "French paradox"

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.

[Homunculiheaded]

The best answer to this is the success of JavaScript. JavaScript historically has been a deeply flawed language. However, it was able to become one of the most widely used languages precisely because, despite all its warts, it implements the core foundations from the lambda calculus correctly (lambda functions, first class functions and closures). This allowed JS programmers enormous power to overcome these warts. Here are two examples:

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.

[asciihacker]

> it was able to become one of the most widely used languages precisely because, despite all its warts, it implements the core foundations from the lambda calculus correctly

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.

[tel]

As others have noted, LC is hardly trendy crap and you might say that 80% of CS is just trying to find more natural names for LC.

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.

[dewster]

Again, I'm most likely an idiot, but I'm just not seeing it in any of the examples I've encountered. Not trying to be dense, I realize the onus is mostly on me here, and I really am interested in fundamentals. Just wondering if there is a better example of why I should go out of my way to understand lambda calculus, cause this one ain't cutting it. LC may well indeed form the basis of everything CS - if so why doesn't it seem very impressive at first (and second, and third) sight?

[tel]

> why doesn't it seem very impressive at first (and second, and third) sight?

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.

[eximius]

If you work in a big company making internal web apps for HR to manage payroll, then no, the lambda calculus will never be useful to you.

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.