Programming with Math | The Lambda Calculus

[@vivada2667]

This video is super good. Multiple times throughout the video, I was like "ok this does not make any sense" and then immediately after saying that, you said "That seems confusing. Let's look at an example."

[@Eyesomorphic]

That's very reassuring, I'm glad you enjoyed it :)

[@eth3792]

The phrase "we know it's correct because it type checks" has blown my mind. I must learn more about Curry-Howard correspondence now

[@tylerfusco7495]

if you want to go really far into it, look into languages with this taken to the logical extreme, like Lean4. people have written a huge amount of math as code, and *the fact that it type checks* means that all of those proofs are correct.

[@warmooze]

Absolutely insane

[@MrSamwise25]

Just a warning: the treatments I've seen of the CH correspondence (e.g. Girard's Proofs and Types) have either been frustrating in key technical points or too vague to get a deep understanding. This isn't to dissuade you, but to reassure you that it isn't you, it's the text.

[@MrSamwise25]

What's your favorite first-order logic system? Mine is Fitch-style proofs, and I found it easier to just go through the correspondence myself with that system.

[@jawad9757]

wait until you hear about dependently typed programming languages

[@AnOldGreyDog]

One of the things I took away from reading _Gödel, Escher, Bach_ (mumble, mumble) years ago was that computer languages don't differ in their _ability_ only in their _expressiveness_ . In other words, any language (of at least λ-calculus complexity) can do what any other language can. It's just easier to express in some.

[@anywallsocket]

Yeah cuz λ calc is Turing complete, so it’s complexity is sufficient to simulate any normal computation, including the simulation of any other computer.

[@writerightmathnation9481]

Complexity is not the same as effectiveness. Some languages are faster because of their expressiveness, and others are slower because of the design of their use of their expressive power.

[@anywallsocket]

@@writerightmathnation9481 i believe that was OP's point, you just said it differently. no one is saying complexity == effectiveness

[@SL3DApps]

This isn’t true. A language ability is highly different when used for certain areas in computing. However, If you’re only interested in making simple programs then you won’t ever have to worry.

[@cinderwolf32]

​@@SL3DApps things like I/O, direct memory access, network access, etc don't count here. This video, and the comment you're replying to, are about computation, not making programs and apps. Computation does not care about these things, and studying it takes place in an imaginary world with infinite memory and infinite time. In that case, Scratch and C are equivalent. If you're seriously unconvinced, consider that someone has successfully emulated a RISC machine in Scratch and used it to boot Linux all within the project.

[@yaksher]

@2:30 I like how this presented as some sort of obvious improvement over writing an arrow even though it's more visual noise and more characters.

[@Anonymous-df8it]

I wonder what the programming language would look like if the arrow was preserved

[@yaksher]

@@Anonymous-df8it This is what languages like Ocaml do.

[@ScottHess]

In a regular computer system, using . is a lot easier than using an arrow. Of course, the notation also added lambda at that point, so no gains had…

[@yaksher]

@@ScottHess Yeah, I mean, you can do that, but somehow virtually no language does, probably because it's much worse for legibility. Even haskell which does use a \ or lambda then uses an arrow, though you're right that it's less convenient to type than a dot. I think in practice, Rust's solution of using |args| is one of the better ones in terms of typing ergonomics

[@darqed]

as someone who loves both maths and programming, this is probably my favourite math video I've ever seen

[@sadsongs7731]

I mean, to claim that Lambda calculus can replace any programming language is like saying assembly can replace any programming language. True in theory but GOOD LUCK trying to get anywhere.

[@tylerfusco7495]

@@sadsongs7731 i mean, thats literally what functional programming languages are. Lisp, Haskell, OCaML, Lean, Clojure, etc. Are all pretty widely used, and are literally built on top of nothing but lambda calculus (but in practice are optimized or compiled to speed up evaluation).

[@sadsongs7731]

@@tylerfusco7495 Those languages offer far more conveniences than what lambda calculus notation provides. They may be "built on top of" but they are not just lambda calculus. That was my point with assembly. You technically don't need anything else, but it's a pain in the behind to write compared to a higher level programming language. These languages offer abstractions that take time to learn and, sure, would be better if you didn't have to learn them but they are there because raw lambda, like raw assembly, is not user friendly.

[@tylerfusco7495]

@@sadsongs7731 well yeah, nobody is advocating for lambda calculus being the actual thing you program in. that's like thinking a video outlining how assembly language works is advocating for assembly language to replace higher level languages. that's not the point, the point is that the higher level abstractions can all be built on top of and formalized using the lower level ones.

[@Darkon10199]

if you love both math and cs i really recommend type theory. it's the math field that studies this stuff, lambda calculus is the starting point, but it's some of the most beautiful and groundbraking math i've ever studied

[@AndresFirte]

This video is amazing! I encourage everyone to watch the video, and then grab a pen and paper and rewatch the video, trying to get ahead of what is being shown. I tried that and realized that I hadn’t actually understood many of the things in the video, like the notation. Videos like these are so well explained that you often feel like you understood everything. But then when you grab pen and paper you realize that there’s many details that you missed. And by the end of it, you feel like you truly understood 90% of it

[@alicagank]

I’m a linguist, not particularly mathematically inclined, and honestly, I can’t believe I understood half of it. Incredibly simple yet intuitive. I love the visuals too! Please keep up the good work! :))

[@kikivoorburg]

Some linguists have rigorously encoded linguistics using type theory! It’s well beyond my level of understanding, but some information can be found on Wikipedia

[@voltydequa845]

@@kikivoorburg If it was so we would have today real (symbolic logic) AI instead of the hyped trickstery that is presenting the gpt/llm stochastic parrot, or, better, the technique of "pattern matching on steroids"(© Torvalds), as AI. Language understanding (understanding implies inferences, so no llm) is all about domain, context and cognitive representation. Though types (domain & context) can help, encoding the cognitive representation is prohibitive seen the complexity (if we were that intelligent, we would have implemented the industrial revolution as soon as we got down from the trees).

[@cube2fox]

Simply typed lambda calculus is actually used in formal semantics, which is a branch of linguistics.

[@carmensavu5122]

@@cube2fox Yea, but I don't think it works.

[@tjperkins2323]

Great timing! I've always wanted to share this with my friends but I find it extremely hard to explain. It's nice that you made it accessible to others without much experience in math.

[@Eyesomorphic]

Glad it was helpful!

[@scroipt]

Though this really is more of a "hey this seems to work out" kind of proof than a particularly rigorous one.

[@little-ork]

halfway through the video I suddenly understood Haskell

[@ckpioo]

💀💀

[@ckpioo]

haskell mentioned

[@peacefulexistence_]

LC does have that effect on people :) ML (the family of languages Haskell is a part of) derives from LC.

[@rogergalindo7318]

now you have to follow the prophecy and become a haskell wizard!

[@pascalcharbonneau9019]

I have been trying really hard to learn functional programming without learning Haskell and this video gave me hope haha.

[@chrisray9653]

This reminds me of that MIT video from '86 talking about the eval / apply loop at the core of Lisp. "MIT Structure and Interpretation of Computer Programs" "Scheme / Lisp"

[@dw3yn693]

you've got a link?

[@jackren295]

@@dw3yn693 I think it's this series, which is a classic: kzbin.info/www/bejne/Y3vCqX9qfqybgKM

[@chrisray9653]

@@dw3yn693 It's called Structure and Interpretation of Computer Programs (SICP MIT by Abelson and Sussman)

[@nythrox3047]

What's the name

[@mikemilner8080]

@@dw3yn693 Try a Google search of the MIT OpenCourseWare web site. The Wizzard book (Structure and Interpretation of Computer Programs) gets its name from the MIT course 6.001's title. I took 6.001 way back in 1969 - at that time the course used PAL (Pedagogical Algorithmic Language), a syntacically sugared version of Curried Lamba Calculus. Having only be previously exposed to procedural languages, the power of functional languages was a revelation.

[@gerocastano8]

As a computer science student that studied functional programming and mathematics, I absolutely love this video. Please keep going!

[@Dhiren_]

This is the best video I've seen on understanding how lambda calculus relates to logic, at the low-level! Thank you!

[@Eyesomorphic]

How kind :D

[@codeguru5024]

7:30 "This method...is named currying after the magician Haskell Curry." I'm sure advanced mathematics seems to be magic to some people.

[@houstonbova3136]

I thought he said Logician.

[@maximumhamster]

I heard the same thing, but it was due to listening on 2x speed. When I put it back to the 1x speed I could hear Logician.

[@BonktYT]

get off your high horse

[@angeldude101]

I heard "magician" and I was playing at 1x speed _and_ had captions turned on that said "logician."

[@lemoneer7474]

What’s funny is that this isn’t even the first time I’ve misheard logician as magician.

[@blaz2892]

Lambda Calculus seems like the Functional version of a Turing Machine. Very interesting.

[@Eyesomorphic]

They are computationally equivalent, so you can actually encode a Turing Machine in the lambda calculus, and vice versa! This also means that there is a lambda calculus equivalent of a Universal Turing Machine, so you can build terms in the lambda calculus that act as an interpreter to run terms in the lambda calculus!

[@anywallsocket]

Bro watched the video 😂

[@scottcarothers837]

@@Eyesomorphicwell, yeah, of course they’re equivalent. lamba calculus is turing complete.

[@zTJq40sl]

​@@Eyesomorphic It's even relatively simple: If we encode the variable x as λ a b c . a x the application M N as λ a b c . b [encoding of term M] [encoding of term N] the lambda abstraction λ x . M as λ a b c . c (λ x . [encoding of M]) then an interpreter for the such-encoded lambda terms is "just" E = Y λ e m . m (λ x . x) (λ m n . (e m) (e n)) (λm v . e (m v)) where (as seen at 12:28) Y = λ f . (λ x . f (x x)) (λ x . f (x x)) (I'm using here "λ x y z . M" as a shorthand for "λ x . λ y . λ z . M", as usual once we've seen that we can emulate multi-argument functions by currying.) So yeah, if just looking at these lambda terms, they might seem rather unwieldy. But considering that they implement a fully self-hosting interpreter for a turing-complete language, they are rather tame. (And all the a b c-dot-something stuff is just for marking the encoded terms as (a) variable, (b) application or (c) abstraction, so that the interpreter can handle them accordingly.)

[@BC2300-NewStart]

Yeah, there's this thing called the church Turing thesis thay was only found cuz church and Turing realized that their attempts at defining computability were basically equal fr

[@tessimago9625]

that's nice, now print "hello world"

[@angeldude101]

Hmm... that might be challenging... Would you accept just returning a string containing the characters for "hello world". In typed lambda calculus: "hello world" In untyped lambda calculus: (would need to define cons cells to form a linked list and store in that list the Church-encoded Peano numbers corresponding to the ASCII/Unicode codepoints of each character)

[@AnarchoAmericium]

(λx:String.x)("hello world")

[@gregoryfenn1462]

No, returning a string or data object isn't what the OP wants, they want the program to literally write to our stdout console. It's the most basic task in any new programming language, so how is that done in lamda calculus?

[@angeldude101]

@@gregoryfenn1462 For a more serious answer, one possibility would be to evaluate to a function whose argument is a hypothetical print "function", and then call that "function" with "hello world". Lambda Calculus can perform any _pure_ computation, but it doesn't inherently have any access to any host environment. Technically, if you stripped C of external libraries (including libc) and inline assembly, you would be just as incapable of "printing" to a "screen" as you would be in pure Lambda Calculus. Same as if you tried to write Brainfuck without the . and , commands.

[@nikolaygruychev2504]

consider a "standard library" - your program must be a function, not an application, and it accepts a pair list of all input. it can also emit a pair list itself, to represent the output. funnily, pairs can be used as sort-of-iterators, given that cons = \x. \y. \f. f x y; car = \p. p (\x.\y. x) ; cdr = \p. p (\x.\y. y), then we can have a lazyCons = \x.\f.\g. g x (lazyCons (f x) f) [google y combinator recursion], meaning that lazyCons 1 (\x. x + 1) gives us a list of all natural numbers, i.e. enumFrom 1 in haskell. with this, we can theoretically process any input stream, do computation with it, and emit output partially while the computation is going on much the same way a regular turing machine can. lambda calculus was not intended as proof math can be a programming language, but that machines can do math or something, idk im not a computer scientist

[@andrew_ray]

And if you've ever had the privilege of writing Haskell code, it uses the same kind of type checker using an algorithm developed by Milner and Hindley to prove that your program is 100% type-safe, which actually means that if your code compiles, there's a decent chance it's correct. And if it's not, then your toe definitions aren't robust enough.

[@Zeero3846]

A compiled program is going to be correct, but whether you actually described the problem you intended to solve is an exercise left entirely to you.

[@andrew_ray]

@@Zeero3846 But by making liberal use of newtypes, the compiler can forbid many mistakes. For example, if you define newtypes for Seconds, Minutes, and Hours, the compiler will not let you make the mistake of assigning a number of minutes to a variable that expects to be denominated in hours. Or inches. Or hectopascals. You can avoid forgetting to sanitize inputs by requiring that all rendered strings be wrapped in a SafeString newtype. With the OverloadedStrings directive, string literals within the code don't need to be made safe, but any strings that come from user land do. And if the only way to convert a user land String to a SafeString is through the sanitizer... then you've proven you haven't forgotten to sanitize any user input because your program literally wouldn't typecheck if you had.

[@voltydequa845]

@@Zeero3846 Suggestion: the next time ask the gpt-style commenter to define better, by quantifying, what his «decent chance it's correct» means. He got 32 likes for serving hot-air - a dynamics similar to that of popular tv shows where more simplistic and vague one is, more the public appreciates.

[@throstlewanion]

Absolutely fascinating premise. At first I was a bit confused about the purpose of this language, but now you have opened my eyes to the existence of an entire field dedicated to the study of the theory of programming. Wonderful video!

[@Eyesomorphic]

I'm glad that the video had it's intended effect! Thanks :)

[@Ploofles]

so what your saying is i can write every single python program in one line

[@neutillius]

But It ld be a very long one. Like classical literature sentences for pages.

[@natebrown2805]

exec("print('hello') print('world')")

[@TrusePkay]

Try languages like F# and Scala. You will see how 3 lines of Scala will dwarf 15 lines of Java

[@AkivaB]

You can already do many of them anyways Comprehensions are weird

[@M-F-H]

even without "def" : just a single lambda expression! :)

[@AlLiberali]

Years of fp propaganda from my friends; And it is this video that finally convinces me it is in fact worth the effort

[@Eyesomorphic]

That is quite the compliment, thank you!

[@CTimmerman]

@@Eyesomorphic As a Python fan, I still prefer Python's readability to Lisp and math. AND and NOT gates are more intuitive to me than strange symbol transformations with formulas i never learned.

[@voltydequa845]

No way! This video, although valid, has nothing to do with the (added) value of FP. This video wouldn't have contributed to your appreciation of the FP if you didn't already knew about FP. It happens because too many FP zealots fail to explain it in a linear and axiomatic way. For example FP helps abstraction, but too many of them fail to abstract being obsessed by side-effects, purity, etc etc. Kinda fundamentalists that get lost in their talking the functional talk.

[@neoplumes]

Wait, this was released 10 days ago? I swear I come back to watch this every 6 months

[@shadamethyst1258]

11:00 - "there aren't any y in M" If only Coq would accept this as a proof every time this one detail comes up...

[@СергейМакеев-ж2н]

Are you using de Brujin indices? If so, when substituting M into x, the last thing you do to M is increase all indices by 1, which means there aren't any zeroes there, right?

[@shadamethyst1258]

@@СергейМакеев-ж2н That's the solution that the class I followed quickly led us to, yeah. But for a bit, we would work with call by value without de bruijn indices, and propagating substitutions across lambdas was a pain

[@danielli3288]

this video is very good, it doesn't assume what you know and explains everything in a clear and concise way

[@GlortMusic]

You summed up most of the Theory of Computation, Complexity and Logic course that I attended at university. Kudos to you Eyesomorphic! 👏🏼

[@fredericmazoit1441]

Very nice video. I would have added a hint as to why java is not more powerful than lambda calculus: we can write a java interpreter in lambda calculus. Thus any computation of a java program can be be performed by a lambda term.

[@56independent]

How does one then interact with the OS like most programming languages allow? How does one do the less abstract and more pragmatic "get me onto the internet" stuff? Whilst programming and lambda are equally powerful when considering closed systems where all the data is spoon-fed, in the real world of hardware and connections, one needs the interface with the real world.

[@Matthew-by2xx]

@@56independentThere are functional languages like Haskell, you still very much so can.

[@fredericmazoit1441]

@@56independent As with a processor, there are 2 kind of conputation: inputs/outputs and "real" computation. The structure of most programs can be reduced to while not finished: inputdata=input() data=computation(data) output(data) When we say that lambda calculus is as powerful as, say, java, we do not consider inputs/outputs.

[@aioia3885]

you could also make a java interpreter in the lambda calculus. In fact, someone made a compiler from c to the lambda calculus

[@56independent]

@@Matthew-by2xx ah, i forgot i even tried to learn it once

[@amritawasthi7030]

I knew about your channel since I watched the videos about category theory. I don't know how i didnt subscribe this channel. This video popped up and i was amazed by it. It's so wonderful in all sense. I watched this and saw that I hadn't subscribed to this channel.

[@setheisenberger247]

Incredible video. I was learning Lean4 a few months ago and found it difficult to wrap my head around the syntax. This video gives excellent motivation for the way Lean is!

[@himanshutripathi7441]

This is why i pay for internet. Thank you very much. I did not pay much attention in class , but if the class was explained like this it would have been awesome.

[@rumble1925]

I recommend the talk "Lambda Calculus - Fundamentals of Lambda calculus & functional programming in Javascript" and follow along in the code examples - for anyone that wants to try this in practice and encode your own functions

[@ai_outline]

We need more channels like this. Great Computer Science content mate!! Instant subscribe 🙏🏼

[@ruanvermeulen7594]

I came back to this video. I wanted to tell someone else about the concept, but no reading material explains it this beautifully. Of course I just gave them the link to the video.

[@Eyesomorphic]

That's extremely kind, thanks!

[@swankitydankity297]

fantastic video! you paced it so well and animated it so clearly that I was able to follow closely and never felt lost.

[@Italanon]

I was introduced to Alonzo Church’s lambda calculus paper when carrying out my a MSc. Course back in 1978. I don’t know how this popped up in my feed :)

[@Oscar-vs5yw]

10/10, clear explanation, good examples, awesome balance of rigor and simplicity. And a conclusion that very much so made me wonder about lambda calculus! I was always too afraid to approach lambda calculus, but your video showed it to just be python! Thanks so much

[@Eyesomorphic]

That's very encouraging, thanks for the kind words

[@danielpark9033]

Thank you so much! I can now understand how lambda calculus works more than ever!

[@ryanbartlett672]

Great animations, pacing, and no assumption that we know this logic

[@mohamedfarouk9654]

Alice is so obsessed with Java.

[@mythacker4365]

😂😂😂😂

[@bennyboiii1196]

There's a lambda interpreter called Interaction Combinators which uses graph theory to do lambda calculations in parallel without any race conditions or collisions. This actually makes parallel computing a lot easier for functional programmers, because historically, it was extremely difficult for FP do be done in parallel. It's also easier than doing it with procedural programming languages, because you don't need mutexes and locks.

[@samuelmayna]

Where did you read this?😂😂😂The opposite is what is true. FP was actually invented to enhance multiprocessing since no state is shared.

[@germanassasin1046]

16:02 very generous of you to use c as an example for statically typed language

[@ChecedRodgers]

What a lovely video. This nicely clarified a few concepts I'd encountered in passing but had not unpacked yet. Thanks for this.

[@Eyesomorphic]

That's very kind 🤠

[@st04713]

Awesome ! please and please upload more contents. This video saves a lot of my time trying to understand functional programing.

[@cindrmon]

thanks for igniting my interest for computer science just because of lambda calculus! didn't know this was indirectly taught to us through LISP, since it does seem resemble a lot of similarities to LISP's functional programming approach

[@underfilho]

I was expecting some haskell propaganda, but its actually for proof-assistants, great to hear about that!

[@pianocoder]

Thanks for the nice video again! It's very unfortunate that Coq wasn't mentioned here. :) For anyone interested in proof assistants, I recommend Software Foundations volume 1 for Coq, and mathematics in lean tutorial for Lean!

[@shathamaayouf6048]

This was therapeutic and educational at the same time. Wow.

[@funktorial]

really good animations dude. also did a really good job of picking what not to include (eta reduction, Church-Rosser, etc)

[@kenevanchik4478]

I had to take a course in this subject for my CS major long ago when I was a young man. It reminds me why I personally think I had so much problems with it, and certain kinds of math in particular. The concepts being presented to me are straightforward. What isn't however, is keeping all the symbols and characters clear in their meaning. I find these kinds of subjects tend to write things in ways which maximize brevity at the expense of understanding. Maybe that's just needed if you're an expert in the field, but honestly there just isn't enough mental separation for me from the visual presentation of the syntax. Variables are lower case letters, but applications are upper case. That beta-reduction example of M[N/x] is masking a lot going on. The example is simple in the video for comprehension, but that can get really complicated in a hurry. As a developer in the real world you can see lambda expressions in languages such as Kotlin, and frankly I don't know how much I like it. A lambda expression for a common or well known function is easier to type. If however, the function isn't well known, or complicated, then a lambda expression can make the function cryptic to the developer and difficult to grasp.

[@wol2403]

You know a video is really good when it takes you 2 hours to watch it even though its only 20 minutes long

[@kevon217]

Wow, this was so intuitively explained. Excellent!

[@cmilkau]

Not only do you only need 3 rules of syntax, in fact you only need 3 objects: a "const" function (λx.λy.x), a "symbolic evaluation" function (λf.λg.λx.[f(x)][g(x)]) [you can interpret this as taking a family f_x of functions and a family g_x of function arguments and return a family f_x(g_x) of function values), and function application. There is a mechanistic algorithm that turns any lambda expression into an expression tree containing just these two functions as leaves and function composition as inner nodes. Some important derivations: const = λx.λy.x symb = λf.λg.λx.(fx)(gx) chain = λf.λg.λx. f(gx) = λf.λg.λx.(const f x)(gx) =(**)= λf.λg. symb (const f) g =(***)= λf. symb (const f) = λf. (const symb f)(const f) = symb (const symb) const swap_args = λf.λx.λy. f y x = λf.λx.λy. (f y)(const x y) = λf.λx. symb f (const x) =(*)= λf. chain (symb f) const = λf. (chain (symb f)) (const const f) = symb (chain chain symb) (const const) swap_args = λf.λx.λy. f y x = λf.λx.λy. (f y)(const x y) = λf.λx. symb f (const x) = λf.λx. (const (symb f) x)(const x) = λf. symb (const (symb f)) const = λf. symb (const (symb f)) (const const f) = symb (λf. symb(const(symb f))) (const const) = symb (symb (const symb) (λf.const(symb f))) (const const) = symb (symb (const symb) (symb (const const) symb)) (const const) const_id = λy.λx.x = swap_args const =(*)= chain (symb const) const =(**)= symb (const (symb const)) const id = λx.x = (λy.λx.x)(const) = const_id const =(*)= chain (symb const) const const = symb const (const const) There is a simpler derivation of const_id and id, but it doesn't yield the correct type on typical (a bit too naive) type systems: const_id = λg.λx.x = λg.λx. const x (gx) = λg. symb const g = symb const, id = λx.x = (λy.λx.x)(const) = const_id const = symb const const This is because typical type systems would expect g to accept a value x, even though it is never "called" like that, because the value gx is completely ignored. Other interesting equations: chain =(***)= λf. symb (const f) = chain symb const const_id = chain const_id const

[@Ridaha]

Awesome video :-) Formalized mathematics is the future! A proof of Fermat's Last Theorem in LEAN is being currently worked on by professor Kevin Buzzard and the lean community!

[@hitoshiyamauchi]

I thank you for this excellent introduction to lambda-calculus. Thanks for the video. 😀

[@Eyesomorphic]

That means a lot, thank you :D

[@blankboy-ww7jt]

Very good introductory content, from lambda calculus to types and the CH correspondence

[@Phostings1]

I was always curious about what a lamda function did. I did some digging around and eventually understood how it works on the programming side of things. So watching this verified my understanding to some extent and made me feel a little better knowing i'm not quite strong in math,lol.

[@Double-Negative]

since regular lambda calculus is untyped, you can give functions inputs that shouldn't work. for example, if you add 2 instances of church + using church +, you get another binary function f(x,y) = 2x + y

[@CTimmerman]

Sounds significant somehow, but dangerous like Perl.

[@alonamaloh]

"Makes ANYTHING a comptuter can do", except for spell checking, apparently. :)

[@Eyesomorphic]

That does seem to be the case 😭

[@nerida3347]

Man, i would've paid attention in math class if my teachers took their time like this and explain it clearly lol

[@backhdlp]

this is actually really easy to understand if your first programming language was functional

[@adrianfd7440]

I completely enjoyed this video. Thank you so much

[@logician1234]

Please do a video on Calculus of Constructions and encoding logic in it

[@iisthphir]

Good concept, shame about the masochist who came up with the notations.

[@com0oan]

Tried to understand lambda calculus for years. First video that made the concept click in my mind. thanks!

[@familiagavassafavoretti4805]

Those pauses you make are key. Great job!!!

[@RAyLV17]

I have always been kind of comfortable with programming, but found it difficult to go into proofs and higher mathematics. But learning about this and LEAN is giving me hope. I am surely gonna check it out!

[@Eyesomorphic]

That's great to hear, proof assistants can be daunting but I find them very rewarding!

[@sundae6610]

This give me motivation. Making a language might be a good side project after i finished my current one haha

[@ValidatingUsername]

1:45 Do not confuse this with multivariable equations that you can find the inverse of or isolate for a variable and determine properties given that alpha equivalence and alpha conversion capacity. If y = x^2 that doesn’t mean x = x^2 unless the “programming language” overwrites the interpretation to make them isomorphic. Because that’s what different glyphs holding the same value is doing.

[@JJ-tp2lc]

I hope you do another video on lambda calculus, especially on the Y combinator, because I still dont quite understand it

[@ChumitoMC]

Can't believe it took me this video to understand Python's lambda function 😭 thx for this video! ☺️☺️☺️💖

[@dylanjayatilaka8533]

Bravo! I didn't think that the notion of higher order was special, but it was astounding that you could encode True and False. And "3", which seems to be three applications of any old function f. And recursion. And it seemed to me that the Curry-Howard correspondence could also itself be expressed in terms of the lambda calculus, as a proposition. Is there an end to this madness? It occured to me that, I myself might correspond to a kind of imperfect lambda machine, which begs the question, what machine? Where did the lambda notion of this representation of True and False come from? Is it possible to define a lamba expression/machine that comes up with hypotheses such as True and False, and is able to make and name things like Bool and "numbers"? I feel the answer to this imperfectly phrased question is False. But bravo again on this episode, I finally "get it", at the expense of going slightly mad. I just mention that I had to pause at several points, whereas on most other videos, I go at twice normal speed. Bravo!

[@snoopy1alpha]

I remember learning that at university. I also remember us covering the Y-function and recursion in the lambda calculus. I wish you hat covered that in more detail. My lambda calculus skills have been crippled over the years. However, I remember that I used to be good at it 😀Maybe I should challenge myself again in Haskell.

[@NostraDavid2]

If you want to do another video about math that's the foundation for a lot of code I recommend the Relational Model by E. F. Codd. I'll admit that the first paper was not as rigorous as the Lambda Calculus, but it is Super fundamental to any relational database.

[@NostraDavid2]

Oh, and use both 1969 (nice!) and 1970 papers!

[@GabriTell]

This is so great... Will you ever make a video about Type Theory? 👀

[@lexkoal8657]

Thanks for the video. A few questions/clarifications: what does Applications M M means at 4:10, and it would have been helpful to explain how multiple inputs work: the most left input goes first and works on the most left lambda abstraction and so on. Because input goes where the variable is kinda obvious but other semantics of lambda calculus are not that clear

[@vibaj16]

it means applying M to M. When lambda terms are next to each other, you apply from left to right, unless parentheses change the order: a b c means apply a to b, then apply that to c. On the other hand, a (b c) means apply b to c, then apply a to that.

[@julianvillaquira4127]

First video I watch and immediately subscribed. PS: Eyesomorphic is a damn good name 🤯

[@Eyesomorphic]

Thank you!

[@liobello3141]

You have made me very happy today.

[@Eyesomorphic]

Likewise! Thanks very much :)

[@PhilippSLSchäfer]

Lean is so cool! Not coming from a formal mathematical background Lean helped me to learn what mathematical proofs are all about. But since most analysis textbooks are based on ZF(C) and Lean is based on dependent type theory I couldn't use it to solve all my exercises :/

[@DanDart]

I seriously thought you said "magician" instead of "logician" there - that's hilarious and probably also true.

[@ananyapamde4514]

What a beautiful video! God bless you

[@jasonbrault5273]

If I might, Clojure is a modern variation on lamba calculus (a lisp) written on Java, C# (for clr) and can compule to javascript, where the type system is a moot point. A return of an object is true (including an empty list) but only false and nil is false. Fits a Haskel maybe type and allows functional composition, similar to your example of currying in the video. As Java and javascript have been the focus targets of clojure, interoperability with the underlying system is there, while the majority of the clojure types are immutable. (That's right, following a function lambda calculus design, data structres underneath do not change underneath you like in other languages. (Imagining your x can change at anytime in your currying functions, and you have the failure of modern OO languages (python lists can also change underneath you, breaking your functional proof of a programing system)) Having the choice of "when" you want a side effect, while still following a functional approach, makes clojure a go to language for me. A lisp, that is basically a mote featured lambda calculus, is a joy to write in. I'd just caution too much emphasis on types, when coming to programming. While yes types need to be accounted for, building functions that sort multiple types in a list (but all can be converted to a date long, as an example), allows a programmer to focus on the business requirement. Simply extending protocols in one location to make the function handle the types (with nil punning for null returns), allow ease to work with linux epoch and sql time stamps in a single function. By focusing too much on Types, you actually extend boilerplate code, add a requirement for internal knowledge, etc. To use your lambda calculus example, the type unsigned int, signed int, float, double, long and BigDecimal are examples of numeric types, as they are all represented in a computer's memory differently. But you, as someone building a function, want to add numbers (where all these types are of super type number). To work to build multuple functions for the multiple combinations is excessive, and instead, a dispatch system makes more sense. So what does a type really prove then, except it either is a thing or not a thing (and explicitly false). This allows a function to be built that can take comparators of "mismatched" types. In clojure syntax (where the first valid is the function and everything after is the arguments), this; (< -3.142 -2 (/ -1 2) 0 0.23 3 4.6273 4.752738M) would return true (though multiple different types). There is so much more I could say about the language (atom and ref for state change and memory transactional functions across multiple threads to simplify and guarentee state), macros for code writing code at runtime (crafting functions through symbol manipulation), filter map and reduce operations for functional compositions, natural handling of lists so you can iterate over infinite lists (and done need to build out counting a range to operate on (and inject off by one errors)), an affinity to build self recurring designed function, and a design philosophy the encourages smaller simpled functions to build higher order functions to solve problems. All based on a lisp, and there for lambda calculus design, of one function followed by arguments. Thanks for the video. (P.S. while I don't recall exactly what got me into clojure, the implementation of mini-kanren and symbolic logic functions (where given an answer, you can receive what was the inputs based upon a set of predicates) got me fascinated. I even found myself purchasing the reasoned schemer just to make sure I understood the beauty I was seeing. If you liked this video, I recommend watching any video from Daniel P. Friedman; William E. Byrd on the topic (for those who don't know, scheme is another programming language that is also a lisp). If you followed this video, your would also be also able to follow any video on just about any lisp language)

[@taylormanning2709]

"Named after the magician Haskell Curry" (7:37) Can't believe I had to look that up. For a second... I believed you

[@Eyesomorphic]

Sorry, a few people seem to have misheard 'Logician' as 'Magician'. Though there is an argument to be had that Curry's work was profound enough to classify it as magic!

[@roastyou666]

You can talk about logical programming next, like PROLOG.

[@the_actual_lauren]

Why don't we just use function notation as established early on in math education such as f(x) = x + 1 instead of lamda x . x + 1 which is harder to read?

[@M_1024]

"^x.x + 1" is directly the function itself. "f(x) = x + 1" creates a function and gives it a name. Its like a difference between "5" (value) and "x := 5" (assigment). In fact "f(x) = x + 1" is equivalent to "f := (^x.x + 1)".

[@the_actual_lauren]

@@M_1024 Thanks

[@iamsushi1056]

I’d love to see the lambda extraction to run DOOM I’d imagine the “graphics” could be represented by some sort of helper function inputting to a set of triple functions that input xy coordinates and output some sort of xyz fields (z being brightness). Obviously the software component would be complex, but workable (perhaps requiring a computer to compile it into lambda), but the firmware would be more tricky, needing a special custom program in some sort of non-lambda language to contain it and act as a bridge to the hardware proper. Input handling would also be interesting. Following the standards of assembly based game systems like the NES the binary of all the button positions could be transmitted as one number and then decoded later. The original DOOM didn’t support analogue controls after all, which makes things much easier. Memory can be treated pretty similarly, combining the binary data banks as one large integer that gets passed back into the main function and then parsed as needed. Psuedorandom and RNG is actually pretty deterministic and easy to do in a function or two. The big problem comes with time. Even if you can get a dynamic “superfunction” containing a bunch of other functions and dynamically call or ignore them (easily possible at least in theory), and have a big string of memory that gets passed back in as a variable, pure math is instantaneous. Either you would get a single frame of DOOM forever, or (ignoring hardware limitations) it would immediately read the inputs and outputs feeding back into it and try and resolve itself like expanding a recursive expression, inevitably resulting in an immediate ‘game over’.

[@bluepiston9347]

im not very familiar with this but you could take all unique states in the game like character positions and buttons held and output them along with the graphics then the computer of this would wait the time of a single frame and take in the previous state to continue just one more frame. edit: i admit this is cheating as the lambda itself can't wait.

[@bluepiston9347]

either my other reply OR: you could have lambda work with some "quantum" superpositional bufoonery to simulate and output every possible combination of button presses at any time to give a single output containing every doom game that could every be played (insert monkey at a typewriter joke here).

[@skomants2997]

Hey man we need more category theory videos please ❤

[@bachirlachguel9218]

This looks great and is very well explained, which software do you use for the slides ?

[@Eyesomorphic]

I use Manim for the animated mathematics and pivot for the animated figures. Then I use da Vinci resolve to splice them all together :)

[@Andy17385]

bro, where was this during my autumn semester :D

[@CjqNslXUcM]

I'm eagerly awaiting the next video.

[@LethalChicken77]

The problem with functional programming is it's not how humans think and it's not how computers work.

[@mushykitten]

nontheless it's an extremely useful tool for computer science. sometimes computer science or math is about exploring these unique systems and seeing what is there to learn about them.

[@rogergalindo7318]

the thing is, it’s not that simple. Compiler optimizations can do wonders. Haskell can get at 3x C. Which really is on the camp of go, java, etc, o only beaten by cpp c or rust on the other hand, once you “get” how to think “functionally”, it’s really not that hard. It’s just a matter of usage or habit

[@klermaud314]

It is definitely how many people think. It just depends on how you learned programming. And basically no programming language that people write their programs in is how computers work. The whole point of programming languages is to abstract away from the underlying machine.

[@klembokable]

I disagree with everything you just said. As someone who has built a garbage register computer in a simulation, and wrote a bit of haskell, I see as little connection between haskell and assembly as I do between python and assembly...

[@klembokable]

As far as humans thinking is concerned, I think seeing the world in terms of the inputs and outputs of actions makes about as much sense as seeing things in terms of the individual attributes of the objects acted on

[@DeathSugar]

Wish someone made step-by-step explanaition of that simple lean proof with unfolding the stuff.

[@oceanontube]

Great explanation , thank you

[@linusandersen5608]

any book recommendations on lambda calculus / computation theory?

[@TrusePkay]

This video reminds me of my F# days. The real fundamental property of functional languages that separate them from mainstream imperative languages is that functional code has an immutable state. You cannot reassign values on the fly. And there are no nulls, although these are compensated with Option type systems. This makes functional languages not suitable for applications where states are important. Because the definition is clear, functional languages are short and free of bugs most of the time. They read code left to right. I was talking to a friend. He asked me how can a programming language be practically acceptable if it does not have procedures like if statements, loop statements, nulls, return keywords. I showed him how pattern matching, function composition, partial applications, generative sequences, and list comprehension, pattern work in F# and Scala, and you don't need to write verbose repetitive loops and branches. Just go straight to the point, and the program is ready. It's sad that functional programming is not mainstream or not even computing with the mainstream.

[@beck3k]

The figure wears a wide-brimmed hat while teaching lambda calculus, just like my programming languages professor!

[@writerightmathnation9481]

It might help if you point out how this is significantly different from the traditional notation using Polish notation: f(x).

[@tricky2014]

I find lambda calculus so much more elegant than turing machines.

[@jeffreybritton3338]

Great explanation and animations.

[@qcolive]

close enough welcome back haskell

[@hazyfish1215]

Only 7K upvotes? I would expect it to be 700K!!!

[@BertLeyson]

Hearing Bob and Alice literally reminds me of GBG.

[@theedspage]

Thank you for the great introduction.

[@KayOScode]

Having experience with Haskell helped me understand this video