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

@@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!

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

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

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

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.

Great work on deriving IsZero! I bet it was satisfying to see your solution matched the one I presented.

@@glebec Thanks, and yes it was! Great presentation by the way! I wasn't expecting a response on a video so old (in KZbin terms).

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`

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

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

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.

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

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

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

@@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 👍

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.

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

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

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!

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

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.

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

@@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)?

@@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!

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

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.

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.

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

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

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.

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.

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

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

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

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

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

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.

The third one is almost, but not quite, correct. Three ways to define `succ` include `λnfa.f(nfa)`, `λnf.Bf(nf)`, and `λnfa.Bf(nf)a`. Or in JS, `n => f => a => f(n(f)(a))`, `n => f => B(f)(n(f))`, and `n => f => a => B(f)(n(f))(a)`. But the third version is not necessary, because all it does is take an `a` and immediately apply the same `a`, which is what the expression would do implicitly. When you have `λax.bx` you can cancel the x's to get `λa.b`. This is called "eta-reduction" and it means `λnf.Bf(nf)` will work just fine.

@@glebec thanks for answering! but won't the third one 'λnfa.B(nf)a' return undefined for the next church numeral calls? Since we didn't pass any value to f?

@@please.stop.coping careful - I wrote `λnfa.Bf(nf)a`, not `λnfa.B(nf)a`. The composition function `B` passes values to `f` for us! Remember, `B = λfga.f(ga)`. So `B f (n f)` = `λa.f((n f) a)`. In English + JS, composing `f` with `n f` gives us a function `a => f(n(f)(a))`. We don't have to explicitly mention the input `a` when we use `B` because B gives us back a function that takes `a`. This is why B (aka "compose") is used in what is called "tacit" or "point-free" programming - it lets you express how functions combine without explicitly writing the input parameter. ("point" here means "input," so "point-free" means "without showing inputs.") To use a simpler example, these are all equivalent: f a => f(a) b => a => f(a)(b) c => b => a => f(a)(b)(c) But there is no need to use the longer versions when just `f` will do, even though we can't see the input `a` which `f` takes written down here.

@@glebec Ohhh i see, thank you for the clarification, I would've gotten it down before if i just substituted the functions in B with the input, that didn't come to me at all. Btw thank you for the talk! Hope to see more.

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!

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

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.

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?

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

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

@@glebec Thank you very much!