Wow! I've known about currying for some time but I always just took for granted that it obviously works. Very gratifying to see a formal definition of it
Yes, although they are not that interesting. See the following discussions: math.stackexchange.com/questions/635993/what-is-the-dual-of-implication and www.reddit.com/r/dependent_types/comments/3bdzi7/the_dual_of_product_and_is_coproduct_or_what_is/
10:06 Using the name 'eval' for the function that takes (z, a) to b is very odd. If you're trying to use traditional Lisp terminology, you've got it wrong. The correct name for that function is 'apply'. 'eval' is a function from _s-expressions and environments_ to values (I'm eliding mention of the store since we're in the functional paradigm here).
why is there only one function from Void -> a for a type a? if a was Bool, why aren’t “give me any Void and I’ll give you True” and “give me any Void and I’ll give you False” different functions? i guess it comes down to “how do we precisely define when two functions are the same?”
I think because you can never actually give the function a Void, any two functions from Void to an are the same. They have the same output for all possible inputs, because there are no possible inputs
So, function object (a ⇒ b) is such object that: 1) there is morphism eval : (a ⇒ b) × a → b, 2) and for every given object z, for every given morphism g : (z × a) → b, there is unique morphism h : z → (a ⇒ b), such that g = eval ∘ (h × idₐ) ???
From a linguistic perspective verbs are functions generalized to be a relations[logic programming], contextual, ambigious, and able to look at the structure of its arguments (nouns). However, lets consider them functions, and when you say "I went to the store to buy food". The verb buy here is applied only one argument food where it would normally have another argument called the subject this means that buy is "curried" so you have a dependent clause that you can feed into a higher-order function (buy) to do its work.
@@anirudhdhullipalla5214 You know the Curry-Howard-Lambek Isomorphism that Bartosz has mentioned!? Well Lambek also worked on something known as Lambek calculus which relates grammar and its logical form to categories. There was also Montague who first used lambdas with grammars.
The only reason 0^0 is undefined in calculus is because a limit of kind "0^0" can be equal to 1, or 0, or any other number, which contradicts the uniqueness of limit.
@@Bratjuuc I'm not a real mathematician, but i always thought 0^0=1 because it's empty product. As 0! = 1. Also I'm not sure we can use limits here until we are talking about function f(n)^g(n), where f(n)->0 and g(n)->0 when n->+inf. Btw if f(n)=g(n) then limits will be 1. Limits doesn't work for numbers only for functions or sequences. Imagine we have only integers in that case there are no limits at all because we can't come close enough to any number and still be unequal to it.
@@SharplEr >btw if f = g then the limit will be equal to 1 That's a very specific example, which in no way proves that 0^0 is always 1, it just shows that there exist one limit of such type that equals to 1. What if f(n) = 1/123456^n, g(n) = -1/n? What would the limit of f(n)^g(n) look like?
@@SharplEr yeah, to talk about limits, we need to have metrics. A lot of calculus is defined in limits, f.e. pi^e. How do we even talk about pi^e, what does that even mean? How do we multiply a number with itself irrational number of times? This is where limits are coming to the rescue, Turns out that for every positive a, f x = a^x is continuous, we already know how to compute a^x for rational x, so we can just plug limits in the "holes" in the number line, by holes I mean irrational numbers. Sadly, we can't do that for 0^0.
@@Bratjuuc you mixed up limits and operations. Zero is natural, so we could use definition of natural powers : a^n = Prod a, i=1..n. And by definition empty prod is 1. This fact often used in all types of discrete math. All this limits arrives only if we are trying to work with real numbers. But here we could don't care about it because zero is natural. For example even more problems arrives when you trying to work with complex numbers or more exotic quaternion, for example.
The connection between functions and exponentials is beautiful! Is there any work connecting the size of these exponentials to Occam's razor? Comparing the size of function sets seems like a promising route for model comparison.
What is the exact formal difference between a product and a function object? If I pick b as a (a ⇒ b) object, I will automatically get eval as a projection, and also maybe a morphism h, but I'm not sure.
2:38 If the objects in *Hask* are types, and functions of a given signature are a type, then isn't it fair to say that *Hask* contains its hom-sets? Where is my misunderstanding? Is there something about the bottom values that ruins the relationship?
Thanks Dr. Milewski. If you'd be so kind as to carry me a step further, I'm struggling to see the difference between b^a and hom(a, b). Perhaps... If b^a ~ hom(a, b), would it be straightforward for you to define the isomorphism, say for the case of Int -> Int (i.e. std::function)? In that case, hom(Int, Int) = Int x Int = Int^Int, right? Perhaps, is the distinction when the function is strictly a subset of the Cartesian product? In other words when the domain and codomain are not equal? In that case, I could see that hom(A, B) is a subset of AxB. But then hom(A, B) isn't isomorphic to AxB because the relationship isn't surjective: I could easily find an element in the cartesian product which isn't mapped to from hom(A,B), since the cartesian product would also contain hom(B,A). Thanks for taking the time to worth through all of that.
Probably the best way to see this is to realize that hom(1, b^a) is isomorphic to hom(a, b), where 1 is the terminal object. This follows directly from the definition of the exponential object using an adjunction, and the fact that the terminal object is the unit of the product. In Hask, a function from the unit picks an element of the set, here the element of the exponential set.
Seeing as ∞ is not a number, but a symbol used in calculus to denote the behavior of certain limits, you would have to define limits in category theory first.
My blog goes over this material, sometimes in more detail, and it has exercises. bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Most random bunches of objects and arrows that satisfy category axioms will not have products (and are not Set-like). In particular, a single-object monoid is not Set-like, a preorder of natural numbers is not Set-like. Any discrete category (no arrows other than identities) is non-cartesian.
I could follow this well except for the part at ~30 where the diagram is interpreted to say a function of two arguments is equivalent to a function which returns a function. Now I understand what the conclusion means, but not how you get it from the diagram. g`=g o h x id How can you infer from that that g` (a function of two arguments) is the same as h (a function of one argument) . There is also a g in that equation which is a function of two arguments (z x a, just like g` is a function of z`x a) . Does equivalent mean more loose like up to isomorphism?
You don't so much get it from the diagram as from the words: For every g (a function of a product of two arguments) there is a unique function h (which produces a function a=>b). That defines a mapping from g to h. The other way around is trivial: for every h you construct g = eval . (h x id).
Something funny crossed my mind. For every morphism a -> b we have an object (a -> b) X a, and a morphism ((a -> b) X a) -> b. If that's so, wouldn't we also have an object that represents ((a -> b) X a) -> b and, therefore, a morphism ((a -> b) X a) -> b) X ((a -> b) X a), and so on?
There's a whole Wikipedia article on the topic of 0^0. In category theory this is a set of morphisms from the initial object to itself so it must be a singleton. Every object has at least one endomorphism, the identity. Void is no exception.
@@DrBartosz Indeed, I had a very simplistic view of 0^0 that came from introductory analysis classes at university a long time ago :) . Also, I should have realized that Void -> Void is the identity morphism for this object =/ Thanks a lot for the reply and the clarification!
this b^a thing is again something where I thought "WTF?? Why do mathematicians make everybody's lives hard??" but then realize after the explanation that it really makes totally sense from a certain perspective. ps: at 40:44 you can really tell by his voice that he went full crazy and it is too late.
crrrrssssshhhhrrrrghhhh booom! Mind blown !! :)) This is how mi mind was when i saw: Bool -> Int to be Int ^ 2 then Int ^ Bool Rely awesome stuff !! Wish i stumbled upon this concepts sooner :))
I have to say, this is the best explanation of exponentials I have encountered by far. Textbooks really struggle when it comes to category theory.
Goldblatt's book on topoi is good. I tend to watch yt vids and look in that book when I don't understand something
Wow! I've known about currying for some time but I always just took for granted that it obviously works. Very gratifying to see a formal definition of it
I just have to ask... are there coexponentials? :)
Or put another way, would turning all the arrows be meaningful? As it seems to be so elsewhere.
Yes, although they are not that interesting. See the following discussions: math.stackexchange.com/questions/635993/what-is-the-dual-of-implication and www.reddit.com/r/dependent_types/comments/3bdzi7/the_dual_of_product_and_is_coproduct_or_what_is/
10:06 Using the name 'eval' for the function that takes (z, a) to b is very odd. If you're trying to use traditional Lisp terminology, you've got it wrong. The correct name for that function is 'apply'. 'eval' is a function from _s-expressions and environments_ to values (I'm eliding mention of the store since we're in the functional paradigm here).
why is there only one function from Void -> a for a type a? if a was Bool, why aren’t “give me any Void and I’ll give you True” and “give me any Void and I’ll give you False” different functions?
i guess it comes down to “how do we precisely define when two functions are the same?”
I think because you can never actually give the function a Void, any two functions from Void to an are the same. They have the same output for all possible inputs, because there are no possible inputs
So, function object (a ⇒ b) is such object that:
1) there is morphism eval : (a ⇒ b) × a → b,
2) and for every given object z, for every given morphism g : (z × a) → b, there is unique morphism h : z → (a ⇒ b), such that g = eval ∘ (h × idₐ)
???
This is so cool, explaining currying in category theory.
From a linguistic perspective verbs are functions generalized to be a relations[logic programming], contextual, ambigious, and able to look at the structure of its arguments (nouns). However, lets consider them functions, and when you say "I went to the store to buy food". The verb buy here is applied only one argument food where it would normally have another argument called the subject this means that buy is "curried" so you have a dependent clause that you can feed into a higher-order function (buy) to do its work.
@@anirudhdhullipalla5214 You know the Curry-Howard-Lambek Isomorphism that Bartosz has mentioned!? Well Lambek also worked on something known as Lambek calculus which relates grammar and its logical form to categories. There was also Montague who first used lambdas with grammars.
@@allendupras Ah, cool!
So, in category theory 0^0 is definitely 1?
Since there's only one Void -> Void.
The only reason 0^0 is undefined in calculus is because a limit of kind "0^0" can be equal to 1, or 0, or any other number, which contradicts the uniqueness of limit.
@@Bratjuuc I'm not a real mathematician, but i always thought 0^0=1 because it's empty product. As 0! = 1. Also I'm not sure we can use limits here until we are talking about function f(n)^g(n), where f(n)->0 and g(n)->0 when n->+inf. Btw if f(n)=g(n) then limits will be 1. Limits doesn't work for numbers only for functions or sequences. Imagine we have only integers in that case there are no limits at all because we can't come close enough to any number and still be unequal to it.
@@SharplEr >btw if f = g then the limit will be equal to 1
That's a very specific example, which in no way proves that 0^0 is always 1, it just shows that there exist one limit of such type that equals to 1.
What if f(n) = 1/123456^n, g(n) = -1/n? What would the limit of f(n)^g(n) look like?
@@SharplEr yeah, to talk about limits, we need to have metrics. A lot of calculus is defined in limits, f.e. pi^e. How do we even talk about pi^e, what does that even mean? How do we multiply a number with itself irrational number of times? This is where limits are coming to the rescue, Turns out that for every positive a, f x = a^x is continuous, we already know how to compute a^x for rational x, so we can just plug limits in the "holes" in the number line, by holes I mean irrational numbers. Sadly, we can't do that for 0^0.
@@Bratjuuc you mixed up limits and operations. Zero is natural, so we could use definition of natural powers : a^n = Prod a, i=1..n. And by definition empty prod is 1. This fact often used in all types of discrete math. All this limits arrives only if we are trying to work with real numbers. But here we could don't care about it because zero is natural. For example even more problems arrives when you trying to work with complex numbers or more exotic quaternion, for example.
Sir, you opened a new chapter in my journey through mathematics and programming
The connection between functions and exponentials is beautiful!
Is there any work connecting the size of these exponentials to Occam's razor? Comparing the size of function sets seems like a promising route for model comparison.
What is the exact formal difference between a product and a function object? If I pick b as a (a ⇒ b) object, I will automatically get eval as a projection, and also maybe a morphism h, but I'm not sure.
33:19 explanation of interpretation as exponential
Thank you for the awesome lecture. I have a question. Is it required to have a product for every pair of objects to define function types?
2:38 If the objects in *Hask* are types, and functions of a given signature are a type, then isn't it fair to say that *Hask* contains its hom-sets? Where is my misunderstanding? Is there something about the bottom values that ruins the relationship?
Haskell type a->b is the exponential object. It is isomorphic to the hom-set between a and b.
Thanks Dr. Milewski. If you'd be so kind as to carry me a step further, I'm struggling to see the difference between b^a and hom(a, b). Perhaps... If b^a ~ hom(a, b), would it be straightforward for you to define the isomorphism, say for the case of Int -> Int (i.e. std::function)? In that case, hom(Int, Int) = Int x Int = Int^Int, right?
Perhaps, is the distinction when the function is strictly a subset of the Cartesian product? In other words when the domain and codomain are not equal? In that case, I could see that hom(A, B) is a subset of AxB. But then hom(A, B) isn't isomorphic to AxB because the relationship isn't surjective: I could easily find an element in the cartesian product which isn't mapped to from hom(A,B), since the cartesian product would also contain hom(B,A).
Thanks for taking the time to worth through all of that.
Probably the best way to see this is to realize that hom(1, b^a) is isomorphic to hom(a, b), where 1 is the terminal object. This follows directly from the definition of the exponential object using an adjunction, and the fact that the terminal object is the unit of the product. In Hask, a function from the unit picks an element of the set, here the element of the exponential set.
Beautify how Currying falls off the construction
Hi,
at 41m55s, an interesting question pop up in mind mind. how does the Category theory deals with undefine limis from calculus like 1^\infinity ?
Seeing as ∞ is not a number, but a symbol used in calculus to denote the behavior of certain limits, you would have to define limits in category theory first.
Thanks for Great Lectures. What supplementary text you would suggest for further reading and solving problems. Thanks.
My blog goes over this material, sometimes in more detail, and it has exercises. bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Can you give an example for a non-cartesian category? Additionaly what does a category witch is not Set-like looks like?
Most random bunches of objects and arrows that satisfy category axioms will not have products (and are not Set-like). In particular, a single-object monoid is not Set-like, a preorder of natural numbers is not Set-like. Any discrete category (no arrows other than identities) is non-cartesian.
I could follow this well except for the part at ~30 where the diagram is interpreted to say a function of two arguments is equivalent to a function which returns a function. Now I understand what the conclusion means, but not how you get it from the diagram.
g`=g o h x id
How can you infer from that that g` (a function of two arguments) is the same as h (a function of one argument) . There is also a g in that equation which is a function of two arguments (z x a, just like g` is a function of z`x a) .
Does equivalent mean more loose like up to isomorphism?
You don't so much get it from the diagram as from the words: For every g (a function of a product of two arguments) there is a unique function h (which produces a function a=>b). That defines a mapping from g to h. The other way around is trivial: for every h you construct g = eval . (h x id).
Something funny crossed my mind. For every morphism a -> b we have an object (a -> b) X a, and a morphism ((a -> b) X a) -> b. If that's so, wouldn't we also have an object that represents ((a -> b) X a) -> b and, therefore, a morphism ((a -> b) X a) -> b) X ((a -> b) X a), and so on?
omfg!!! this is magic
9:48 for some reason I found this hilarious
Thank you for the great lectures!
So by analogy f :: Void -> Void would be equivalent to 0^0, which is undefined, so f doesn't exist!
There's a whole Wikipedia article on the topic of 0^0. In category theory this is a set of morphisms from the initial object to itself so it must be a singleton. Every object has at least one endomorphism, the identity. Void is no exception.
@@DrBartosz Indeed, I had a very simplistic view of 0^0 that came from introductory analysis classes at university a long time ago :) .
Also, I should have realized that Void -> Void is the identity morphism for this object =/
Thanks a lot for the reply and the clarification!
this b^a thing is again something where I thought "WTF?? Why do mathematicians make everybody's lives hard??" but then realize after the explanation that it really makes totally sense from a certain perspective.
ps: at 40:44 you can really tell by his voice that he went full crazy and it is too late.
Sorry for the spam. In what video do you define/explain universal property?
Which video do u explain where you treat types as objects?
what do you mean that what we do in programming is approximately what the category of Set is?
crrrrssssshhhhrrrrghhhh booom! Mind blown !! :)) This is how mi mind was when i saw: Bool -> Int to be Int ^ 2 then Int ^ Bool
Rely awesome stuff !! Wish i stumbled upon this concepts sooner :))
Why is it none trivial to form products of morphisms?
Whats a hom-set? A set of morphisms?