4 ms·

There has to be some programmer rite of passage involving learning lambda calculus. I went through this a few years ago when something similar was posted. I lea

by dexwiz 3y ago

There has to be some programmer rite of passage involving learning lambda calculus. I went through this a few years ago when something similar was posted. I learned the notation, marveled at its dual simplicity and completeness, and and did a few exercises. But I came out the other side none the wiser. I think I was looking for some great epiphany on the nature of computation. Alas, it eluded me in the end. It was fun but ultimately useless for me.

somat 3y ago
You will probably be wanting unlambda then. an implementation of the lambda calculus without the lambda forms. http://www.madore.org/~david/programs/unlambda/ http://www.madore.org/~david/programs/unlambda/
tombert 3y ago
I love theory, and I also really like lambda calculus, but I feel like this sentiment applies to most theory, particularly stuff after undergrad. I spent a not-insignificant amount of time learning how to do proofs with Isabelle. I learned a lot about inductive proofs, set theory, meta-logic, and challenged myself to prove a lot of the stuff I had previous taken for granted (e.g. proving that different sorts refine each other). I enjoyed it, and similarly was convinced that this was going to be some life-changing thing that changes my career trajectory and... Nothing changed. No one in charge of companies gives a shit about theory. They all claim that they love theory, they claim that they are very research focused, they claim that they value all the time you spent learning this stuff, but in reality they really just want you to change the color of buttons, or change the format of dates, or add a field to a JSON. It sometimes feels like no software engineer but me actually wants to learn any math, and will refuse to touch anything even resembling it. And I'm not picking on Isabelle here; I've had similar results trying to pitch TLA+ and Coq and Agda for some of the more error-prone parts of the codebase, with different sales-pitches, and without fail the managers will always say that they "will look into it", and promptly do absolutely nothing. The first two times a manager said that, I believed them, but after that I realized that they're just trying to shut me up and tell me "no" politely. It was enough to depress me, and it still kind of does. I still think learning stuff for fun is worth it, but I'd be lying if I told you if I knew why.
- hnoyrnndd 3y ago
  A friend of mine worked at Rockwell Collins and wrote proofs, and theorem provers, all day. If you work on webshit like me you won’t get to use these skills much. (On the other hand, recursing over the structure of JSON-like data often feels like 80% of the job, so I think the skills come into play at least a tiny bit).
  - tombert 3y ago
    I work on web-adjacent-shit, mostly data processing stuff in Kafka that eventually ends up on the web. I don't get to recurse over JSON, occasionally I get to design a system from scratch and that's more fun, but it's usually not more complicated than "draw boxes that point to other boxes and/or cylinders on screen". Sometimes I draw a picture of cloud. I like my job just fine, it's a decent job, and I like my managers and coworkers as well, but it's just disappointing that enthusiasm for math and theory is what got me to this stage of my career, but I never really got to use it, and I don't see that ever really changing for me. Maybe I will write a paper at some point at least.
    - andoando 3y ago
      Yeah I am at the same place. Considering going for a phd because at this point I cant muster any kind of interest in corporate tech.
      - tombert 3y ago
        From experience, that has its own share of frustrations as well. You get to work in theory and that’s fun, but if you decide to do a PhD while also working a desk job, I recommend you do not tell your employers. I made the mistake of telling an employer, and whenever I made any mistake in my work, no matter how small, the employer would immediately say that the PhD work is distracting me, and my focus not BigCo. My PhD is on an indefinite hiatus right now, because it’s something I am questioning the utility of right now.
        3y ago
mjh2539 3y ago
I used it in a graduate course on formal semantics (https://www.wiley.com/en-us/Semantics+in+Generative+Grammar-p-9780631197133); https://www.wiley.com/en-us/Semantics+in+Generative+Grammar-... after I graduated I wanted to learn how to program so I googled "lambda calculus programming language" and found Haskell. That was ten years ago. Though I rarely use Haskell anymore, the lambda calculus still holds a special place.
DonaldPShimoda 3y ago
The "utility" of the lambda calculus, in my opinion, comes down to Church's original choice of terminology. He did not call the things denoted by lambda "functions"; rather, they were abstractions. What makes the lambda calculus so cool is that it lets us see that abstraction is the root of all computation, at least through one perspective (as opposed to the Turing point of view). Learning the lambda calculus directly will allow you to appreciate functions ("abstractions") and use them more effectively; you can reason about their computation and composition.
- andoando 3y ago
  I dont quite think of functions and abstractions as the same. Abstractions seem to do more with having a self referential property. Though I suppose that can be seen as the identity function f->f. IIRC Church was heavily influenced by Turing and vice versa.
  - dexwiz 3y ago
    Turning was Church’s student.
    - tromp 3y ago
      It's amazing how often Turing gets miss-spelled as Turning. Is that because of overzealous spell checkers?
      - deleted 3y ago
        [deleted]
      - dexwiz 3y ago
        Probably, I posted that from my phone.
- 082349872349872 3y ago
  Might the terminology have been due to early awareness of the cardinality problem associated with the abstractions (D->D) being a subset of the values (D)?
NotCamelCase 3y ago
Funny that you bring this up -- I feel exactly the same way and I even had more math background than average SW person. Being on the engineering side of things without much knowledge/focus on programming languages theory and the mathematical nature of computation, one feels as if all the niceties we have in popular PLs are just laws of nature that we just had to discover, whereas in reality they too had to be derived, tried, improved first. But then you study something like this and expect to be able to finally connect the dots and yet, it's still not immediately obvious how we arrived here!
agumonkey 3y ago
The Y combinator (npi) was also a very mind opening exercise. Even recreating pairs was quite fun.

by dexwiz 3y ago

somat 3y ago

You will probably be wanting unlambda then. an implementation of the lambda calculus without the lambda forms. http://www.madore.org/~david/programs/unlambda/ http://www.madore.org/~david/programs/unlambda/

tombert 3y ago

I love theory, and I also really like lambda calculus, but I feel like this sentiment applies to most theory, particularly stuff after undergrad. I spent a not-insignificant amount of time learning how to do proofs with Isabelle. I learned a lot about inductive proofs, set theory, meta-logic, and challenged myself to prove a lot of the stuff I had previous taken for granted (e.g. proving that different sorts refine each other). I enjoyed it, and similarly was convinced that this was going to be some life-changing thing that changes my career trajectory and... Nothing changed. No one in charge of companies gives a shit about theory. They all claim that they love theory, they claim that they are very research focused, they claim that they value all the time you spent learning this stuff, but in reality they really just want you to change the color of buttons, or change the format of dates, or add a field to a JSON. It sometimes feels like no software engineer but me actually wants to learn any math, and will refuse to touch anything even resembling it. And I'm not picking on Isabelle here; I've had similar results trying to pitch TLA+ and Coq and Agda for some of the more error-prone parts of the codebase, with different sales-pitches, and without fail the managers will always say that they "will look into it", and promptly do absolutely nothing. The first two times a manager said that, I believed them, but after that I realized that they're just trying to shut me up and tell me "no" politely. It was enough to depress me, and it still kind of does. I still think learning stuff for fun is worth it, but I'd be lying if I told you if I knew why.

hnoyrnndd 3y ago
A friend of mine worked at Rockwell Collins and wrote proofs, and theorem provers, all day. If you work on webshit like me you won’t get to use these skills much. (On the other hand, recursing over the structure of JSON-like data often feels like 80% of the job, so I think the skills come into play at least a tiny bit).
- tombert 3y ago
  I work on web-adjacent-shit, mostly data processing stuff in Kafka that eventually ends up on the web. I don't get to recurse over JSON, occasionally I get to design a system from scratch and that's more fun, but it's usually not more complicated than "draw boxes that point to other boxes and/or cylinders on screen". Sometimes I draw a picture of cloud. I like my job just fine, it's a decent job, and I like my managers and coworkers as well, but it's just disappointing that enthusiasm for math and theory is what got me to this stage of my career, but I never really got to use it, and I don't see that ever really changing for me. Maybe I will write a paper at some point at least.
  - andoando 3y ago
    Yeah I am at the same place. Considering going for a phd because at this point I cant muster any kind of interest in corporate tech.
    - tombert 3y ago
      From experience, that has its own share of frustrations as well. You get to work in theory and that’s fun, but if you decide to do a PhD while also working a desk job, I recommend you do not tell your employers. I made the mistake of telling an employer, and whenever I made any mistake in my work, no matter how small, the employer would immediately say that the PhD work is distracting me, and my focus not BigCo. My PhD is on an indefinite hiatus right now, because it’s something I am questioning the utility of right now.
      - 3y ago

mjh2539 3y ago

I used it in a graduate course on formal semantics (https://www.wiley.com/en-us/Semantics+in+Generative+Grammar-p-9780631197133); https://www.wiley.com/en-us/Semantics+in+Generative+Grammar-... after I graduated I wanted to learn how to program so I googled "lambda calculus programming language" and found Haskell. That was ten years ago. Though I rarely use Haskell anymore, the lambda calculus still holds a special place.

DonaldPShimoda 3y ago

The "utility" of the lambda calculus, in my opinion, comes down to Church's original choice of terminology. He did not call the things denoted by lambda "functions"; rather, they were abstractions. What makes the lambda calculus so cool is that it lets us see that abstraction is the root of all computation, at least through one perspective (as opposed to the Turing point of view). Learning the lambda calculus directly will allow you to appreciate functions ("abstractions") and use them more effectively; you can reason about their computation and composition.

andoando 3y ago
I dont quite think of functions and abstractions as the same. Abstractions seem to do more with having a self referential property. Though I suppose that can be seen as the identity function f->f. IIRC Church was heavily influenced by Turing and vice versa.
- dexwiz 3y ago
  Turning was Church’s student.
  - tromp 3y ago
    It's amazing how often Turing gets miss-spelled as Turning. Is that because of overzealous spell checkers?
    - deleted 3y ago
      [deleted]
    - dexwiz 3y ago
      Probably, I posted that from my phone.
082349872349872 3y ago
Might the terminology have been due to early awareness of the cardinality problem associated with the abstractions (D->D) being a subset of the values (D)?

NotCamelCase 3y ago

Funny that you bring this up -- I feel exactly the same way and I even had more math background than average SW person. Being on the engineering side of things without much knowledge/focus on programming languages theory and the mathematical nature of computation, one feels as if all the niceties we have in popular PLs are just laws of nature that we just had to discover, whereas in reality they too had to be derived, tried, improved first. But then you study something like this and expect to be able to finally connect the dots and yet, it's still not immediately obvious how we arrived here!

agumonkey 3y ago

The Y combinator (npi) was also a very mind opening exercise. Even recreating pairs was quite fun.