Thanks Bartosz, these lectures are fantastic. I have looked into category theory before but since it is very abstract it has seemed kind of hollow without knowing the motivation of the definitions. It is nice to have this inviting and careful expository to understand why things are defined the way they are. I have really been enjoying it so far. I have watched through all the previous videos and didn't really see the significance of the product in the way it is defined, until this video starting around 1:45. The fact that c is the most "pure" out of all the other candidates for product due to it being more "reduced" than the others (i.e., following the arrow of truth further) is what made it click for me. You kind of said it before but re-explaining it here helped clarify it.
This video series is epic!!! I would love to be able to go through it faster because I can’t wait to learn more but it is not something always trivial to understand so let’s just go one step at a time…
I've been following this series while reading this book mitpress.mit.edu/books/basic-category-theory-computer-scientists, and thanks to you I've gotten great intuition, and can "easily" follow the book, I'm even doing the exercises!
Are the injections from objects A and B into their coproduct category proofs that their disjunction is true? (If we were to represent them as propositions)
I have a very general question about the meaning of the commutation diagrams. Can the equality of morphisms be deduced from the diagram? For example, can p' = p . m be concluded just from the product type diagram? Or do the diagrams just express the _possibility_ of morphisms being equal? I guess it's the latter, because otherwise it would not make sense to have multiple morphisms between the same pair of objects, right?
Right! A diagram shows two (or sometimes more) ways of getting from one object to another. When we say: the following diagram commutes, we impose the condition that they be equal. In the case of a product, we say there exists a (unique) m such that p' = p . m. There may be other m's for which this is not true. Conversely, if there are no ms satisfying this equation, or if there are multiple ms that do, this is not a product.
A designer knows he has achieved perfection not when there is nothing left to add, but when there is nothing left to take away. Antoine de Saint-Exupery Read more at: www.brainyquote.com/quotes/quotes/a/antoinedes121910.html ... Hence the universal construction "trick"
How is pattern matching on sum type defined using morphisms? Is it just an inverse of i (or j)? If so, do these inverse morphisms always exist? Looking at how pattern matching works, it looks like they should.
Pattern matching is the result of the universal property. You define a function h from the sum a+b to c by providing two functions a->c and b->c. These correspond to two cases in the pattern match.
I still can't catch something. Why 'a' union has no morphism to discriminated union 'aL+aR' ? Why it can not cover just a part of a set, aL for example? Is this reqired to cover the entire set? I feel some contradiction to previous lessons, where a unit set has morphisms to all other sets, just picking one element within it. Sorry for my stupidity ((
Thanks Bartosz, but is 'aL+aR' to 'a' morphism actually unique? There could be other morphisms, that also 'discard' the tag L/R, but remap elements of 'a' in other way. Composition requirements will be also satisfied, if i` and j` remap elements of 'a' in the same way as m. And such i` and j` actually exist, because the tag L/R is not influencing on the result. Where is my mistake?
@@ВалентинТ-х6ц i and j are part of the definition of your coproduct. What you are proposing is selecting a different coproduct. Which is fine, because a coproduct is only defined up to a (unique) isomorphism. But for a given triple: set and two injections, the mapping m is unique.
Isn't a coproduction just a kind of inheritance? The coproduct C of classes A and B is just an abstract class with two subclasses A and B. (Of course you need wrappers if A is say int to make it a class)
Except that the tagged constructors (ie actual instances of a coproduct isnt typeable). So "Left Int", "Left a", "Right Bool", "Right b" cannot be typed (a function cannot have these as types for their parameters or return values). But subclasses are classes and can be typed.
Is there a way to form (co)equalizers in a language like haskell? I am coming from math to cs, and this was one of the first things I tried to do, but it does not seem straightforward.
(co)equilizers are special types of (co)limits. I've seen (co)limits defined in Haskell by Edward Kmett using Kan extensions. Have a look at: hackage.haskell.org/package/category-extras-0.52.1/docs/Control-Functor-Limit.html
As a mathematician also interested in how CT is applied to Haskell, this was also the first question on my mind. It seems important: clearly products (and coproducts) exist in the category Hask (maybe ignoring issues like bottom which I don't fully understand quite yet). If it also had had equalisers (coequalisers, resp.) then it would have all limits (colimits, resp.), that is it would be complete (cocomplete, resp.). It would be nice if there was a clear, mathematicial account of this. Presumably this should all work out since Hask seems to be quite closely modelled by Set (which has all limits and colimits).
TypeScript goes even further although it's not a functional language (so maybe you won't like it). It defines product of two (as you call them) "types" by an & operator. The problem is that you cannot construct (sorry for using number instead of Int, but TypeScript has only number): let x : number & bool; x = // ??
Now I realise that | operator is not exactly same as Either, because the value can be taken from this set: {a, b, a & b}. On the other hand the Either takes a value just from {a, b}
the "true" way, in a sense, of defining products and coproducts in haskell isn't by using builtins like (,) though. to construct the product (up to isomorphism) of a and b, you define data Product a b = a `P` b or equivalently with record syntax/GADT syntax: data Product a b = P { p :: a, q :: b } data Product a b where P :: a -> b -> Product a b for coproducts you define data Coproduct a b = I a | J b or with GADT syntax data Coproduct a b where i :: a -> Coproduct a b j :: b -> Coproduct a b of course you can extend these for n-ary (co)products, since haskell has all finite (co)products
I can see that in category set the sum is at least the same cardinal number as the sum of the cardinal numbers of the two sets, but I don't see why it cannot be larger.
I don't get how these universal constructions work. We prepare some template, then we search entire category for this pattern, we get some results, but how do we rank them? We just declare some property the ideal object we're looking for satisfies and what comes next? How do we get a pointer to the ideal object? How do we compute it? How do we find out there is one? How do we know that it's unique? I don't get it at all.
Well, maybe it's like a root of unsolvable polynomial of power of 5: we know that it exists, but it's algebraicly impossible to write answer in algebraic form
It's a valid candidate but definitely not the best. Exercise: find the unique h :: Int -> Either (Int, Float) (Bool, Int) that makes the two triangles commute.
Thanks for the reply, I think I understand: There is no such function, as i couldn't know whether to create a Left or a Right (And also, i don't know which Float/Bool to create). But there is a function the other way: m :: Either (Int, Float) (Bool, Int) -> Int m (Left l) = fst l m (Right r) = snd r So Either (Int, Float) (Bool, Int) is strictly the better canidate than Int.
I get confused every time I restart trying to watch this series. What does it mean for there to be a unique morphism from a to b? Is this unique up to isomorphism, or is it really unique? If I compose an arrow x with an identity, is it x, or is it x only up to isomorphism? What does it mean for there to be two morphisms from a to be which are NOT isomorphic? How can we distinguish different morphisms between the same two objects?
It means unique as elements of the class of morphisms from a to b, denoted Mor(a, b) or more commonly, Hom(a, b). This class can be a set or proper class.
what are the equivalents for i and j in haskell for the coproduct? Or the Either type? The relation with the coproduct with the haskell Either type is blurry. Are there two functions, i and j that construct the Either type or is i and j typically represented as a -> b -> c in haskell?
Non-discriminated union is a weird thing, which really makes sens only in some set theories. The difference is when two sets overlap, which is hard to express in category theory or in programming.
@@DrBartosz I see. Also I'm really enjoying both your lectures and your book. It really is the missing piece for me to understand category theory. Phenomenal job!
So basically, now my C++ exceptions are gone? Saw this here: github.com/google/draco Funny thing is, now I can see that int f(); doesn't map unit to int, but unit+exception to int + exception or similar unless we declare it noexcept. The only problem remains is the side effects generated by the functions.
Thanks Bartosz, these lectures are fantastic. I have looked into category theory before but since it is very abstract it has seemed kind of hollow without knowing the motivation of the definitions. It is nice to have this inviting and careful expository to understand why things are defined the way they are. I have really been enjoying it so far.
I have watched through all the previous videos and didn't really see the significance of the product in the way it is defined, until this video starting around 1:45. The fact that c is the most "pure" out of all the other candidates for product due to it being more "reduced" than the others (i.e., following the arrow of truth further) is what made it click for me. You kind of said it before but re-explaining it here helped clarify it.
I had at least 3 epiphany moments during this video, it explains so much! Thank you.
I only had 2 but still that's great!
This is putting so much into place. Formalizing intuitions that has taken years to form.
This video series is epic!!! I would love to be able to go through it faster because I can’t wait to learn more but it is not something always trivial to understand so let’s just go one step at a time…
I've been following this series while reading this book mitpress.mit.edu/books/basic-category-theory-computer-scientists, and thanks to you I've gotten great intuition, and can "easily" follow the book, I'm even doing the exercises!
I'm looking for good books about category theory for programmers. Did you look another book apart from this one?
Actually, there is a book compiled from blog posts by the author of these talks at github.com/hmemcpy/milewski-ctfp-pdf
Maybe D. I. Spivak, Category Theory for the Sciences.
100 years from now these vids will have the same prominence as the constitutions
Are the injections from objects A and B into their coproduct category proofs that their disjunction is true? (If we were to represent them as propositions)
Exactly. See my talk at Lambda Days: ruclips.net/video/dgrucfgv2Tw/видео.html
I have a very general question about the meaning of the commutation diagrams. Can the equality of morphisms be deduced from the diagram? For example, can p' = p . m be concluded just from the product type diagram? Or do the diagrams just express the _possibility_ of morphisms being equal? I guess it's the latter, because otherwise it would not make sense to have multiple morphisms between the same pair of objects, right?
Right! A diagram shows two (or sometimes more) ways of getting from one object to another. When we say: the following diagram commutes, we impose the condition that they be equal. In the case of a product, we say there exists a (unique) m such that p' = p . m. There may be other m's for which this is not true. Conversely, if there are no ms satisfying this equation, or if there are multiple ms that do, this is not a product.
A designer knows he has achieved perfection not when there is nothing left to add, but when there is nothing left to take away. Antoine de Saint-Exupery
Read more at: www.brainyquote.com/quotes/quotes/a/antoinedes121910.html
... Hence the universal construction "trick"
How is pattern matching on sum type defined using morphisms? Is it just an inverse of i (or j)? If so, do these inverse morphisms always exist? Looking at how pattern matching works, it looks like they should.
Pattern matching is the result of the universal property. You define a function h from the sum a+b to c by providing two functions a->c and b->c. These correspond to two cases in the pattern match.
Thank you for clarifying!
I still can't catch something. Why 'a' union has no morphism to discriminated union 'aL+aR' ? Why it can not cover just a part of a set, aL for example? Is this reqired to cover the entire set? I feel some contradiction to previous lessons, where a unit set has morphisms to all other sets, just picking one element within it. Sorry for my stupidity ((
The mapping exists but is not unique.
Thanks Bartosz, but is 'aL+aR' to 'a' morphism actually unique? There could be other morphisms, that also 'discard' the tag L/R, but remap elements of 'a' in other way. Composition requirements will be also satisfied, if i` and j` remap elements of 'a' in the same way as m. And such i` and j` actually exist, because the tag L/R is not influencing on the result. Where is my mistake?
@@ВалентинТ-х6ц i and j are part of the definition of your coproduct. What you are proposing is selecting a different coproduct. Which is fine, because a coproduct is only defined up to a (unique) isomorphism. But for a given triple: set and two injections, the mapping m is unique.
@@DrBartosz Aha! Thanks a lot.
Isn't a coproduction just a kind of inheritance? The coproduct C of classes A and B is just an abstract class with two subclasses A and B. (Of course you need wrappers if A is say int to make it a class)
Except that the tagged constructors (ie actual instances of a coproduct isnt typeable). So "Left Int", "Left a", "Right Bool", "Right b" cannot be typed (a function cannot have these as types for their parameters or return values). But subclasses are classes and can be typed.
I'm actually a Mathematician and I find this course very amusing :)
Is there a way to form (co)equalizers in a language like haskell? I am coming from math to cs, and this was one of the first things I tried to do, but it does not seem straightforward.
(co)equilizers are special types of (co)limits. I've seen (co)limits defined in Haskell by Edward Kmett using Kan extensions. Have a look at: hackage.haskell.org/package/category-extras-0.52.1/docs/Control-Functor-Limit.html
As a mathematician also interested in how CT is applied to Haskell, this was also the first question on my mind. It seems important: clearly products (and coproducts) exist in the category Hask (maybe ignoring issues like bottom which I don't fully understand quite yet). If it also had had equalisers (coequalisers, resp.) then it would have all limits (colimits, resp.), that is it would be complete (cocomplete, resp.). It would be nice if there was a clear, mathematicial account of this.
Presumably this should all work out since Hask seems to be quite closely modelled by Set (which has all limits and colimits).
TypeScript goes even further although it's not a functional language (so maybe you won't like it). It defines product of two (as you call them) "types" by an & operator. The problem is that you cannot construct (sorry for using number instead of Int, but TypeScript has only number):
let x : number & bool;
x = // ??
Now I realise that | operator is not exactly same as Either, because the value can be taken from this set: {a, b, a & b}. On the other hand the Either takes a value just from {a, b}
the "true" way, in a sense, of defining products and coproducts in haskell isn't by using builtins like (,) though.
to construct the product (up to isomorphism) of a and b, you define
data Product a b = a `P` b
or equivalently with record syntax/GADT syntax:
data Product a b = P { p :: a, q :: b }
data Product a b where
P :: a -> b -> Product a b
for coproducts you define
data Coproduct a b
= I a
| J b
or with GADT syntax
data Coproduct a b where
i :: a -> Coproduct a b
j :: b -> Coproduct a b
of course you can extend these for n-ary (co)products, since haskell has all finite (co)products
I can see that in category set the sum is at least the same cardinal number as the sum of the cardinal numbers of the two sets, but I don't see why it cannot be larger.
Hongbo Li if it could be larger, m would not be unique (there could be multiple version of m doing funny things out of (Either a b))
I don't get how these universal constructions work. We prepare some template, then we search entire category for this pattern, we get some results, but how do we rank them? We just declare some property the ideal object we're looking for satisfies and what comes next? How do we get a pointer to the ideal object? How do we compute it? How do we find out there is one? How do we know that it's unique? I don't get it at all.
Well, maybe it's like a root of unsolvable polynomial of power of 5: we know that it exists, but it's algebraicly impossible to write answer in algebraic form
Can the coproduct also be the common type of two pairs? For example:
a = (Int, Float)
b = (Bool, Int)
c = Int
i = fst
j = snd
It's a valid candidate but definitely not the best. Exercise: find the unique h :: Int -> Either (Int, Float) (Bool, Int) that makes the two triangles commute.
Thanks for the reply, I think I understand:
There is no such function, as i couldn't know whether to create a Left or a Right (And also, i don't know which Float/Bool to create).
But there is a function the other way:
m :: Either (Int, Float) (Bool, Int) -> Int
m (Left l) = fst l
m (Right r) = snd r
So Either (Int, Float) (Bool, Int) is strictly the better canidate than Int.
Actually, I meant a function in the opposite direction. There is just one.
I get confused every time I restart trying to watch this series. What does it mean for there to be a unique morphism from a to b? Is this unique up to isomorphism, or is it really unique? If I compose an arrow x with an identity, is it x, or is it x only up to isomorphism? What does it mean for there to be two morphisms from a to be which are NOT isomorphic? How can we distinguish different morphisms between the same two objects?
It means unique as elements of the class of morphisms from a to b, denoted Mor(a, b) or more commonly, Hom(a, b). This class can be a set or proper class.
what are the equivalents for i and j in haskell for the coproduct? Or the Either type? The relation with the coproduct with the haskell Either type is blurry. Are there two functions, i and j that construct the Either type or is i and j typically represented as a -> b -> c in haskell?
The two constructors, Left and Right.
There is Vid and CoVid. Sorry I just wanted to say that I am watching this during 2021.
I'm curious in Haskell how can you "derive" a union from a disjoint union (Either) on types as sets. What would m look like?
I guess by by derive, I mean factorize...
Non-discriminated union is a weird thing, which really makes sens only in some set theories. The difference is when two sets overlap, which is hard to express in category theory or in programming.
@@DrBartosz I see. Also I'm really enjoying both your lectures and your book. It really is the missing piece for me to understand category theory. Phenomenal job!
So basically, now my C++ exceptions are gone? Saw this here: github.com/google/draco
Funny thing is, now I can see that int f(); doesn't map unit to int, but unit+exception to int + exception or similar unless we declare it noexcept. The only problem remains is the side effects generated by the functions.
🇹🇻 31:20 😅
Is Coproducts the same as sum types?
In programming, yes.
Bartosz Milewski Thank you, and congratulations on these outstanding lessons.
Why isn't a pair/tuple called a product type?
It is. Did I say otherwise?
Sorry, must have missed it
Soooo, c is like an atomic "function", and c' can be factored in terms of m and the real c, right? xD
In 2016, you had Vid
In 2019, you had CoVid.