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: Composing optics

Fabrizio Genovese (Apr 18 2020 at 13:33):

Very basic question: I have a lens (S,T) -> (A,B) and I'm depicting it as a comb. So the inside of the comb has a A wire on the left, and a B wire on the right. now suppose I have a function f:A -> B. I'd like to put this function inside the comb, that is, I'd like to use it to connect the A and the B wires. Is this possible using profunctor optics? I saw I can lift functions to getters and setters but I don't know if this helps me to achieve what I want :confused:

sarahzrf (Apr 18 2020 at 13:43):

yes it is! Hom is always a tambara module

EDIT: ...as long as you're considering your category with the same action on both sides of the Hom

Fabrizio Genovese (Apr 18 2020 at 13:45):

So I dn't need getters or anything?

Fabrizio Genovese (Apr 18 2020 at 13:45):

I can just pick my favourite function and stick it in?

sarahzrf (Apr 18 2020 at 13:45):

yup!

Fabrizio Genovese (Apr 18 2020 at 13:46):

Great!

Fabrizio Genovese (Apr 18 2020 at 13:46):

Thanks :D

sarahzrf (Apr 18 2020 at 13:46):

oh, but do note

sarahzrf (Apr 18 2020 at 13:46):

the result of the diagram will then itself be a morphism of the original category, rather than an optic or something

Fabrizio Genovese (Apr 18 2020 at 13:47):

Absolutely, that's precisely what I need :D

Fabrizio Genovese (Apr 18 2020 at 13:47):

The problem was that I was keeping to compose combs ad infinitum, but in the end a fucntion is exactly what I needed

Fabrizio Genovese (Apr 18 2020 at 13:48):

So I have a f: A -> B that represents my "initial policy" and I keep plugging it into lenses, and so on and so on updating the policy

Fabrizio Genovese (Apr 18 2020 at 13:48):

Also, am I wrong or I can view a function A -> B as a lens (A,B) -> (*, *) ?

Fabrizio Genovese (Apr 18 2020 at 13:49):

That is, I see f as a "trivial" comb with no inner wires whatsoever

sarahzrf (Apr 18 2020 at 13:51):

umm

sarahzrf (Apr 18 2020 at 13:51):

my initial impulse was that that was correct, but something sounds slightly off about it when i think about another kind of optic i use, so now i'm trying to resolve that—one sec

sarahzrf (Apr 18 2020 at 13:53):

wait, what is * there

sarahzrf (Apr 18 2020 at 13:53):

some kind of terminal object or what

Fabrizio Genovese (Apr 18 2020 at 13:53):

The terminal object, yes

sarahzrf (Apr 18 2020 at 13:53):

kk

Fabrizio Genovese (Apr 18 2020 at 13:55):

So I'd have:
view: $A \to *$, hence something useless
update: $A \times * \to B$, hence any function $A \to B$

Fabrizio Genovese (Apr 18 2020 at 13:56):

And then, at least in the case of lenses, composing a lens (X,Y) -> (A,B) with this effectively "closes" the comb

sarahzrf (Apr 18 2020 at 13:57):

oh sorry i was taking so long to reply—it's definitely true that for lenses we have A → B ~ (A, B) → (1, 1)

sarahzrf (Apr 18 2020 at 13:57):

but something definitely seems wrong about that when you generalize to other kinds of optics...

sarahzrf (Apr 18 2020 at 13:58):

or... maybe not... uh

Fabrizio Genovese (Apr 18 2020 at 13:58):

Well other optics seem to be combs with different shapes

Fabrizio Genovese (Apr 18 2020 at 13:59):

So probably if you compose that with something else you just maim your original shape in other abhorrent ways

sarahzrf (Apr 18 2020 at 14:00):

ok no yeah so im pretty sure this hinges on lenses being cartesian

sarahzrf (Apr 18 2020 at 14:00):

but with linear lenses, for example, you can still insert a morphism into a comb

sarahzrf (Apr 18 2020 at 14:00):

the morphism itself just doesnt count as an optic of the kind you describe

Fabrizio Genovese (Apr 18 2020 at 14:00):

Ok. So is there a "general" way to close combs?

Fabrizio Genovese (Apr 18 2020 at 14:01):

This actually entails another question: Are all optics combs of some sort?

sarahzrf (Apr 18 2020 at 14:01):

NO WAIT hold on im thinking about a thing

sarahzrf (Apr 18 2020 at 14:01):

ugh sorry

sarahzrf (Apr 18 2020 at 14:02):

ok actually if we have a morphism A → B that does give a linear lens (A, B) → (I, I), where I is the tensor unit rather than the terminal object

sarahzrf (Apr 18 2020 at 14:03):

makes sense :)

Fabrizio Genovese (Apr 18 2020 at 14:03):

Yes, that seems reasonable

Fabrizio Genovese (Apr 18 2020 at 14:03):

Which actually means that everything your comb can do is multiply that function by a scalar

Fabrizio Genovese (Apr 18 2020 at 14:04):

where a scalar is any morphism $I \to I$

sarahzrf (Apr 18 2020 at 14:04):

anyway yes i think it's fair to say that optics are combs in general

sarahzrf (Apr 18 2020 at 14:04):

you plug tambara module heteromorphisms into them if you want to close them

Fabrizio Genovese (Apr 18 2020 at 14:05):

sarahzrf said:

you plug tambara module heteromorphisms into them if you want to close them

That's a scary name :D

sarahzrf (Apr 18 2020 at 14:05):

;)

sarahzrf (Apr 18 2020 at 14:05):

how much do you know about profunctors

Fabrizio Genovese (Apr 18 2020 at 14:06):

I know that Hom is a profunctor. Then three years ago Neil Ghani explained ends and coends to me in a superclear way, it was amazing. But I forgot everything.

Fabrizio Genovese (Apr 18 2020 at 14:06):

Long story short assume you are speaking with a potato.

sarahzrf (Apr 18 2020 at 14:06):

:potato:

Fabrizio Genovese (Apr 18 2020 at 14:06):

Yes, that's me

sarahzrf (Apr 18 2020 at 14:06):

:(

sarahzrf (Apr 18 2020 at 14:07):

don't be so hard on yourself

sarahzrf (Apr 18 2020 at 14:07):

anyway

Fabrizio Genovese (Apr 18 2020 at 14:07):

What, being a potato is amazing. And as a bonus I taste great when fried!

sarahzrf (Apr 18 2020 at 14:07):

:D

Jules Hedges (Apr 18 2020 at 14:07):

Nice, the fact that functions $A \to B$ are the same as optics $(A, B) \to I$ is one of the magic tricks behind how open games work... happy to see this fact getting some love

sarahzrf (Apr 18 2020 at 14:07):

a profunctor C ⇸ D is a functor D^op × C → Set, or maybe a functor C^op × D → Set, depending on your convention

sarahzrf (Apr 18 2020 at 14:08):

the former one does look backward, but it also makes it so that C ⇸ D is the same as C → PSh(D) if you flip the args and curry

Fabrizio Genovese (Apr 18 2020 at 14:08):

Yup

sarahzrf (Apr 18 2020 at 14:09):

im more used to the former convention, but ill use the latter one for now i guess

Fabrizio Genovese (Apr 18 2020 at 14:09):

Both are fine for me

sarahzrf (Apr 18 2020 at 14:10):

so a good way to think about profunctors is that a profunctor P : C ⇸ D gives a notion of "heteromorphism" from objects of C to objects of D

sarahzrf (Apr 18 2020 at 14:10):

given A in C and B in D, think of P(A, B) as a kind of hom-set

Fabrizio Genovese (Apr 18 2020 at 14:10):

Yes, that's what you use to do profunctor collage too

sarahzrf (Apr 18 2020 at 14:10):

i thought i was talking to a potato

Fabrizio Genovese (Apr 18 2020 at 14:11):

I am! But I've been explained many things many times, so I have a shaky memory where every time you say something I may incorrectly recall something else

sarahzrf (Apr 18 2020 at 14:11):

kk

Fabrizio Genovese (Apr 18 2020 at 14:11):

Potato + random oracle maybe

Fabrizio Genovese (Apr 18 2020 at 14:11):

Anyway, I'm following up to now

sarahzrf (Apr 18 2020 at 14:11):

so i'll write f : A ~> B to mean f ∈ P(A, B)

Fabrizio Genovese (Apr 18 2020 at 14:11):

Ok

Fabrizio Genovese (Apr 18 2020 at 14:12):

It's literally like a hom but now hom is a P

sarahzrf (Apr 18 2020 at 14:12):

then, the action of P on morphisms gives "composition" of heteromorphisms with real morphisms

sarahzrf (Apr 18 2020 at 14:12):

and functoriality tells you that this is still associative and unital

Fabrizio Genovese (Apr 18 2020 at 14:12):

Yes. So in the trivial case of hom this is pre- and post- composing, but for profunctors it may be anything as long as it's compositional

sarahzrf (Apr 18 2020 at 14:13):

however, note that it doesn't give you composition of heteromorphisms with each other, even if that were well-typed cuz u had an endoprofunctor

sarahzrf (Apr 18 2020 at 14:13):

anyway this generalizes both presheaves and copresheaves

sarahzrf (Apr 18 2020 at 14:13):

a presheaf is a profunctor C ⇸ 1 in the convention i just picked

Fabrizio Genovese (Apr 18 2020 at 14:13):

sarahzrf said:

however, note that it doesn't give you composition of heteromorphisms with each other, even if that were well-typed cuz u had an endoprofunctor

I didn't notice that

Fabrizio Genovese (Apr 18 2020 at 14:14):

Yes

sarahzrf (Apr 18 2020 at 14:15):

so:

sarahzrf (Apr 18 2020 at 14:15):

(and now im just giving you the optics crash course ;) )

sarahzrf (Apr 18 2020 at 14:16):

given a monoidal category M, an action of M on some other category C is a strong monoidal functor M → End(C)

sarahzrf (Apr 18 2020 at 14:16):

a category equipped with an action of M is an M-actegory (not a typo)

Fabrizio Genovese (Apr 18 2020 at 14:17):

Okz

sarahzrf (Apr 18 2020 at 14:17):

so, fix some monoidal M. we'll think of it as a category whose objects are "contexts" to extend objects of other categories by

sarahzrf (Apr 18 2020 at 14:18):

so an M-actegory is a category whose objects can be enlarged by being placed into a context drawn from M

sarahzrf (Apr 18 2020 at 14:19):

if we have a profunctor P : C ⇸ D between M-actegories C and D

Fabrizio Genovese (Apr 18 2020 at 14:19):

So for each object C every element of m is giving me an "update" on C

sarahzrf (Apr 18 2020 at 14:20):

i dunno about an "update" as much as an "extension"—"update" sounds to me like it'd be a morphism

Fabrizio Genovese (Apr 18 2020 at 14:20):

So wait, who are the objects of End(C)? Morphisms C -> C for some C?

sarahzrf (Apr 18 2020 at 14:20):

oh!! sorry!!!

sarahzrf (Apr 18 2020 at 14:20):

End(C) is the category of endofunctors on C, monoidal under composition

sarahzrf (Apr 18 2020 at 14:20):

so this is a direct categorification of monoid actions on sets

Fabrizio Genovese (Apr 18 2020 at 14:21):

Oh, ok, the same one where monads live

Fabrizio Genovese (Apr 18 2020 at 14:21):

gr8

sarahzrf (Apr 18 2020 at 14:21):

yup

sarahzrf (Apr 18 2020 at 14:21):

in fact, lax monoidal functors turn monoids into monoids, so if you have a monoid object in M, you get a monad on any M-actegory :)

Fabrizio Genovese (Apr 18 2020 at 14:21):

cool

sarahzrf (Apr 18 2020 at 14:22):

now, if X is an object of M and A is an object of the M-actegory (C, F), i'll write X . A to denote F(X)(A)

Fabrizio Genovese (Apr 18 2020 at 14:23):

F is the functor M -> End(C)?

sarahzrf (Apr 18 2020 at 14:23):

yeah

Fabrizio Genovese (Apr 18 2020 at 14:23):

Ok

sarahzrf (Apr 18 2020 at 14:23):

so, if we have M-actegories C and D, and a profunctor C ⇸ D

sarahzrf (Apr 18 2020 at 14:24):

to equip P as a Tambara module is to give a way of lifting its heteromorphisms thru context extension

sarahzrf (Apr 18 2020 at 14:25):

that is, whenever we have f : A ~> B, we need to be able to get f' : X . A ~> X . B

Fabrizio Genovese (Apr 18 2020 at 14:25):

That's a very fancy way to say "monoidal products don't have to get in the way" :D

sarahzrf (Apr 18 2020 at 14:25):

and this needs to be subject to a whole boatload of diagrams

sarahzrf (Apr 18 2020 at 14:25):

well, monoidal product is only one very particular case of an actegory :)

Fabrizio Genovese (Apr 18 2020 at 14:25):

True

Fabrizio Genovese (Apr 18 2020 at 14:25):

Action is probably the right word

Fabrizio Genovese (Apr 18 2020 at 14:25):

but yes, I get what you are saying

sarahzrf (Apr 18 2020 at 14:25):

:)

sarahzrf (Apr 18 2020 at 14:26):

so then there's a key result which says

Fabrizio Genovese (Apr 18 2020 at 14:26):

So tambara means exactly that I can lift stupid morphisms to context-aware morphisms

sarahzrf (Apr 18 2020 at 14:26):

something like that?

sarahzrf (Apr 18 2020 at 14:26):

it's a kind of structure you can add to the profunctor

Fabrizio Genovese (Apr 18 2020 at 14:26):

Well they are well behaved wrt the action, so

Fabrizio Genovese (Apr 18 2020 at 14:27):

Oh, it's a structure

Fabrizio Genovese (Apr 18 2020 at 14:27):

so there's more than one way to do it

Fabrizio Genovese (Apr 18 2020 at 14:27):

ok

sarahzrf (Apr 18 2020 at 14:27):

welllllll, it's kind of like a functor's morphism mapping

sarahzrf (Apr 18 2020 at 14:27):

in the sense that it's technically structure, but there's usually really one obvious way to do it

Fabrizio Genovese (Apr 18 2020 at 14:27):

Yea, ok

sarahzrf (Apr 18 2020 at 14:28):

and plenty of mappings of objects have no morphism mapping that will work, so "being functorial" is also sort of a property

sarahzrf (Apr 18 2020 at 14:28):

many profunctors cannot be equipped as tambara modules

Fabrizio Genovese (Apr 18 2020 at 14:28):

Ok

sarahzrf (Apr 18 2020 at 14:28):

but anyway so

sarahzrf (Apr 18 2020 at 14:29):

[one of] the key result[s] is

sarahzrf (Apr 18 2020 at 14:29):

well, first: given M-actegories C and D, we have a general definition of a category of optics whose objects are pairs (S ∈ C, T ∈ D) in terms of coends

sarahzrf (Apr 18 2020 at 14:29):

and then:

Fabrizio Genovese (Apr 18 2020 at 14:30):

Yes, I remember that definition :D

sarahzrf (Apr 18 2020 at 14:31):

[one of] the key result[s] is: optics (S, T) → (A, B) are equivalent to transformations P(A, B) → P(S, T), natural in P, which ranges over Tambara modules C ⇸ D

sarahzrf (Apr 18 2020 at 14:31):

i.e.: an optic is something that can take context-liftable heteromorphisms A ~> B and lift them to ones S ~> T

Fabrizio Genovese (Apr 18 2020 at 14:32):

Oh!

Fabrizio Genovese (Apr 18 2020 at 14:32):

Is this the profunctor representation theorem in https://arxiv.org/pdf/2001.07488.pdf?

sarahzrf (Apr 18 2020 at 14:32):

yup!

Fabrizio Genovese (Apr 18 2020 at 14:33):

Great, so that theorem is exactly saying to me that I can close combs?

sarahzrf (Apr 18 2020 at 14:33):

exactly!

sarahzrf (Apr 18 2020 at 14:33):

well, one direction is saying that you can close combs with heteromorphisms of any tambara module

Fabrizio Genovese (Apr 18 2020 at 14:33):

$\ast \mathrm{\_}\ast$\_

sarahzrf (Apr 18 2020 at 14:34):

the other direction is saying that if you have a comb which you can close with heteromorphisms of any tambara module, that's an optic

Fabrizio Genovese (Apr 18 2020 at 14:34):

Yup. So all my headaches were due to the fact that I was working with the frong side of the theorem

Fabrizio Genovese (Apr 18 2020 at 14:35):

Cool :D

sarahzrf (Apr 18 2020 at 14:35):

:thumbs_up:

Fabrizio Genovese (Apr 18 2020 at 14:35):

Well, this was immensely helpful

Fabrizio Genovese (Apr 18 2020 at 14:35):

Thank you very much :D

Fabrizio Genovese (Apr 18 2020 at 14:35):

:heart: :heart: :heart:

sarahzrf (Apr 18 2020 at 14:35):

no problem!

sarahzrf (Apr 18 2020 at 14:35):

this is an explanation i've been rehearsing lol

sarahzrf (Apr 18 2020 at 14:35):

it's basically the amped-up version of what's going into my talk

sarahzrf (Apr 18 2020 at 14:36):

(in there im gonna talk about preordered monoids & stuff rather than monoidal categories, since everything im doing is depleted)

Fabrizio Genovese (Apr 18 2020 at 14:36):

Well, on behalf of the people(?) of the potato nation I say thank you

sarahzrf (Apr 18 2020 at 14:36):

you may also find it helpful to know that uh

sarahzrf (Apr 18 2020 at 14:37):

Tambara modules form the 1-cells of a bicategory Tamb whose objects are M-actegories

sarahzrf (Apr 18 2020 at 14:37):

this is the M-equivariant version of the bicategory Prof

Fabrizio Genovese (Apr 18 2020 at 14:38):

It's not immediately useful for me, but I'll try to not forget it in case I'll need it :D

sarahzrf (Apr 18 2020 at 14:38):

and Hom is the identity in Tamb just like it is in Prof

sarahzrf (Apr 18 2020 at 14:38):

it's always a tambara module C ⇸ C

sarahzrf (Apr 18 2020 at 14:39):

anyway here's a quick example of an action which you might find plausible that isn't just plain ⊗

sarahzrf (Apr 18 2020 at 14:40):

given a monoidal category C, let M be C × C, but put a monoidal structure on it by setting (A, B) ⊗ (A', B') = (A ⊗ A', B' ⊗ B)

sarahzrf (Apr 18 2020 at 14:40):

(this is actually a vast generalization of an example i use in my talk :wink:)

sarahzrf (Apr 18 2020 at 14:40):

(where the monoidal category in question is... the discrete monoidal category of strings)

sarahzrf (Apr 18 2020 at 14:41):

so here acting on something with a context can put something before it and after it

sarahzrf (Apr 18 2020 at 14:41):

which you can't do with just acting on the left, if your ⊗ is not braided

sarahzrf (Apr 18 2020 at 14:42):

uh, right, and let the action of M on C be given by (X, Y) . A = X ⊗ A ⊗ Y

Fabrizio Genovese (Apr 18 2020 at 14:43):

I'll be at your talk :D

sarahzrf (Apr 18 2020 at 14:43):

^_^

sarahzrf (Apr 18 2020 at 14:44):

hope you like program verification lol

Fabrizio Genovese (Apr 18 2020 at 14:48):

No, I hate it but I work with this stuff, so...

sarahzrf (Apr 18 2020 at 14:48):

hah

Morgan Rogers (he/him) (Apr 18 2020 at 16:31):

Fabrizio Genovese said:

Potato + random oracle maybe

GLaDOS!?

Morgan Rogers (he/him) (Apr 18 2020 at 16:32):

sarahzrf said:

(and now im just giving you the optics crash course ;) )

I was hoping the discussion would go this way, I hope this gives me the opportunity to ask some much more basic questions myself, like... what's a lens? And what's an optic? I've now read the nLab pages, but I want to hear what you would tell someone if they asked you about these things in person :wink:

sarahzrf (Apr 19 2020 at 01:07):

Morgan Rogers said:

sarahzrf said:

(and now im just giving you the optics crash course ;) )

I was hoping the discussion would go this way, I hope this gives me the opportunity to ask some much more basic questions myself, like... what's a lens? And what's an optic? I've now read the nLab pages, but I want to hear what you would tell someone if they asked you about these things in person :wink:

i would probably give the same lecture i just did above :mischievous:

Morgan Rogers (he/him) (Apr 19 2020 at 10:30):

I was hoping you could give me a little more insight into optics than the nLab's spiel, though:

Optics are constructions used in computer science as bidirectional data accessors. They include lenses and prisms, used to access, respectively, components of product data types and components of coproduct data types.

If there's no further insight to be had (is it just a cool name for typification of universal morphisms to limits/colimits?) then never mind

sarahzrf (Apr 19 2020 at 22:18):

i mean, the lecture i gave above involved considerably more than that...

Morgan Rogers (he/him) (Apr 20 2020 at 10:02):

Your lecture contains plenty of information, but as someone who didn't know any of the concepts beyond what a profunctor is beforehand, I'm trying to say "your lecture made this subject sound cool, but what is it about?" For example, what is the motivation for studying optics, and why is the representation theorem that was mentioned [one of] the key result[s]?
This is #learning: basic questions, after all, I'm not just being facetious!

Pastel Raschke (Apr 20 2020 at 10:24):

functional programming, database views and schemas: bidirectional data accessors, used to lift transformations of small things to transformations of bigger things the small things are inside

supervised learning (brendan fong): https://arxiv.org/abs/1903.03671

compositional game theory (jules hedges): https://arxiv.org/search/cs?searchtype=author&query=Hedges%2C+J

Pastel Raschke (Apr 20 2020 at 10:39):

note learners and open games are lenses, not optics in general (unless someone would like to correct me on that)

Jules Hedges (Apr 20 2020 at 10:40):

I'd like to correct you on that

Jules Hedges (Apr 20 2020 at 10:42):

Open games are not lenses. The other way round is true, but that's not conceptually very interesting (open games are indexed families of lenses plus a bit more, so a lens is an open game via a singleton family). Open learners turn out to be symmetric lenses which is an existing thing that turns out to be more or less spans of ordinary lenses (but with a slightly different composition). That trick fails for open games though

Jules Hedges (Apr 20 2020 at 10:42):

Also open games (and probably also open learners) can be easily generalised from lenses to optics. I now take that as the basic definition because it's so useful

Jules Hedges (Apr 20 2020 at 10:45):

In any case, the real motivation for studying optics is as bidirectional transformations of data. The other applications very much come out of nowhere. I wrote an extremely revisionist history here: https://julesh.com/2018/08/16/lenses-for-philosophers/

Pastel Raschke (Apr 20 2020 at 10:49):

those applications came out of category ether, but are now their own sources of motivation for people who may not be as interested in database schema transformation

sarahzrf (Apr 20 2020 at 23:38):

Morgan Rogers said:

Your lecture contains plenty of information, but as someone who didn't know any of the concepts beyond what a profunctor is beforehand, I'm trying to say "your lecture made this subject sound cool, but what is it about?" For example, what is the motivation for studying optics, and why is the representation theorem that was mentioned [one of] the key result[s]?
This is #learning: basic questions, after all, I'm not just being facetious!

right, sorry!

sarahzrf (Apr 20 2020 at 23:38):

i'll post more l8r, rn i have split attention

sarahzrf (Apr 20 2020 at 23:40):

o i see jules has already covered it actually :>

Jules Hedges (Apr 23 2020 at 16:50):

Yep, I'm referring to bayesian open games, and yep, it hasn't been written up for open learners