5 ms·

I've been attracted to this - along with 2D cellular automata - a bit like a moth to a flame for some time. I find the little machine visualisations mesmerising

I've been attracted to this - along with 2D cellular automata - a bit like a moth to a flame for some time. I find the little machine visualisations mesmerising, the heavily parenthesized Greek representation charming (they look like standing orders written in an alien language, looking for all the world like space invaders) and the tiny code sizes magical. But I can't quite wrap my mind around the core concepts and internalize them into a mental model. It's too different from the simple world of imperative C or scripting languages I guess I call home. So I'm left watching das blinkenlights from the outside, as my attention span chokes on the layers of computer science incorporated into typical explanations. *shrug* I'd be very interested if anyone knows of an ELI5-style alternate path I could walk to break each of the concepts down one at a time. (I ask because I think this is (currently) the kind of thing I think ChatGPT would struggle to present as effectively as a human.)

joseda-hg 2y ago
It's too basic for what you need but the video from eyesomorphic [1], is a wonderful conceptual introduction [1] https://www.youtube.com/watch?v=ViPNHMSUcog https://www.youtube.com/watch?v=ViPNHMSUcog
- tromp 2y ago
  > Whilst it certainly isn't a contender for modern programming languages Yet all that separates the λ-calculus from one modern programming language, Haskell, is a layer of syntactic sugar on top, and a runtime that effectuates its pure IO actions. We can in fact compile Haskell programs using just stdin/stdout for IO into terms of the untyped lambda calculus, as wonderfully demonstrated in Ben Lynn's IOCCC entry [1], or equivalently, into BLC programs. [1] https://www.ioccc.org/2019/lynn/index.html https://www.ioccc.org/2019/lynn/index.html
  - JadeNB 2y ago
    > Yet all that separates the λ-calculus from one modern programming language, Haskell, is a layer of syntactic sugar on top, and a runtime that effectuates its pure IO actions. We can in fact compile Haskell programs using just stdin/stdout for IO into terms of the untyped lambda calculus, as wonderfully demonstrated in Ben Lynn's IOCCC entry [1]. That's what Turing completeness means, though; you can do the same thing with C, with the same provisos. (Conal Elliott has an amusing satire on this: http://conal.net/blog/posts/the-c-language-is-purely-functional http://conal.net/blog/posts/the-c-language-is-purely-functio... .) It's not that the lambda calculus isn't sufficiently expressive, just that it's not a language in which humans want to write.
    - tromp 2y ago
      I wasn't just claiming Turing completeness of Haskell. I was pointing out that every language construct, every subexpression in Haskell, directly represents a corresponding lambda term, with corresponding semantics (e.g. laziness).
      - JadeNB 2y ago
        > I wasn't just claiming Turing completeness of Haskell. I was pointing out that every language construct, every subexpression in Haskell, directly represents a corresponding lambda term, with corresponding semantics (e.g. laziness). I was referring to the Turing completeness of the lambda calculus, not of Haskell. But, again, I think that trying to work directly with lambda expressions everywhere, even if it is possible and, as you say, straightforward for "vanilla" Haskell, quickly shows why we put some semantic sugar over it. That is to say, it's certainly true that, in an obvious sense, the layer of semantic sugar is thinner for Haskell than for C, but it's still "just" semantic sugar, and still just as conceptually important, in both cases.
  - dunham 2y ago
    For anyone who's interested - Ben Lynn also has a series of articles that explain the creation of that compiler and add further enhancements: https://crypto.stanford.edu/~blynn/compiler/ https://crypto.stanford.edu/~blynn/compiler/
- nakedneuron 2y ago
  video author is using 3b1b's manim (https://github.com/3b1b/manim https://github.com/3b1b/manim). wonderful presentation.
JadeNB 2y ago
"To mock a mockingbird" (https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird) is a wonderful introduction to something that's sufficiently more abstract than lambda calculus that you'll probably find the latter pleasingly concrete afterwards, but it takes only tiny, bite-sized steps (err, mixed metaphors) to get you to understanding.
kccqzy 2y ago
The best way to wrap your mind around the core concept and internalize them into a mental model is writing an interpreter yourself. It's been abundantly clear to me since young that for anything involving math, you don't internalize it if you merely passively let someone else explain it, whether that's reading a textbook/blog or attending a professor's lecture or watching a YouTube video. You have to do the exercises. Lambda calculus is the same. You can easily define the data structure to represent a program in untyped lambda calculus and then write an interpreter for it. Then go implement some interesting concepts such as the Y combinator or the Omega combinator. If you find lambda calculus too difficult to do things like arithmetic or linked lists, you don't have to stick with Church numerals or Scott encodings. Just introduce regular natural numbers and lists as ground types; when you later have a better understanding, write programs to transform regular numerals from and to Church numerals and bask in the fact that they are isomorphic.
- prakashrj 2y ago
  I agree that you have to do the exercises instead of expecting others to explain and walk you through it. https://www.youtube.com/watch?v=LXhsutNKhec https://www.youtube.com/watch?v=LXhsutNKhec Just one programming book was able to help my son, who is 12 yrs old, learn lambda calculus and write a meta circular evaluator.
- anyfoo 2y ago
  Mathematics is not a spectator sport. I had the luck of reading that quote while I was an undergrad. I did not actually pursue a career in pure math, but it certainly helps me every time I want to understand some math in order to apply it. (Lambda calculus, type systems, Fourier/Laplace/z-transform, ...)
WorldMaker 2y ago
I think the most ELI5 approach is Alligator Eggs [0] which was built for 8-year-olds to play like a game. You can find a lot of the advanced concepts outside of the core also explained in terms of Alligator Eggs and some software visualizers, but there's also something to be said about hands on learning and about printing it out yourself on some cardstock or cardboard paper, cutting it out, personalizing it with crayons, and playing it with a child or at least your inner child. [0] https://worrydream.com/AlligatorEggs/ https://worrydream.com/AlligatorEggs/
nakedneuron 2y ago
sorry for not providing explanations, but check this out: https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html did you see https://news.ycombinator.com/item?id=42256394 https://news.ycombinator.com/item?id=42256394 (The Art and Mathematics of Genji-Ko 172 points, by olooney, 49 days ago, 10 comments)? very tangentially related, but also mesmerizing stuff, i think..
laszlokorte 2y ago
You might find my practical introduction to lambda calculus and combinatory logic based on javascript helpful. [1] Its mostly based on other introductory resources but I tried to write it from a practical step by step perspective I found most useful for myself. [1]: https://static.laszlokorte.de/combinators/ https://static.laszlokorte.de/combinators/
louthy 2y ago
Spending time with pure functional programming (languages like Haskell) will open up these concepts in a real-world programming environment. Obviously languages like Haskell are more complex than this, but they're all fundamentally based on lambda calculus. That could be the first step away from the imperative thinking you describe. (That was certainly my way in to this world anyway!)
ookdatnog 2y ago
If you have some time to spare, read SICP [0] and do the exercises :) (probably easiest to use DrRacket [1] as the interpreter) [0] https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/6515/sicp.zip/full-text/book/book.html https://mitp-content-server.mit.edu/books/content/sectbyfn/b... [1] https://docs.racket-lang.org/sicp-manual/SICP_Language.html https://docs.racket-lang.org/sicp-manual/SICP_Language.html

joseda-hg 2y ago

It's too basic for what you need but the video from eyesomorphic [1], is a wonderful conceptual introduction [1] https://www.youtube.com/watch?v=ViPNHMSUcog https://www.youtube.com/watch?v=ViPNHMSUcog

tromp 2y ago
> Whilst it certainly isn't a contender for modern programming languages Yet all that separates the λ-calculus from one modern programming language, Haskell, is a layer of syntactic sugar on top, and a runtime that effectuates its pure IO actions. We can in fact compile Haskell programs using just stdin/stdout for IO into terms of the untyped lambda calculus, as wonderfully demonstrated in Ben Lynn's IOCCC entry [1], or equivalently, into BLC programs. [1] https://www.ioccc.org/2019/lynn/index.html https://www.ioccc.org/2019/lynn/index.html
- JadeNB 2y ago
  > Yet all that separates the λ-calculus from one modern programming language, Haskell, is a layer of syntactic sugar on top, and a runtime that effectuates its pure IO actions. We can in fact compile Haskell programs using just stdin/stdout for IO into terms of the untyped lambda calculus, as wonderfully demonstrated in Ben Lynn's IOCCC entry [1]. That's what Turing completeness means, though; you can do the same thing with C, with the same provisos. (Conal Elliott has an amusing satire on this: http://conal.net/blog/posts/the-c-language-is-purely-functional http://conal.net/blog/posts/the-c-language-is-purely-functio... .) It's not that the lambda calculus isn't sufficiently expressive, just that it's not a language in which humans want to write.
  - tromp 2y ago
    I wasn't just claiming Turing completeness of Haskell. I was pointing out that every language construct, every subexpression in Haskell, directly represents a corresponding lambda term, with corresponding semantics (e.g. laziness).
    - JadeNB 2y ago
      > I wasn't just claiming Turing completeness of Haskell. I was pointing out that every language construct, every subexpression in Haskell, directly represents a corresponding lambda term, with corresponding semantics (e.g. laziness). I was referring to the Turing completeness of the lambda calculus, not of Haskell. But, again, I think that trying to work directly with lambda expressions everywhere, even if it is possible and, as you say, straightforward for "vanilla" Haskell, quickly shows why we put some semantic sugar over it. That is to say, it's certainly true that, in an obvious sense, the layer of semantic sugar is thinner for Haskell than for C, but it's still "just" semantic sugar, and still just as conceptually important, in both cases.
- dunham 2y ago
  For anyone who's interested - Ben Lynn also has a series of articles that explain the creation of that compiler and add further enhancements: https://crypto.stanford.edu/~blynn/compiler/ https://crypto.stanford.edu/~blynn/compiler/
nakedneuron 2y ago
video author is using 3b1b's manim (https://github.com/3b1b/manim https://github.com/3b1b/manim). wonderful presentation.

JadeNB 2y ago

"To mock a mockingbird" (https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird) is a wonderful introduction to something that's sufficiently more abstract than lambda calculus that you'll probably find the latter pleasingly concrete afterwards, but it takes only tiny, bite-sized steps (err, mixed metaphors) to get you to understanding.

kccqzy 2y ago

The best way to wrap your mind around the core concept and internalize them into a mental model is writing an interpreter yourself. It's been abundantly clear to me since young that for anything involving math, you don't internalize it if you merely passively let someone else explain it, whether that's reading a textbook/blog or attending a professor's lecture or watching a YouTube video. You have to do the exercises. Lambda calculus is the same. You can easily define the data structure to represent a program in untyped lambda calculus and then write an interpreter for it. Then go implement some interesting concepts such as the Y combinator or the Omega combinator. If you find lambda calculus too difficult to do things like arithmetic or linked lists, you don't have to stick with Church numerals or Scott encodings. Just introduce regular natural numbers and lists as ground types; when you later have a better understanding, write programs to transform regular numerals from and to Church numerals and bask in the fact that they are isomorphic.

prakashrj 2y ago
I agree that you have to do the exercises instead of expecting others to explain and walk you through it. https://www.youtube.com/watch?v=LXhsutNKhec https://www.youtube.com/watch?v=LXhsutNKhec Just one programming book was able to help my son, who is 12 yrs old, learn lambda calculus and write a meta circular evaluator.
anyfoo 2y ago
Mathematics is not a spectator sport. I had the luck of reading that quote while I was an undergrad. I did not actually pursue a career in pure math, but it certainly helps me every time I want to understand some math in order to apply it. (Lambda calculus, type systems, Fourier/Laplace/z-transform, ...)

WorldMaker 2y ago

I think the most ELI5 approach is Alligator Eggs [0] which was built for 8-year-olds to play like a game. You can find a lot of the advanced concepts outside of the core also explained in terms of Alligator Eggs and some software visualizers, but there's also something to be said about hands on learning and about printing it out yourself on some cardstock or cardboard paper, cutting it out, personalizing it with crayons, and playing it with a child or at least your inner child. [0] https://worrydream.com/AlligatorEggs/ https://worrydream.com/AlligatorEggs/

nakedneuron 2y ago

sorry for not providing explanations, but check this out: https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html did you see https://news.ycombinator.com/item?id=42256394 https://news.ycombinator.com/item?id=42256394 (The Art and Mathematics of Genji-Ko 172 points, by olooney, 49 days ago, 10 comments)? very tangentially related, but also mesmerizing stuff, i think..

laszlokorte 2y ago

You might find my practical introduction to lambda calculus and combinatory logic based on javascript helpful. [1] Its mostly based on other introductory resources but I tried to write it from a practical step by step perspective I found most useful for myself. [1]: https://static.laszlokorte.de/combinators/ https://static.laszlokorte.de/combinators/

louthy 2y ago

Spending time with pure functional programming (languages like Haskell) will open up these concepts in a real-world programming environment. Obviously languages like Haskell are more complex than this, but they're all fundamentally based on lambda calculus. That could be the first step away from the imperative thinking you describe. (That was certainly my way in to this world anyway!)

ookdatnog 2y ago

If you have some time to spare, read SICP [0] and do the exercises :) (probably easiest to use DrRacket [1] as the interpreter) [0] https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/6515/sicp.zip/full-text/book/book.html https://mitp-content-server.mit.edu/books/content/sectbyfn/b... [1] https://docs.racket-lang.org/sicp-manual/SICP_Language.html https://docs.racket-lang.org/sicp-manual/SICP_Language.html