A Flock of Functions: Combinators, Lambda Calculus, & Church Encodings in JS - Part II

🔗 Part I: • Lambda Calculus - Fund... 🔗 Slides: bit.ly/2xpcPKn 🔗 Repo: github.com/glebec/lambda-talk
A presentation given at Fullstack Academy of Code, by instructor Gabriel Lebec. The Lambda Calculus is a symbol manipulation system which suffices to calculate anything calculable. This branch of pure mathematics forms the backbone of functional programming languages, and here it is presented through the concrete and familiar lens of JavaScript.

[@glebec]

ERRATA: 21:32, `Thrice Twice` should be equal to `Twice ∘ Twice ∘ Twice`, not `Twice(Twice(Twice)))`. It would be correct to say `N3 N2 f = N2 (N2 ( N2 f)))`.

[@Jasoet]

What REPL did you use for testing the notation?

[@Jasoet]

its js repl. so nevermind :D

[@glebec]

Yep, Node.

[@abedrole7512]

Thank you, one of the greatest educational I've seen about computing. Definitely more elegant than Turing machines.

[@abedrole7512]

By the way I used those booleans functions and operators to compute branches when extending an assembler in Scheme - so it's a totally practical thing. I didn't knew about their origin - so I'm proud to say that I rediscovered them in some way. I was stucked when I made the parallels with your formulas. 👍

[@AegirAexx]

You changed my life. Things will never be the same for me.

[@DOROnoDORO]

may i ask why?

[@NonTwinBrothers]

@@DOROnoDORO I think he turned into a reeeeeally big half-life fan or something

[@user-tx4wj7qk4t]

​@@DOROnoDORObecause you can use combinators to compose functions and write better code, particularly tacit code

[@dimitarivanov7249]

​@@DOROnoDOROI am no longer gay after watching this

[@DOROnoDORO]

@@dimitarivanov7249 I'm sorry for your loss

[@VladTrishch]

I was clapping along with the audience. Awesome talk!

[@mateja176]

People love your content, the comments speak for themselves! You should make more videos, perhaps expanding further or taking an in depth look at some of the covered topics.

[@glebec]

I appreciate it! Would like to produce some more content, have to think on what I'd like to tackle next. There are so many monad tutorials and y-combinator explanations out there already, I'd like to find a new spin if possible… but I also know I shouldn't let the existence of other sources stop me from developing my own.

[@mateja176]

Well said, sir! Like 3blue1brown said the quality of content depends on the originality of the idea and how it is presented. May you find the right intersection between the two and of course what's fun for you.

[@Seunmanuel]

Gabriel Lebec You are such an awesome teacher.... 🙏 Kindly do a tutorial on category theory and monads also in JavaScript... Thank you.

[@waltermelo1033]

@@glebec your way of teaching is much more appealing than almost any teacher that i saw, no one can explain lambda calculus so clearly, you can make a youtube channel based on this :D

[@DaniloSouzaMoraes]

@@glebec I really, really liked the historical context with the explanation. It brings intuition for what you teach. I would personally like to see more content contrasting the different mathematicians and church vs turing.

[@DimensionEpic]

Just to be clear: make sure if youtube dies, or google, or internet... this talk survives. Any post-apocalyptic humanity, or next civilization in this planet, would need this. I'm been studying about this for decades, and there is no way you can get the same amount of information in less time. Thank You Gabriel, what you did is a Treasure ! These are the foundations of everything. One can conquer the universe, just with these tools and a towel.

[@psychedel0c]

4 years later and people are still using this to learn lambda calc. I wish you were my prof man, you make this material so much easier to understand and your enthusiasm is so contagious

[@Michael-sh1fb]

I'm so glad you uploaded this separately. Would have been a great shame to miss out on this. Your talk was amazing. The way you combined and continually built upon concepts from earlier in the talk is excellent. This is also a master class in how to design and write slides. Functional programming has always somewhat eluded me, and I feel like this is the basis I've been missing

[@rbettsx]

This is such a contrast to other presentations on the subject at business-oriented programming conferences. 1. The graphics/typography genuinely elucidate, and act as a mnemonic for, the subject matter, in a way a chalkboard never could. They are not mere decoration. A great example for any student of graphic design. 2. The tone of authentic humility. Not: 'I am showing you how clever I am', but: 'i am sharing how beautiful this is'.

[@marcusklaas4088]

This part was even better than the first. Bravo!

[@Zjooji]

I think this might be my first or second comment ever on youtube. I just wanted to say thank you. I really enjoyed both of these. It was really interesting and I enjoyed your enthusiasm. :)

[@glebec]

Thanks for going the extra mile to comment! Always nice to hear feedback. :-)

[@kvadratbitter]

27:44 aah, that explains why I couldn’t quit this video...

[@Yetipfote]

lol good one!

[@xZodax]

Nice talk! I had been willing to learn a bit about lambda calculus for some time and this deserves being on the top spot of youtube searches. :D Thanks a lot!

[@glebec]

xZodax thanks for the kind words.

[@andreaszweili8593]

You deserve an award for this talk. Very well done congratulation!

[@fredericferaud9106]

A great thanx (5 years later) : it's definitely the simplest material I found about Lambda Calculus. Neat, enthusiastic, and with historical references. Great job !

[@Jannic91]

I also rarely comment on KZbin but this ... amazing talk, the only video on whole KZbin which really taught me something about FP. Most videos on here talk about how using map instead of a for loop is functional programming. Subscribed and looking forwards to more content! Would love to see an introduction to Haskell from you. I tried learnyouahaskell, but its really hard to work through when every sentence is: So here is this function it does this, there is also this function that does this, and there is this function that does that ... In contrast to that your talk is like hey lets create this function. It looks like this any Idea how to do this. So what do we need this this and that and it does this and btw its essentially this other function we already know *mind blown* This really keeps you thinking along and reestablishes the previous concepts (which gives you that satisfying aha moment). Sorry for the long post, but you get the idea I'm stoked I found this talk.

[@glebec]

Well thanks very much for your comments! Makes me happy to hear that the talk stoked your interested in the subject. I would enjoy making an intro to Haskell, but given that I'm still relatively new to the language (got into it this year) I'd want to think for a while about the best way to go about it. I found that learnyouahaskell was a fast and casual way to get exposure to a lot of the language quickly, but it didn't "stick" very well; Haskell Book (aka Haskell Programming From First Principles) is much more in-depth and the exercises help you truly learn the language, but it's also very long, drier in style, and requires some discipline to push through. On the subject of FP, you may want to check out Kyle Simpson's nicely gradual github.com/getify/Functional-Light-JS book. It carefully steps through FP in a sequential way. On the other end of the spectrum, see Brian Lonsdorf (aka DrBoolean, aka Professor Frisby) and his various articles / videos. His live talks tend to go whiplash fast, but his Egghead video series and GitBook (Prof. Frisby's Mostly Adequate Guide to Functional Programming) are a bit more step-by-step, and he has a fun / silly style.

[@Jannic91]

Thanks for your suggestions, I'll have a look at the Haskell Book (I don't really mind math stuff, quite the opposite I think its really interesting) and Functional-Light-JS also looks promising. I started the Mostly Adequate Guide to Functional Programming but somehow stopped at chapter 7. I don't even know why because I quite liked it until then as far as I remember, I'll definitely revisit it.

[@peterostertag8699]

Thank you, first time that I understood what this is all about! And I did not know that js can be so elegant. At first sight I thought it was Haskell

[@garyliddon]

Thank you so much for these two videos; amazing seeing Boolean logic, basic math derive and memory from a minuscule set of rules.

[@processing7836]

You have gotten me so excited to learn lambda calculus and to try to rederive all of the things you showed in your talk on my own. I just ordered To Mock a Mockingbird and can't wait to get started on it.

[@glebec]

Psyched to hear it! My 2c about To Mock a Mockingbird: don't be reluctant to read the answers. Smullyan presents a LOT of challenges, and not always in the easiest order; problem 1 might be very difficult, and problem 2 trivially simple. I made a lot more progress in the book and enjoyed it much more once I let go of the stubborn feeling that I had to solve everything myself.

[@samueleagostinelli5346]

Me too! This subject is super interesting! :P

[@caosed4991]

This video is going in my changed my life playlist. Really loved it!

[@bielosX]

Thank you for this. Finally i understand lambda calculus. Awesome examples.

[@nilp0inter2]

What a beautiful talk. Congratulations!

[@LearnedSome]

Thank you very much for putting this out for free.

[@iminsik]

It's really mind-blowing, and is the the only material and lecture I can understand lambda calculus. Nice work!

[@tobias-edwards]

Brilliant talk, beautiful slides too

[@arsnakehert]

Oh my god, so lucky this showed up in my recommended after watching the first part!

[@gsashee]

Thank you for this excellent video (and also for the previous one). Very informative and well presented.

[@logauit]

This is amazing Gabriel! Thank you for these `Combinators, Lambda Calculus` explanation.

[@romaing.1510]

Amazing presentation (the two parts) !

[@shyamspeaking]

Wonderfully clear presentation. I am going back to my lambda calculus book now. Thank you.

[@replikvltyoutube3727]

This is a really good hands on demonstration, thanks!

[@poe84it]

@33.29 when you double checked Phi, you have passed to Vireo the second argument with a comma, not by a second call. By the way, great talk! Thanks a lot! You've inspired me!

[@glebec]

Yep, I saw it later. Hard to fight JS habits sometimes! Functional languages like Haskell borrow LC's application syntax of just a space, so there isn't a need for all the parens. Thanks for the kind words, -G.

[@AndrewSmithDev]

This was absolutely great thanks for posting it

[@1K1NDR3D]

Great talk. Thank you!

[@ALL_ONE_SUN]

Planning to watch this later. Glad I saw it today though. Seems to be one of the best videos I have found on the topic. Thanks! (Great starting with defining how to define a number from a blank by the way)

[@glebec]

Be sure to watch Part I at kzbin.info/www/bejne/aYe0ZGtohqxgr5Y. :-)

[@benduplessis6327]

Brilliant speaker. LC makes a lot more sense now

[@glebec]

Very kind of you! I am happy to make LC clearer.

[@zernnavier]

Amazing explanation and clear presentation. Kindly make a video on Monad and Monoid.

[@goobah01]

Excellent pair of videos. The birds do nothing for me but it a superbly clear walk through λ Church numerals always remind me of a secondary school math teacher I had who stumped us 11 year olds with “Try to explain what 2 is. See you next lesson”. He didn’t do Church numerals but he wanted us to think.

[@qwerty-mz8is]

Amazing video! Mind blown!

[@glebec]

Thanks! Glad you enjoyed it.

[@teamacio9043]

Will you do part 3? This series is the best explanation i have found out there. You could cover lists (nil,isnil,head,tail,fold,infinite lists), functors and monads

[@glebec]

I'm glad you enjoyed it. For a while I didn't think I'd be likely to do a part 3 as I didn't have a strong feeling of what topics I'd like to cover, in what style, etc. - at least, without it feeling too similar to Michaelson's book. Lately though I've been having some fun with LC on Codewars and thinking that Scott encodings (of algebraic data types), multiple list representations, other number representations (Scott, BinaryScott) etc. could make a good continuation of the series. Perhaps I will make a part 3 at some point. Functors and Monads don't have a first class representation in the untyped lambda calculus. They _exist_, in the sense that lists are functorial, Maybe is functorial, and so on, but without polymorphism / typeclasses / etc. it's hard to capture the notion in a way that is clear or helpful in the base LC per se. Still, implementing list-map, maybe-map and so on could be a good bit of content. At some point though that feels more natural and helpful in something like Haskell (which is based on an augmented form of LC) and there are many good resources for learning Haskell per se. Still, something to keep in mind.

[@teamacio9043]

@@glebec Alright, thanks for responding and explaining. :)

[@jogadornumerozero3257]

5 years later, trying to learn this thing XD thanks from Brasil, teacher, u are awesome

[@AryaMh]

Thanks a lot man, it was very helpful.

[@K1rac]

Thank you for this. This is so cool.

[@ycombinator765]

Thanks a lot for this masterpiece!!!! And Merry Christmas! Would you ever cover how Functional Languages are translated into the machine code?

[@glebec]

It would be a great topic I think, but I'd want to learn a lot more about it firsthand - right now most of what I know about compiling functional languages is from reading other peoples' summaries. :-)

[@user-df9gs2yh9e]

This is so good!

[@MhdBasharDas]

Thanx for your great efforts

[@gampolt]

Awesome video

[@trisimix]

This is pretty great

[@arsnakehert]

Best thing about JS videos is how you can just open a console in your browser and hack along

[@glebec]

I am glad you noticed! I wanted the demo to proceed from a blank slate so anyone could try it.

[@arsnakehert]

@@glebec lol, I'm so used to and biased towards editing files and then running them I literally forget I can open up a REPL and just experiment with things when I need to

[@rationalagent6927]

Awsome talk

[@gm2407]

What I like about Lambda calculus is that it gives function to thought. Pun not intended. A person grapaling with a problem defines the constituant parts and applys function to the issue. It is a beautiful poetry.

[@glebec]

I also very much like the functional way of breaking down a program into data inputs and data outputs. When I approach solving a code problem now, my first question is almost always "what is the type of at least some sub-problem here." If I can start with a type signature for some part of the code, everything else can flow outwards from there. Lambda Calculus per se doesn't have a notion of types, but I think types and functions go together like PB&J, or ham and swiss, or whatever your favorite combo might be.

[@BjarkeEbert]

This is very useful if you want to program in the great Unlambda programming language! :-D

[@rpdladps]

많은 도움이 되었습니다.

[@rossgeography]

amazing talk

[@MrBetaJacques]

Thank you very much. I will pass my funktional programming course because of this, you've been a great help

[@adumont]

I love this video and the previous one. I discovered them last month, and I've been watching them twice, and I'm sure I'll watch succ(twice) or more. I have a question though, I don't get why LEQ = is0(SUB n k). I would tend to think is0(SUB n k) would be EQ not LEQ.

[@glebec]

Thanks! As to why `LEQ = is0(SUB n k)`, the reason is because so far our Church Numerals are a functional encoding of the Natural numbers {0, 1, 2, ..} and don't have a representation (yet) for negative. The way we defined `SUB`, if you subtract anything from zero, you end up with zero again. So for example, `SUB FIVE FOUR = ONE`, `SUB FIVE FIVE = ZERO`, but also `SUB FIVE SIX = ZERO` and `SUB FIVE SEVEN = ZERO`. Therefore if our result is `ZERO` all we know is that the left-hand number (the "minuend") was equal to _or less than_ the right-hand number (the "subtractahend"). Now, what is the actual machinery by which our subtraction function "bottoms out" when it hits zero? We defined subtraction in terms of repeatedly applying a predecessor function `PRED`; in turn, `PRED` was defined by counting *up* N times from a pair `(0, 0)` by shifting the right element to the left and incrementing the right. To get the `PRED ZERO`, we count up _zero_ times from the pair `(0, 0)`, so we still end up with `ZERO` as a result. In other words, for our Church numeral encoding of Natural numbers, the predecessor of ZERO is ZERO.

[@adumont]

@@glebec thanks for the explanation, all clear now. Really amazing quality talks, I do hope you make more on lambda calculus subjects, it amazes me.

[@max1point8t]

Mind. Blown.

[@Yetipfote]

I think my brain imploded and exploded at the same time.

[@MisterFanwank]

I really love all of my string operations being at least O(n) because of null termination. This gives me that same feeling inside.

[@glebec]

Hah! Yes, naturally many of the encodings (especially Church numerals) in the raw simply-typed lambda calculus are completely unpractical for actual computing - though as a mathematical formalism intended to prove facts *about* computation, compute time is not the original purpose. That being said (as in part I), modern functional languages provide the most of the capabilities of lambda calculus (first-class anonymous higher-order functions, currying) while still taking advantage of the underlying imperative hardware (e.g. IEEE 754 floats). Funnily enough though, the classic functional String type as seen in Haskell is indeed a linked list of characters, which does have poor runtime complexity for many algorithms. In practice, Haskell-written apps often turn to the Text datatype instead, which is optimized for typical text-y things.

[@please.stop.coping]

I kept misinterpreting fab as f(a(b)) when its actually f(a)(b) since f takes two parameters.

[@glebec]

Yep, it takes some time to get used to reading `f a b c` as `f(a)(b)(c)`, but after a while it becomes second nature!

[@hasanrazza1]

The arguments in lambda calculus are also functions right? So, when we write const once = f => a => f(a), the "a" here is also a function - correct?

[@biglukegolem]

Yes thats correct. The lambda calculus just has three things variables functions and function application. So either a is not specified variable or its a function, you don't have stuff like integers unless you define them and in order to do that you would encode an int as a function.

[@glebec]

This is a great question with a more complicated answer than one might expect. I would start by saying that in combinatory logic, the only things that exist are combinators (like K, I, S, M, B, C, etc.) which are effectively functions. So combinators take combinators and return combinators. In that system, you *must* start with some predefined combinators and then all you can do is derive new combinators - so in CL, everything is a function, 100%. At first glance, lambda calculus seems similar. The *syntax* for LC only gives you lambda abstractions (i.e. function definitions), applications (i.e. function invocations), and variables. What can the variables stand for? Well, it looks like the answer would be "more lambdas," and indeed that is often the case. Certainly when using LC to study computation from a mathematical / formal perspective, we are often modeling combinatory logic using lambda calculus syntax. However, LC does not necessarily *require* that variables stand for lambdas or combinators or functions or anything else. Within LC, variables could stand for *nothing* - that is, they can be meaningless symbols with no binding. And even further, part of the beauty of LC as it pertains to programming is that variables could stand for other concepts not defined within LC per se. For example, you can invent an "extended" LC where you state that variables can also stand for concepts (like colors, shapes, feelings, numbers, bools, whatever). LC doesn't "know" about such concepts, so the most it can do is shuffle such variables around, taking them as params and returning them as expressions or closures. But you would still be "doing lambda calculus" if you were to use beta reduction, eta reduction, alpha equivalence, etc. to mechanically rewrite expressions where (orthogonally speaking) some of the variables happen to stand for "external" concepts. Note that in this talk I never do that! I use lambda calculus to express combinatory logic, and I use combinatory logic to *encode* or *derive* new concepts like bools, numbers, tuples, etc. (and their associated operations). So every variable or param in this talk is either a function (including functional encodings of bools/numbers/etc.) OR it is a free variable with no binding, and therefore no meaning at all. But you definitely *could* "enhance" LC with variables that stand for non-LC entities, and that is basically what functional programming languages do all the time. E.g. in Haskell we can write `(\a -> a) 5`, and that applies the identity lambda to the computer notion of an Int. Mixing LC with common software datatypes.

[@hasanrazza1]

@@glebec Thank you for the in depth explanation; I am extremely grateful for the time you took out to write it. If I've understood correctly, I would say that LC is basically encoded logic e.g., what are we doing given something (a function, number, color, or anything else), and combinators are sort of building blocks or atoms of logic, using whom we can build more complex logic of any complexity. I guess this is what Moses Shonfinkel set out to do? Find the most basic way to express logic and build complex logic constructs using them.

[@glebec]

@@hasanrazza1 some more quick responses: (1) "…I would say that LC is basically encoded logic e.g., what are we doing given something (…)" - Mostly yes. IMHO LC is a set of syntactic rules for replacing parts of a written expression; what you _do_ with LC can definitely include encoding certain logical concepts and processes. The main thing LC provides is a system for "computation," i.e. carrying out stepwise logical procedures of a certain richness / complexity. LC is ultimately the mechanical rewriting idea, but that rewriting is _powerful enough_ to express complex computations (through functional encodings). (2) "…and combinators are sort of building blocks or atoms of logic, using whom we can build more complex logic of any complexity" - yep! And since LC is a system for writing definitions of functions, and combinators are a subset of functions, you can define combinators manually in LC, and then perform combinatorial logic using LC's rewriting rules (e.g. beta reduction).

[@hasanrazza1]

@@glebec MashaAllah, prof. Lebec! This explanation was amazing and clear. Thank you once again for taking out the time for it :)

[@rohanrameshraikar567]

Amazing! U r amazing!

[@dierkkoenig]

cool talk! I wonder wether pow=CI could actually be interesting since CI is also not(id) and thus pow=not(id). This might bear connection to x^0=1 (with "not" being 0 and "id" being 1).

[@CarterColeisInfamous]

Im implementing this in my stack machine

[@CarterColeisInfamous]

this is a little harder than i thought... like the beta reduction part

[@glebec]

@@CarterColeisInfamous the talk introduces the concept of beta reduction, but I gloss over some of the tricky formal rules, like how to properly avoid conflating two independent variables with the same name. Implementing lambda calculus evaluators is a good exercise though! I wrote one in Haskell using De Bruijn indices, and I found it pretty challenging but very rewarding. Hope you are having good luck with yours!

[@ryderpham5464]

Does anyone know what these slides were made in? I love the look!

[@glebec]

Slides were made in Keynote. :-)

[@rohanrameshraikar567]

Have u made video on partial functions in lambda calculus.

[@glebec]

I have not, but it's an interesting topic, partly because it depends on some subtleties of how you define "partial" in the context of lambdas / lambda calculus. For example, mathematicians sometimes consider an infinite loop like "M M" to be a value named "bottom" (symbolized via "⊥") and name a partial function as any that "returns ⊥" (e.g. evaluates to an infinite loop).

[@waltermelo1033]

MORE VIDEOOOOOS PLEAAAAAAAAASE!!!!!

[@glebec]

What would you like to see?

[@Yetipfote]

@@glebec other data structures: how would you describe Floats (rational numbers) and Strings, how recursive data structures like a hashmap?

[@glebec]

​@@Yetipfote Those could definitely make for some nice continuing videos. :-) In the meantime, I can also give some short answers. ¶ In this vid I talked about how to represent Natural numbers (0+) and pairs as functions. ¶ Integers (±) can be represented as a pair of (Bool, Nat) where the Bool indicates sign. ¶ Rationals can be represented as a pair of Integers (numerator and denominator). E.g. (1, 2) = 0.5, and (-1, 3) = -0.333…. ¶ If you nest pairs, you get a list: (a, (b, (c, (d, e)))). As a syntax shorthand, you can represent this using [a, b, c, d, e]. IEEE754 Floats can then be represented as a fixed-length list of bits (i.e. bools) if you wanted - a 1:1 mapping with the spec. ¶ You can also represent characters using numbers (e.g. 65 = A, 66 = B), and a String can then be a list of characters, e.g. [65, 65, 65] = "AAA". ¶ For heterogenous data structures with "runtime" (eval-time) type-checking/dispatch, you can couple every value in a pair with a Nat representing its type. So if 0 = Bool, 1 = Nat, 2 = String etc., then if you traverse the two-element list [(0, x), (2, y)] you know what functions to use on x (bool funcs, e.g. Not) and y (string funcs). ¶ Now that you have a form of type encoding, you can define a heterogenous associative list as a list of pairs of string keys and any-type values: [("name", "Einstein"), ("age", 50)] (where "Einstein" and 50 are actually pairs of type-flag and value, e.g. (2, "Einstein") and (1, 50)). Some of your values can themselves be association lists, so you have a recursive structure. ¶ Now mind you an association list implements the Map abstract data type, but not with the performance of an actual hashing-based data structure. This gets back to one of the conclusions of the talk: lambda calc can compute anything computable (e.g. a Map ADT), but the *implementation* may be very different (e.g. a Hash Table data structure vs. an Association List data structure). ¶ Indeed, the mathematical system we are building, based on extremely inefficient Church encodings for numbers, would be horrible for real-world tasks. So real functional languages give you all the capabilities of a lambda calc (first-class functions, currying, composition, purity, etc.) but also take advantage of normal, hardware-level mutation and state under the hood (e.g. IEEE754 floating point calculations). ¶ The trick with FP is that we write our programs in a language that is only concerned with the pure mathematical concepts, but the compiler is allowed to (indeed, must) "cheat" and deal with the messy, mutating Turing machine that is a physical computer. So long as the compiler is written well, we can trust it to handle that stuff for us (e.g. garbage collection) - and indeed, since our *language* is nicely mathematical, pure, and (in many cases) typed, it makes it easier for the compiler to statically analyze and optimize our code. ¶ Finally, I will mention that _some_ data structures can actually be *more* efficient in an FP setting. If you know that data will never be mutated, it can be safely shared / nested inside of other data structures, resulting in less memory duplication. Chris Okasaki wrote a thesis, and then book, called Purely Functional Data Structures which is a major work in this area.

[@Yetipfote]

@@glebec 😍 is there a machine which is better suited for functional programming than a touring machine? Is there an actual hardware implementation of such a machine?

[@tomislavhoman4338]

@@Yetipfote Yup, that's what I'm thinking about too. Did we make a mistake going with Turing machine based machines decades ago, like we chose gasoline cars instead of electric ones hundred years ago and no we have to do painful transition :)

[@JethroYSCao]

Amazing talk. Mine blown.

[@gm2407]

How do we do negative numbers? Not subtraction but pre 0.

[@glebec]

By the end of the video we have shown a way to create pairs of values / 2-tuples (the Vireo combinator). We can model signed integers by extending the natural numbers using a pair of (Bool, Nat) where the bool indicates sign (e.g. True = positive, False = negative). Then we have to write new functions which handle arithmetic on these pairs, e.g. addition of two numbers checks both numbers' sign values and adjusts to use addition or subtraction respectively. Crossing zero is a bit awkward but we can make our functions do an inequality check first and then flip arguments around to yield the correct result, adjusting the sign at the end. This is just one (gnarly) approach to the whole thing; I am sure there are alternative formulations. But the point isn't how elegant (or not) the mechanics are, as we don't usually perform mathematical computations using pure LC in real programs; instead we defer to the hardware math processors (e.g. IEEE 754 Floating Point calculation). The point is that it is _possible_ to perform such computations. That is of interest mathematically even if it is not necessarily useful in all real-world computer programs.

[@gm2407]

@@glebec Thank you. Other than these two videos, are there other videos you have done on LC? I find it very interesting. Just rewatched the first video taking many notes.

[@glebec]

@@gm2407 No other videos that I've done on LC, no (apart from the same talk at other venues). But thanks for your interest.

[@jameswillett5484]

this video needed `churchnum = n => n === 0 ? KI : B(succ)(churchnum)(n - 1)`

[@v_donets]

Cheers Mr Lebec! My team have been working on an modifying Reduction Strategies, applying some reduction extensions and we got stack in the idea of existing an optimal strategy, with which we would be able to compare our strategy. Is it exist any works or do you have any ideas about a fact that there are no optimal Reduction Strategy? Thanks for your attention! Sincerely, V. Donets.

[@justind6983]

Christ, be my teacher! Can you make some content I can purchase? Udemy.com preferred. I soooo want to did into Clojure but it is very intimidating. I also order to mock a mockingbird and am taking your videoes a few minutes at a time to understand them myself. Thanks so much again!

[@glebec]

Hah, thanks for the enthusiasm. If I ever put up any content on such a platform, I'm sure I'll make an announcement. In the meantime I have a few articles up on Medium (medium.com/@glebec) which may interest you if you know JavaScript… though I would enjoy making something more functional, e.g. for Elm or Haskell. One of my friends' first programming languages was Clojure, it looks interesting but my backlog of languages to learn is unfortunately a bit too deep for me to promise anything!

[@gm2407]

In pascal can you build functions from all other languages using only lambda calculus?

[@glebec]

I don't know Pascal; in this talk I mention Haskell (which sounds a bit like Pascal) a few times. Is that what you are referring to? As to whether you can use LC in Haskell to build anything possible in other languages: this depends quite a bit on what is meant *precisely* by "build functions from all other languages." Haskell is a Turing-complete language, so it can certainly _compute_ anything any other programming language can compute. Can you use lambda calculus _specifically_ to do so? Well, Haskell is not 100% the same as the simple untyped lambda calculus; it is actually based on a variation of lambda calculus called System FC, which adds types and some other thing(s). In fact this means that Haskell cannot always do the same thing as simple LC; for example, you cannot easily define the Mockingbird combinator`M f = f f` (or `\f . f f` to use LC syntax) in Haskell. This is fine though because again, Haskell _itself_, being Turing-complete (TC), can still do whatever _task_ you could conceivably want it to do. Haskell is a general-purpose language and it's used in web servers, compilers, command-line interfaces, all sorts of applications. Another point here is that sometimes, a "function" from another language effectively is not a function in the mathematical sense, which is what a lambda from lambda calc is; that is, what some languages call "functions" are really procedures or subroutines which cause side effects. You cannot "implement" `System.PrintLn` or whatever using lambda calculus because LC has no concept of a hardware computer with an operating system that communicates on I/O channels by sending electrical signals etc. But you can _model_ such a system as data, and compute things you want to do with it, and hand off those pure results to a runtime (like Haskell's runtime) which is hard-coded to ingest such models and do actual IO. I hope this begins to answer your very broad question!

[@gm2407]

@@glebec Thanks. I don't know Pascal either. It was just a language I heard does LC (in a video by another youtuber before I looked at this video). I appreciate the answer you gave to my question. So LC compliant languages (in that they are "Turing complete" can write a "think tank paper" about the function but must hand it off to the "executor of the writ" which will take the theory as if it is a command and enact it as such. This is because the execution program has already been written using non LC programing to interact as such.

[@Hvan101]

What is the repl u use?

[@glebec]

It's the floating window option in iTerm. You can create a keyboard shortcut which opens a shell session above your current app. I was just in the Node repl in order to execute JavaScript.

[@MrRyanroberson1]

15:00 i had an idea: G = lambda f, g, x: f x (g x) # i remember a function that works like this, i think it was G B = lambda f, g, x: f (g x) # the B you defined SUCC = lambda n, f, a: f (n f a) # your successor SUCC = lambda n f a: n f (f a) # this is equivalent SUCC = lambda n, f: B (n f) f # the B you mentioned SUCC = lambda n, f: flip B f (n f) # flipping it... SUCC = lambda n, f: G (flip B) n f # oh wow! SUCC = G (flip B) # it's a COMBINATOR!

[@MrRyanroberson1]

A = I* ADD = lambda f, g: f SUCC g ADD = lambda f: f SUCC # g can be implicit ADD = lambda f: A f SUCC ADD = lambda f: flip A SUCC f ADD = flip A SUCC # wow! another combinator (since SUCC and A are combinators) ADD = flip (I*) (G (flip B))

[@MrRyanroberson1]

26:00 IS0 = lambda f: B (B f (K KI)) K FB = flip B IS0 = lambda f: FB K (FB (K KI) f) IS0 = lambda f: (FB K) . FB (K KI) f IS0 = (FB K) . FB (K KI) another combinator. incredible.

[@jameswillett5484]

these 2 videos (this one in particular) made me buy to mock a mockingbird

[@chuanqisun]

warning, this brilliant talk is brain halting.

[@brod515]

14:40. where did the `a` go. won't the `B f (nf)` combinator reduce down to f(nf). doesn't that mean it will call f with nf as a param . but that won't give you the same as calling f with nf(a)? doesn't f expect the result of calling nf with a not nf itself? I'm confused about that section.

[@glebec]

Hi! The expression `B f (n f)` reduces to `λ a . f (n f a)`, not to `f (n f)`. The B combinator takes two functions and produces a *new* function which passes its argument into a pipeline of the original functions. B can be defined as: `λ g h a . g (h a)`. If you apply `B f (n f)`, then `g = f` and `h = n f`, so `g (h a)` is `f (n f a)`. Does this help you understand that section? Let me know if you would like more clarification. Here is a step-by-step demonstration of reducing `B f (n f)`: B f (n f) = (λ g h a . g (h a)) f (n f) # by definition of B = (λ h a . f (h a)) (n f) # by beta-reduction, binding `f` to `g` = (λ a . f (n f a)) # by beta-reduction, binding `n f` to `h`

[@brod515]

​@@glebec Hey thanks for replying I've just read my question I'm not really sure why I asked that 😀. while looking at that part of the video right now I clearly understand it. I'm not sure what I was talking about when I say f(nf). it clearly returns a function that takes a and returns f(n f(a)). 😂 sorry to have wasted your time but thank you for your clear explanation It makes perfect sense. I decided I was going to read a book you recommended in one of this comments because I want to read chapter 4 about the recursion I think that would be very interesting there is a section there about binding and free variables that I'm still trying very hard to understand. the book goes into a bit of detail trying to explain the terminologies more explicitely. the successor combinator is also implemented slightly differently but I guess there is many ways to implement this things. Thank you EDIT: I think I was initially confused because I was looking at it directly how I would look at code so looking at f(nf) made me automatically think a function call was happening.

[@glebec]

​@@brod515 No worries, always happy to help and I'm glad you already understand it. :-) As to things being implemented different ways, that's definitely true! For instance, natural numbers can be implemented via Church numerals like in this talk, but there are also Scott numerals and even "BinaryScott" as I have recently learned - the latter is essentially a list of bits, and can do fast enough arithmetic to be used in nontrivial programs! (Though you still wouldn't use pure LC for math in the real world.)

[@please.stop.coping]

# e = mc² M:= λf.ff E:= λmc.M(mc) Do you recommend i use an abstraction of MULT (and POW/TH) instead of mc.mc? Ex. MULT:= λnk.Bnk or B E:= λnk.M(MULTnk) Even less confusing: TH:= λnk.kn E:= λnk.TH MULTnk N2 Since if Lambda has to be transpiled to computer languages then they can substitute these (whatever it is called) to "shortcuts" that doesn't use church encoding. Or do we just have to get used to reading it that way? I feel like I'm moving away from Lambda in those last examples.

[@glebec]

Hi. Let's start by making sure we agree on what the goal is here. There are two different ways I could understand your using `e = m * c^2` here: - either you are trying to express a function that, for some `m` and `c`, computes `m * c^2`; OR, - you are trying to express the _equality_ `e = m * c^2`, for some `e`, `m`, and `c`, and test that the equality relation `=` holds true for those three values. I would avoid saying that `E` is a function on `m` and `c`, which is what it looks a bit like you are doing, if only because that is not quite what `e = m*c^2` usually means in the realm of physics (although of course it is "legal" to define such a function). OK, so let's assume you are trying to compute `m * c^2` for some `m` and `c` values. The way I would do that using the Church encodings / functions presented in the talk would be like this: f := λmc.MULT m (POW c N2) But there are certainly many other ways we could write this, including expanding the definitions or re-using `MULT`. Some of the ones you propose don't look correct to me however: E:= λmc.M (m c) = λmc.(m c)(m c) -- when m and c are Church numerals, `m c f x` does `m` applications of `c`-fold application to f to x; for example, if `m = N2` and `c = N3`, then this will do (twice thrice) f x which is (thrice (thrice f) x) or 3^2 = 9 applications of f to x. SO, `(m c) = POW c m`, and `(m c) (m c) = POW (POW c m) (POW c m)`; or in usual algebraic terms, we might write that this equals (c^m)^(c^m). Whatever that is, it most likely isn't (m*c^2). I think the main error I see in that attempt and some of your others is forgetting that in lambda calc, function juxtaposition is function application, and for church numerals, that means exponentiation, not multiplication (or composition). Therefore, I do recommend that you express numerical operations using predefined abstractions like MULT, POW, etc. if only to make it harder to make mistakes. > "Since if Lambda has to be transpiled to computer languages then they can substitute these (whatever it is called) to "shortcuts" that doesn't use church encoding. Or do we just have to get used to reading it that way? I feel like I'm moving away from Lambda in those last examples." Yes, a lot of this talk moves away from the pure lambda calculus into a language which transpiles to LC. And in real functional programming languages, they don't ONLY do pure LC, but rather some things (like `2 * 3.5`) use IEEE 754 Floating Point operations on hardware, not actual lambda calc. So FP languages like Haskell, Elm, PureScript etc. are a mix of lambda calculus and traditional operating system calls / CPU instructions. For example, in the Haskell value `f = \a -> a * 2`, f is a lambda that takes a param `a` and evaluates to the expression `a * 2`; however, the `* 2` part is itself no longer lambda calculus, but now traditional computer math. The core of Haskell is a lambda calculus, but some of the terms embedded *in* that lambda calculus are not pure LC. But if we did stick with only LC, you could write a language that uses definitions like `MULT` and `POW` and the transpiler would first substitute all those occurrences with their original lambda calc definitions. A key "gotcha" however is that if you use this shorthand / notation idea, you are NOT allowed to use recursive bindings via names. MULT := λnmx.n(m x) -- this is legal FACTORIAL := λn.IF (EQ n N0) THEN (N1) ELSE (MULT n (FACTORIAL (DEC n))) -- illegal recursion via the name `FACTORIAL`! Why? Because a naive transpiler, replacing our named shorthand with anonymous lambda functions, would infinitely expand the recursive FACTORIAL definition with itself, resulting in nonterminating compilation (infinite loop of substitution). How do we deal with this? The answer is a very clever, and very confusing, lambda function called the Y combinator. The Y combinator is capable of taking a lambda which is "almost" recursive, and "wiring it up" to become recursive, all without using names! With the Y combinator, we can then define a syntax shorthand `LET REC` which lets us define recursive functions using names, which our hypothetical transpiler would convert into a finitely-long Y-combinator version that doesn't use names. How it does that is incredibly difficult to explain, certainly beyond a KZbin comment, but it is really amazing.

[@krumpy8259]

I’m a bit confused with the notion of taking in a pair of numbers and return a function e.g the sum of the pair. Is a pair a function to? What is the arrow representation? A ->B -> C

[@glebec]

Hi! I am not 100% sure which part of the talk you are referring to. Is it the addition function, the Pair (aka Vireo) combinator, or the Phi combinator?

[@krumpy8259]

@@glebec I try to explain by an example, here is a code snippet: add :: Integer -> Integer -> Integer add x y = x + y So if I'd run this code for add 2 5 the answer would be 7. But my problem is the expression ' add :: Integer -> Integer -> Integer '. To me this seems to be a composition of 2 functions, but if I'm not mistaken it is just one function that takes in 2 arguments. And here is the confusion I have not being able to tell that a pair could be understood as a function or not. Sometimes in textbooks you can see the expression G x G -> G and I'm curious if it could be G -> G -> G if a pair is just a function, too or is it? Thanks

[@glebec]

​@@krumpy8259 did you watch Part I of the talk (on the Fullstack Academy channel)? This is a technique called "currying" and I go over it in that other video, which is meant to be watched before this one. To review, currying is when we write an n-ary function (e.g. 2-ary, taking a pair) as n unary functions (e.g. 2 single-argument functions). So, instead of taking a pair of numbers and returning a number: add :: (Int, Int) -> Int …we take a single number, and return a function: add :: Int -> (Int -> Int) The returned function (Int -> Int) _also_ takes a single number, so if we call it with another int, we get a final result. This means we can add two numbers by first applying `add`, and then applying the returned function, in quick succession: (add 1) 2 -- returns 3 But we can also *not* apply the returned function, and just save it for later: (add 1) -- a function which adds 1 to things, but we haven't called it yet Currying makes functions more flexible as we don't have to supply all of our arguments at once. We can instead supply some arguments, and get back a function waiting for more arguments. For convenience, we make the type arrow `->` right-associative, so these are identical: add :: Int -> (Int -> Int) add :: Int -> Int -> Int And also for convenience, we make function application left-associative, so these are identical: (add 3) 2 add 3 2 We can also scale this up to 3-ary or 4-ary functions, for example the type `someFunc :: (A, B, C) -> D` becomes the type `someFunc :: A -> B -> C -> D`, or with parens, `someFunc :: A -> (B -> (C -> D))`. When functions are curried, you can still call them with "all" of their arguments, e.g. `someFunc a b c` returns a value `d`; or you can call them with just some args, e.g. `someFunc a` returns a new function with type `B -> C -> D`, or `someFunc a b` returns a new function of type `C -> D`. To answer your question a little more directly: a function that takes a pair of arguments and returns a result `(A, B) -> C` is **isomorphic** to a curried function `A -> B -> C`. Isomorphism qualitatively means that you can transform the first function to the second, and the second back to the first, with no loss of information. They are equivalent in a deep mathematical sense, even if you use them in slightly different ways (in programming terms, their API isn't identical). Rewriting a function which takes a pair as a curried function is called "currying"; rewriting a curried function as a function which takes a pair is called "uncurrying". I recommend you watch the first video for more clarity on this. There are also ways of _encoding_ the idea of pairs (2-tuples, a data structure) as functions, which I show in *this* video, but that is a separate topic.

[@krumpy8259]

@@glebec Thank you very much!

[@timonpasslick]

What's jsnum(pred(n0))?

[@glebec]

Timon Paßlick - it is 0. In this definition I show natural numbers. Using the Church Pair data structure, since we seed the pred function with the pair (0, 0), the “predecessor” of zero is zero. There are of course more complex ways to build up integers including negative integers, rational numbers, etc. - mostly using Church Pairs to encode the numerator and denominator, sign, etc.

[@timonpasslick]

Ok. And you said that Haskell doesn't use function numbers but int, float etc or did I get you wrong?

[@glebec]

Timon Paßlick Correct. Church numbers are interesting from a logical perspective but would be terribly inefficient on real hardware. The Haskell compiler “cheats” and gives you access to types Integer, Float, etc. with typical imperative (machine-based) implementations, for performance reasons.

[@timonpasslick]

But I could define church numbers in Haskell?

[@glebec]

Timon Paßlick Yep! Also, you can define Peano numbers using Haskell’s type system quite easily: `data PeanoNum = Zero | Succ PeanoNum`. With a bit more code to handle conversion to Integers, logging to the console, etc., this is a common introductory exercise to Haskell’s very nice type system.

[@Ancipital_]

I sadly had no maths when growing up, my school history is far from normal. Wish i could say I get it, and I feel I almost do, just not fully yet. Anyone else running into this? I want to learn Haskell but for that I want a better handle on lambda calculus first.

[@glebec]

@Nulnulzich you don't need to fully get all the encodings and Turing-complete computational tricks of lambda calculus to start understanding Haskell. Do you understand the basics (applying a function to an argument, substituting the value in the function body; currying; and functions as values)? That is all you really need for Haskell per se. Haskell doesn't use Church encodings for booleans and numbers, for example - it has ordinary built-in number types and bools are just a simple data construct. Some more advanced tricks in Haskell rely on concepts seen in lambda calculus (e.g. fixpoint combinators), but I don't even really cover those here.

[@AfterThisShutUp]

It feels like we're cheating when defining the jsnum function at 8:21. Why are we allowed to use addition in that lambda if we haven't even defined the addition operator yet?

[@glebec]

Hi there. If you watch carefully you will notice that we never use `jsnum` in our LC code, we only use it at the end of some LC code as a convenience to print the JS equivalent number to the console. A Church Numeral is a function; we could print it to the console (which would show up as "" or something like that) but to prove to the audience that we made the *right* function (one which represents the number we expected), we need to convert it to an IEEE 754 Number. We don't need or use `jsnum` for any other purpose except the presentation / talk, to convert out final result for display purposes only.

[@AfterThisShutUp]

@@glebec Thanks for the response. Yeah, I came to that same realization after some time. While you're here, are you planning on making a Part 3 of this? Or delving into more functional programming (for example, how category theory is used in programming)?

[@glebec]

@@AfterThisShutUp I wasn't planning on a part 3 - if you want more examples of LC can keep building to produce an entire language (albeit not a performant one, just as a mathematical demonstration), I recommend Greg Michaelson's "An Introduction to Functional Programming Through Lambda Calculus." People have asked for more content in general including something on CT, so you never know if and when I will put up more videos, but mostly I have scattered blog posts on various platforms (dev.to, Medium, etc.). My job also keeps me much busier these days. Never say never though!

[@tricky778]

why do you define pred such that pred n0 == n0 instead of pred n0 == omega ? I imagine that either (B succ pred) n0 == n0 or it == omega, but never would (B succ pred) n0 = n1

[@glebec]

`omega` as in `M M`? I haven't worked through all of the possible ramifications of alternative definitions for `pred`, so one honest answer is that this is a common (and relatively easy to implement) first approach to define a sensible algebra on natural numbers. In other words, I simply didn't think about alternative `pred` formulations. More concretely, however, in a strict programming language the `M M` combinator (`Omega`) doesn't terminate. That means we cannot use it e.g. for testing equality, which is how we implement the inequality `a

[@tricky778]

yes, I meant (M M), the fact it doesn't terminate is what I thought would make it correct - because it is never extensionally equal to anything so, being that in reality there's no predecessor of zero in the set of counting-numbers-with-zero, it's never wrong.

[@tricky778]

you can use a "maybepred" to implement

[@glebec]

Gotcha. Yes, using Omega as the pred of 0 in the Naturals is beautiful from a theoretical / semantics perspective - corresponding to the value "bottom" in Haskell. I suppose that operations (like `

[@tricky778]

I'm sure you can do it with pairs of an encoding of Nothing and Just, and with the bare lambda calculus, the map and extract would be trivial and pretty intuitive, and a case analysis so we can avoid omega during extract - in fact I think the case analysis is the monad bind for maybe in the bare lambda calculus isn't it? so it must definitely work easily.

[@aMulliganStew]

So far I’ve been running at consistently lower abstraction levels. I’m still able to come up with valid answers (thank God for that), but they’re no where near a nice as the ones presented. Hopefully with time, patience, and more than a little bit of practice...

[@glebec]

Keep in mind - most of what I show here is what other people discovered or invented over the course of decades. And all of this is material which I edited and revised and re-wrote over the course of multiple drafts, in multiple formats. The finished product you see in this presentation is a cheat; it's what happens when you're allowed to work on something for a long time and hone it to the point where it looks easy (I hope). But it wasn't! It took a lot of practice, and thinking, and mistakes, to get there. If there is something in this presentation that I hope is original, it is the way the information is illustrated and explained; it's what I wish someone had shown me when I was puzzling through whitepapers, wiki pages, and textbook chapters. Now it makes a lot of sense to me, but I remember when it didn't, and I have nothing but sympathy for anyone in the earlier stages of this journey. Or the middle stages! Cheers, -G.

[@hexa3389]

You could've just used scheme. Its syntax is less well known but it's much more similar to lambda notation

[@glebec]

Of course! But my audience was a group of JS students. :-)

[@hexa3389]

@@glebec ah. That makes more sense. Thanks for responding!

[@oleksandrkozlov4195]

How is it possible that SUCC(ZERO)(NOT)(TRUE) is FALSE if following implementation of SUCC from the video it unfolds into NOT(ZERO(NOT)(TRUE)) which is basically TWICE(NOT)(TRUE)? Also, jsnum(ZERO) is 1 and not actually 0. Is it intended to be that way? Can't get my head around it.

[@glebec]

The short answer is that `NOT (ZERO NOT TRUE)` is `NOT (TRUE)` which is `FALSE`. It's not the same as `TWICE NOT TRUE`. Full explanation: ------ SUCC = λ n . λ f x . f (n f x) ZERO = λ f x . x SUCC ZERO NOT TRUE = (SUCC ZERO) NOT TRUE = (λ f x . f (ZERO f x)) NOT TRUE = (λ x . NOT (ZERO NOT x)) TRUE = NOT (ZERO NOT TRUE) = NOT ((λ f x . x) NOT TRUE) = NOT ((λ x . x) TRUE) = NOT (TRUE) = FALSE Or if you prefer: SUCC ZERO NOT TRUE = (SUCC ZERO) NOT TRUE = (λ f x . f (ZERO f x)) NOT TRUE = (λ f x . f x) NOT TRUE = (λ x . NOT x) TRUE = NOT TRUE = FALSE

[@glebec]

As to your question "Also, jsnum(ZERO) is 1 and not actually 0", this isn't accurate, `jsnum(ZERO)` is indeed 0, not 1: jsnum = n => n(x => x + 1)(0) jsnum(ZERO) = ZERO (x => x + 1) (0) = 0

[@asitisj]

Isn't 0 here just the fixed point? It's literally fa -> a

[@glebec]

ZERO = λ f x . x ID = λ x . x ID treats all inputs as a fixed point. ZERO doesn't - it ignores its first argument (`f`) and returns ID.

[@Yetipfote]

38:37 could you... just go on and on pls? ._.

[@matthewpeterson5159]

Nice intro to Lambda Calculus talk. Not to be that guy, but, well, the keyboard noises are pretty bad lol. But still, good talk.

[@glebec]

Thanks for the comment. The recording for Part II was done impromptu on my machine directly, so the keyboard does sound pretty excessive. Hopefully it didn't distract too much from the content!

[@matthewpeterson5159]

Eh, it was somewhat distracting but it was still a good talk! :)

[@sluchaynayakotya1386]

sadly the zero becomes false only because we arbitrarily decided to put false in the second position at the definition of if statement.

[@kungfooman]

>writes the wrong bluebird definition >blames it on javascript (fp devs in a nutshell)

[@glebec]

JavaScript is to be blamed for all of my errors, including errors in other programming languages, as well as life in general. 😉 /s (In all seriousness, the reason I said "Oh JavaScript" was because it allows me to create a function with an unbound variable reference, which would immediately crash in e.g. Haskell, but is allowed in JS due to bindings being resolved at runtime - allowing the possibility of definitions being added into the global scope after the fact.)

[@lucasa8710]

this is very nice but I have to admit, memorize bird names is pretty boring

[@glebec]

When I was designing the talk, I had to figure out what my goals were, and this issue definitely presented a challenge. The talk would absolutely be easier to follow if I only used JS arrow functions and didn't even show lambda calculus syntax, historical combinator names, or Smullyan's bird names. So I was tempted to follow that "distillation" approach, which would focus on just the core ideas. At the end of the day however, I decided I wanted this talk to be an introduction not only to the programmatic side of things, but also the complex, multifaceted historical context which gave us many different names for the same entities. I hoped that viewers would leave the talk not necessarily remembering every name, but at least not being intimidated when they see a comment on some forum talking about "the C combinator" or "the mockingbird" or "\x y -> x". That the same viewers would be able to think "oh yeah, that's the name for a function, I know how to look this up / read this / figure out what this means." That does make the talk longer and more challenging, but on the positive side, I hope that it has demystified some of the topic for people, allowing them to recognize that these are all just different ways of talking about the same core functions. :-)

[@lucasa8710]

@@glebec absotulety, it was really great, I just have problems to keep tracking of what all names means, but I learned things that I'd never known before, Good Job 👍