Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: optics - grates

Bruno Gavranović (May 24 2021 at 16:12):

I'm trying to understand the definition of a grate in the Profunctor optics: a categorical update paper (Proposition 3.31).

Namely, the variances of the monoidal actions used here seem to be wrong. If I look at the 2nd line of the isomorphism in the screenshot, I see the that variable $C$ bound in the coend is used twice, but both times with the same variance. However, a coend requires bivariance.
Screenshot_20210524_170902.png

How do I understand this?

Reid Barton (May 24 2021 at 16:36):

Comparing Def 3.30 to the type signature above it, I guess Def 3.30 is wrong (the $\bullet$ should be some kind of cotensor, contravariant in the $C$ argument)...?

Bruno Gavranović (May 24 2021 at 17:00):

Hmm, I suppose so. I'll have to unpack what this really means. Even with this information, it's kind of strange to see both $C$'s appear on the left side of the hom...

Bruno Gavranović (May 24 2021 at 17:15):

On second thought, I'm not sure if that's correct, @Reid Barton . For instance, take a look at Prop. 3.2 in the same paper which defines Lenses.

Screenshot_20210524_180734.png

They use two covariant functors in two variables. One would think that's wrong as well, but I now think that that the actual contravariance in the first line of the coend arises as follows.

The functor $\mathcal{D}(- , T) : \mathcal{D}^{op}\to \mathcal{Set}$ is contravariant, and what happens is that we first apply $B$ to $\bullet$ to get a functor $(- \bullet B) : \mathcal{C} \to \mathcal{D}$ which we then "op", i.e. we take $(- \bullet B)^{op} : \mathcal{C}^{op} \to \mathcal{D}^{op}$ and plug it into the functor at the beginning of this paragraph.

Does that seem reasonable?

If so, then I am still pretty confused about the flow of information in a grate, and the lack of explicit variance in the paper isn't helping.

Reid Barton (May 24 2021 at 17:20):

I agree 3.2 is fine.

Reid Barton (May 24 2021 at 17:22):

But the types of a lens corresponding to Def 3.1 would be something like get :: s -> a, set :: (s, b) -> t. So here $\bullet$ seems to correspond to pairing (which makes sense, as it's covariant in both arguments). Whereas in the grates section, an arrow appears instead in ((s -> a) -> b) -> t--I mean the one between s -> a and b.

Bruno Gavranović (May 24 2021 at 17:24):

I'll think about what you posted, but in the meantime I'll post what I started writing:

I really don't know how to interpret the flow of information in grates causally. Maybe it helps if I write down how I think of lenses/prisms.

In lenses, we take an input, then save a state and produce an output. When we get a result from the environment, we use it and the state we saved to produce an update.

In prisms, we take an input, then save a state or produce an output (i.e. query the environment). Depending on what we did, we either use an output from the environment or the saved state.

But in grates, I don't know what the story is. (the short description in the paper does not really help)

Bruno Gavranović (May 24 2021 at 17:36):

Reid Barton said:

But the types of a lens corresponding to Def 3.1 would be something like get :: s -> a, set :: (s, b) -> t. So here $\bullet$ seems to correspond to pairing (which makes sense, as it's covariant in both arguments). Whereas in the grates section, an arrow appears instead in ((s -> a) -> b) -> t--I mean the one between s -> a and b.

Are you saying the $\bullet$ is also something like an exponential? This is pretty strange, especially since they don't refer it in the paper as such:
Screenshot_20210524_183648.png
i.e. they call the other thing the exponential, but not $\bullet$.

Reid Barton (May 24 2021 at 17:36):

Also, since the exponential $\{-, -\}$ of $\mathbf{C}$ has type $\mathbf{C}^\mathrm{op} \times \mathbf{C} \to \mathbf{C}$, the first argument of $\bullet$ also has to live in $\mathbf{C}^\mathrm{op}$ to match the general notion of an optic (2.1).

Reid Barton (May 24 2021 at 17:38):

$\bullet$ could be the exponential for example if $\mathbf{D} = \mathbf{C}$.

Reid Barton (May 24 2021 at 17:40):

It would be unusual to use a multiplication-like symbol like $\bullet$ for an exponential/cotensor type operation though. So I'm guessing there was some kind of confusion on the author's side.

Reid Barton (May 24 2021 at 17:40):

I haven't heard of grates before either, so I can't help you there.

Verity Scheel (May 24 2021 at 17:44):

In the programming sense of grates, ((s -> a) -> b) -> t can be read as “having a function giving an element b for a given accessor (s -> a) produces a new container t”. The idea is the accessors (s -> a) index the (fixed number of) positions in the container whose shape is shared by s and t. These end up having to be representable functors, I believe, because they are containers with a fixed shape. I’m not familiar with the categorical interpretations of optics I’m afraid.

Verity Scheel (May 24 2021 at 17:48):

https://r6research.livejournal.com/28050.html

Bruno Gavranović (May 24 2021 at 18:36):

Reid Barton said:

It would be unusual to use a multiplication-like symbol like $\bullet$ for an exponential/cotensor type operation though. So I'm guessing there was some kind of confusion on the author's side.

Perhaps someone from the profunctor gang can help us here? @Bryce Clarke , @fosco, @Mario Román, @Emily Pillmore ?

Bruno Gavranović (May 24 2021 at 18:38):

Nick Scheel said:

https://r6research.livejournal.com/28050.html

Thanks! This is one of those blog posts I've seen before, but they are very hard to understand for me...

Matteo Capucci (he/him) (May 24 2021 at 21:24):

Assume $\mathbf C = \mathbf D$ (thus $\bullet = \otimes$). Assume we choose a representative $(M, v, u)$ for a grate $\alpha : (A,S) \to (B,T)$. The view part $v$ is a map $A \to \{M, B\}$, while $u$ is a map $M \otimes T \to S$.
I can think of the view part as returning a bunch of $B$ s ( :bee: ), a bunch indexed by $M$. Then the update takes in an $M$ and a $T$. One can use the $M$ to access a $B$, using the map returned by $v$. Then you have a $B$ and a $T$ and you can do your thing $u$ to get an $S$

Matteo Capucci (he/him) (May 24 2021 at 21:29):

This also shows that $M$ is useless, since it can always be shortcut by evaluation. Indeed, the coend reduction shows that I can always assume $M=A$, basically, so that the update receives a map $f :\{A, B\}$ and a $T$. Then it evaluates $f$ with the state $a : A$ coming from outside, and finally gets its $B$.

Matteo Capucci (he/him) (May 24 2021 at 21:30):

So maybe an intuition for this is that the computation of $B$ is deferred: I never actually return $B$ to the environment, and I first ask for a continuation $T$. Once I have it, I compute $B$ and I go on with the second part of the computation.

Matteo Capucci (he/him) (May 24 2021 at 21:30):

This prevents the environment from yielding a continuation that actually depends on $B$, I think.

Matteo Capucci (he/him) (May 24 2021 at 21:31):

(I apologise for using a notational convention which probably different than everyone's here, certainly different from the categorical update paper)

Matteo Capucci (he/him) (May 24 2021 at 21:49):

I think this is what a grate looks like in string diagrams of closed categories:

Matteo Capucci (he/him) (May 24 2021 at 21:50):

pic

Matteo Capucci (he/him) (May 24 2021 at 21:50):

which is admittedly quite bad

Bruno Gavranović (May 24 2021 at 23:38):

Thanks Matteo! This is very helpful.

Matteo Capucci (he/him) said:

I can think of the view part as returning a bunch of $B$ s ( :bee: ), a bunch indexed by $M$. Then the update takes in an $M$ and a $T$. One can use the $M$ to access a $B$, using the map returned by $v$. Then you have a $B$ and a $T$ and you can do your thing $u$ to get an $S$

Hmm, so I am stuck here. "Then the update takes in a $M$". Where does that $M$ come from? Unlike with lenses or prisms, here in the forward pass we do not produce an $M$, but rather we produce a thing that takes in a $M$.

Bruno Gavranović (May 24 2021 at 23:47):

On that note, I'm not sure how to think of reparameterizations here. Say that your map $u : M \otimes T \to S$ is actually a composite $(r \otimes T) ; u'$ where $r : M \to M'$ and $u' : M' \otimes T \to S$

Then, since this is an optic, I expect to be able to slide that $r$ over to the forward pass and plug it into something that creates that $M$. But there's no such thing: the only thing created in the forward pass is $[M, B]$.

So this seems related to the question of variance from before, and I don't see a way how this can work.

Matteo Capucci (he/him) (May 25 2021 at 09:35):

Bruno Gavranovic said:

Thanks Matteo! This is very helpful.

Matteo Capucci (he/him) said:

I can think of the view part as returning a bunch of $B$ s ( :bee: ), a bunch indexed by $M$. Then the update takes in an $M$ and a $T$. One can use the $M$ to access a $B$, using the map returned by $v$. Then you have a $B$ and a $T$ and you can do your thing $u$ to get an $S$

Hmm, so I am stuck here. "Then the update takes in a $M$". Where does that $M$ come from? Unlike with lenses or prisms, here in the forward pass we do not produce an $M$, but rather we produce a thing that takes in a $M$.

Yeah, there's no $M$ coming around. But if it comes around we can do that. I know, it's a bit shaky :~

Matteo Capucci (he/him) (May 25 2021 at 09:38):

Bruno Gavranovic said:

On that note, I'm not sure how to think of reparameterizations here. Say that your map $u : M \otimes T \to S$ is actually a composite $(r \otimes T) ; u'$ where $r : M \to M'$ and $u' : M' \otimes T \to S$

Then, since this is an optic, I expect to be able to slide that $r$ over to the forward pass and plug it into something that creates that $M$. But there's no such thing: the only thing created in the forward pass is $[M, B]$.

So this seems related to the question of variance from before, and I don't see a way how this can work.

The action of such an $r$ on the forward part is $[r,B] : [M', B] \to [M,B]$, given by precomposition. So sliding here means that $v' ; [r,B] = v$ and $u = (r \otimes T) ;u'$, I think.

Bruno Gavranović (May 26 2021 at 19:47):

Yesterday @Matteo Capucci (he/him) and me had some discussions in private and I think we concluded that this definition makes sense only when $\mathcal{D} = \mathcal{C}^{op}$, otherwise the variances do not line up.

I'll just respond to the last message for completeness, to write some arguments I said.

Matteo Capucci (he/him) said:

Yeah, there's no $M$ coming around. But if it comes around we can do that. I know, it's a bit shaky :~

This really does not align with how I see optics: we need to say where the $M$ comes from. This is where the bivariance of the coend comes in.

Matteo Capucci (he/him) said:

The action of such an $r$ on the forward part is $[r,B] : [M', B] \to [M,B]$, given by precomposition. So sliding here means that $v' ; [r,B] = v$ and $u = (r \otimes T) ;u'$, I think.

This can be unpacked and it can be seen that there's no sliding happening here. To get the usual optic equivalence relation, we need just one equation, of the form where $r$ appears once on the left side, and once on the right.

Mario Román (Jan 27 2022 at 10:10):

@Bruno Gavranovic. I think this is just missing an op in the action $(\bullet) \colon \mathbf{C}^{op} \times \mathbf{D} \to \mathbf{D}$.
This way, you have two actions from a common category, $\mathbf{C}^{op}$. The coend computation remains unaltered.

I am quite sure I introduced that typo on the paper, so thank you very much for bringing this to my attention (please, do feel free to also email me for these :) I almost never open Zulip). As @Reid Barton said, using the bullet to denote a contravariant action is particularly confusing. I probably got confused when trying to copy the style of the rest of the definitions. In the previous "Profunctors and Traversals" the contravariance is right, so I must have introduced it when preparing the second paper.

The op will be added in the next version, the bullet will be changed to a more explanatory symbol. Thanks to both again!

Mario Román (Jan 27 2022 at 10:18):

grate.jpg

Bruno Gavranović (Jan 27 2022 at 10:42):

Ah, I was just thinking about this last night! Thanks, I'll have a look!

Bruno Gavranović (Jan 27 2022 at 10:43):

Mario Román said:

The op will be added in the next version, the bullet will be changed to a more explanatory symbol. Thanks to both again!

It's good to know that there's a next version planned. I'm looking forward to reading it

Bruno Gavranović (Jan 27 2022 at 12:02):

@Mario Román I am still confused about what grates do. I'm trying to compare them to lenses or prisms. If I take the the coend representation of a lens $\int^M \mathcal{C}(S, M \times A) \times \mathcal{C}(M \times B, T)$, and think of it operationally, it tells me that I take in an $S$, produce an $M$ and an $A$, and then when receiving a $B$, I take the previously produced $M$ too and use it to construct a $T$.

But for grates, it seems that the first map $\mathcal{C}(S, [C, A])$ doens't produce the residual $C$, it waits for it as an input (via the tensor hom adjunction). Is that correct? If the first map is waiting for an input $C$, that must mean that the second map produces it, and all-together it means that the operational view of a grate is different than that of a lens or a prism, since the information flows from the second map to the first.

Is what I'm saying correct?

Bruno Gavranović (Jan 27 2022 at 12:03):

All I'm trying to really do is have an operational, causal view of what a grate does. I.e. "where do I start", "what do I do" and "where do I end up". With lenses/prisms I start at $S$, (always/possibly) use it construct the residual, and end up at $T$. But with grates it seems different

Mario Román (Jan 28 2022 at 11:19):

Bruno Gavranovic said:

Mario Román I am still confused about what grates do. I'm trying to compare them to lenses or prisms. If I take the the coend representation of a lens $\int^M \mathcal{C}(S, M \times A) \times \mathcal{C}(M \times B, T)$, and think of it operationally, it tells me that I take in an $S$, produce an $M$ and an $A$, and then when receiving a $B$, I take the previously produced $M$ too and use it to construct a $T$.

But for grates, it seems that the first map $\mathcal{C}(S, [C, A])$ doens't produce the residual $C$, it waits for it as an input (via the tensor hom adjunction). Is that correct? If the first map is waiting for an input $C$, that must mean that the second map produces it, and all-together it means that the operational view of a grate is different than that of a lens or a prism, since the information flows from the second map to the first.

Is what I'm saying correct?

Sort of, yes. Although it is confusing for me to say that the second part of the optic produces that C. I think what you are saying describes a particular kind of grate where the second action is the left adjoint to the tensor: Lenses Flowing Back.

I can try to give an operational description of grates saying that they aggregate foci: Operational View of Grates. And if you want to see them as dual to lenses, the Van Laarhoven representation kind of says that: Van Laarhoven Lenses and Grates.

Matteo Capucci (he/him) (Jan 28 2022 at 16:25):

Yeah the Van Laarhoven representation helped me a lot to understand what grates do

Matteo Capucci (he/him) (Jan 28 2022 at 16:26):

Also the fact they are morphisms of 'Naperian containers', i.e. containers with a fixed shape. Together with the fact that $\times$, $+$ and $-^-$ combine to give polynomials, hence containers, made me realize grates are kind of degenerate dependent lenses

Bruno Gavranović (Jan 28 2022 at 22:17):

Grates are pretty mysterious! But becoming less so by the moment. Thanks @Mario Román for writing this up, it's immensely helpful.

I've got many thoughts about this, but I'll just give short remarks now and hopefully write something more concrete later.

And if you want to see them as dual to lenses

Prisms are often to considered "dual" of lenses. I suppose this is a "different duality". Prisms seem to be dual in what they do compared to lenses (+ instead of x), but how would you describe the grate duality?

the Van Laarhoven representation kind of says that: Van Laarhoven Lenses and Grates.

I find the remark about zipping interesting, but a bit confusing. Don't lenses also allow us to unzip? If we have a map $A \times A \to B$, we surely ought to be able to turn it to a map $S \times S \to T$?

Matteo Capucci (he/him) (Jan 29 2022 at 08:59):

Prisms are often to considered "dual" of lenses. I suppose this is a "different duality". Prisms seem to be dual in what they do compared to lenses (+ instead of x), but how would you describe the grate duality?

$+$ is dual to $\times$ as in 'reversing arrows' whereas exponentials are dual to $\times$ as in 'right adjoint'

Bruno Gavranović (Jan 30 2022 at 10:43):

Wouldn't the right adjoint of $\times$ give us linear lenses?

Matteo Capucci (he/him) (Jan 30 2022 at 13:12):

No, linear lenses are the same thing as lenses, just a different presentation that's possible when closed structure is around

Matteo Capucci (he/him) (Jan 30 2022 at 13:13):

Instead grates arise from using the closed structure as one of the actions itself

Bruno Gavranović (Jan 30 2022 at 15:47):

Right, that makes sense

Asad Saeeduddin (Jan 31 2022 at 19:17):

is it correct to say that grates represent the "powerhood" of an object? if so, is there some name for the analogous optic that represents the "copowerhood" of an object?

Asad Saeeduddin (Jan 31 2022 at 19:29):

in the case of both M = C = D = Set i believe this degenerates to the hom functor, which is perhaps what @Verity Scheel was pointing to