39:00 ish Yes, It is true that the comonad laws are just inverted monad laws. This is because the monad laws are just the criteria for being a category, specialized to the Kleisli category where identity = return and composition = (>=>) (Kleisli arrow, "fish operator"). Similarly, the comonad laws are nothing more than the category laws for a CoKleisli category, where identity = extract and composition = (=>=) (CoKleisli arrow, "plane operator" or something). So the laws are just left- and right-identity (extract composed by =>= with a CoKleisli morphism wa->b does nothing to the morphism) and associativity of composition, iirc. But in the normal setting we rewrite these laws to talk about duplicate ("delta" in category theory) instead of CoKleisli composition, which I'm fine with because duplicate really distills the essence of comonads imo, just like how join ("mu") distills the essence of monads more than >=> or bind does
At 39:43 - I suspect it's a mistake to say that duplicate isn't a natural transformation. (I haven't thought it through properly, but this is my intuition). I think this has to be the case because the monad laws arise from the monoid laws since a monad is a monoid in the category of endofunctors. The monoid operation and unit (join and return) are manifest as natural transformations. So if comonad is a comonoid in the category of endofunctors (as the title slide suggests) then shouldn't cojoin and coreturn (extract and duplicate) be natural transformations of the comonoid?
Yes that's right, I also wondered about the same and Bartosz's blog post confirms that extract and duplicate are natural transformations. It's in the Comonad Categorically section bartoszmilewski.com/2017/01/02/comonads/
I don't understand the spreadsheet example at 42:20. Given the intuition from streams and trees (each node becomes an entire stream/tree with a different focus), I would be tempted to say that each cell becomes a spreadsheet. But I have no intuition for what is contained within that spreadsheet. I think this stems from the spreadsheet example being 'global' and the prior examples being 'relative', but I don't know how to think about the spreadsheet example. Edit: Ok, so the spreadsheet in each cell is the same global spreadsheet but with that cell focused in the interior spreadsheet... but why are cells focused at all in the spreadsheet? What is the difference between the same spreadsheet focusing B1 vs. focusing C2? I guess this makes sense if spreadsheets can be queried like "sum of the current column", so "current" must be defined in some way. Is that at all correct? Also (and perhaps this is addressed later in the video or series) but I'm trying to reason for myself what the comonad of Maybe is, and I find this difficult too. I think that once again this is a 'global' comonad but my analysis ends there. Our structure of "Maybe a' becomes a Maybe of 'Maybe a'? I don't even know how to ask the question I'm getting at :/. The 'views' on Maybe Maybe a are Just Maybe a and None, but does that mean anything? Edit: So Maybe does not have a comonad because such a structure would violate the extract law when the Maybe is None. If we handwave that for a moment, would it mean anything to consider 'Maybe Maybe a'?
About that spreadsheet thing, "focusing" on a cell in the spreadsheet means that whatever function which "transforms a cell" by any means, will be applied on the "focused" cell. So you can use "extend" combined with a query to change focus on another cell and apply the transformation to it
The same spreadsheet with a different focus, in Chris' terminology are different views, which are a different comonadic value (a "w a"). They are different because when you extract (i.e. use your "current") you get a different "a" specifically the focus. But you can say that the context (the whole spreadsheet) indeed doesn't change. Maybe (Maybe a) makes sense as a Monadic value, you can squash/join those layers and respect the laws. (Just (Just a)) == (Just a) and all other cases are Nothing. But if I give you a Nothing you have nothing to extract. Some reason that a List isn't a comonad, if I give you an empty list you have nothing to extract. However a non empty list always has something in it, so you can extract it, so a non empty list is a comonad! And funny stuff, a non nothing Maybe, basically a new type (newtype Something a = Something a) is also a comonad :)
"talking to a wall here, this is great" HAHA brutal
39:00 ish Yes, It is true that the comonad laws are just inverted monad laws. This is because the monad laws are just the criteria for being a category, specialized to the Kleisli category where identity = return and composition = (>=>) (Kleisli arrow, "fish operator"). Similarly, the comonad laws are nothing more than the category laws for a CoKleisli category, where identity = extract and composition = (=>=) (CoKleisli arrow, "plane operator" or something).
So the laws are just left- and right-identity (extract composed by =>= with a CoKleisli morphism wa->b does nothing to the morphism) and associativity of composition, iirc. But in the normal setting we rewrite these laws to talk about duplicate ("delta" in category theory) instead of CoKleisli composition, which I'm fine with because duplicate really distills the essence of comonads imo, just like how join ("mu") distills the essence of monads more than >=> or bind does
At 39:43 - I suspect it's a mistake to say that duplicate isn't a natural transformation. (I haven't thought it through properly, but this is my intuition). I think this has to be the case because the monad laws arise from the monoid laws since a monad is a monoid in the category of endofunctors. The monoid operation and unit (join and return) are manifest as natural transformations. So if comonad is a comonoid in the category of endofunctors (as the title slide suggests) then shouldn't cojoin and coreturn (extract and duplicate) be natural transformations of the comonoid?
Yes that's right, I also wondered about the same and Bartosz's blog post confirms that extract and duplicate are natural transformations. It's in the Comonad Categorically section bartoszmilewski.com/2017/01/02/comonads/
It absolutely is a natural transformation from W to W^2
I don't understand the spreadsheet example at 42:20. Given the intuition from streams and trees (each node becomes an entire stream/tree with a different focus), I would be tempted to say that each cell becomes a spreadsheet. But I have no intuition for what is contained within that spreadsheet. I think this stems from the spreadsheet example being 'global' and the prior examples being 'relative', but I don't know how to think about the spreadsheet example.
Edit: Ok, so the spreadsheet in each cell is the same global spreadsheet but with that cell focused in the interior spreadsheet... but why are cells focused at all in the spreadsheet? What is the difference between the same spreadsheet focusing B1 vs. focusing C2? I guess this makes sense if spreadsheets can be queried like "sum of the current column", so "current" must be defined in some way. Is that at all correct?
Also (and perhaps this is addressed later in the video or series) but I'm trying to reason for myself what the comonad of Maybe is, and I find this difficult too. I think that once again this is a 'global' comonad but my analysis ends there. Our structure of "Maybe a' becomes a Maybe of 'Maybe a'? I don't even know how to ask the question I'm getting at :/. The 'views' on Maybe Maybe a are Just Maybe a and None, but does that mean anything?
Edit: So Maybe does not have a comonad because such a structure would violate the extract law when the Maybe is None. If we handwave that for a moment, would it mean anything to consider 'Maybe Maybe a'?
About that spreadsheet thing, "focusing" on a cell in the spreadsheet means that whatever function which "transforms a cell" by any means, will be applied on the "focused" cell. So you can use "extend" combined with a query to change focus on another cell and apply the transformation to it
The same spreadsheet with a different focus, in Chris' terminology are different views, which are a different comonadic value (a "w a"). They are different because when you extract (i.e. use your "current") you get a different "a" specifically the focus. But you can say that the context (the whole spreadsheet) indeed doesn't change.
Maybe (Maybe a) makes sense as a Monadic value, you can squash/join those layers and respect the laws. (Just (Just a)) == (Just a) and all other cases are Nothing. But if I give you a Nothing you have nothing to extract. Some reason that a List isn't a comonad, if I give you an empty list you have nothing to extract. However a non empty list always has something in it, so you can extract it, so a non empty list is a comonad! And funny stuff, a non nothing Maybe, basically a new type (newtype Something a = Something a) is also a comonad :)