Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Judging by Prop 3.1 of Lenses, fibrations and universal translations, lenses are just algebras for our possibility monad, at necessity and possibility.
I’m told this is good. But I don’t have access at the moment: https://dl.acm.org/citation.cfm?doid=3191697.3191718
and of course we should cite the paper by Mitchell that started the discussion.
Given
necessity comonad : possibility monad = jet comonad : infinitesimal disk bundle monad,
and since lens (in computer science) (at least lawlike ones) seem to be algebras for the possibility monad, what are algebras for the infinitesimal disk bundle?
We’d need, over and a map .
Oh, is it just the constants . But then what’s that exciting about lenses?
That paper Lenses, fibrations and universal translations continues that when the of views is such that is split epi then a lens just is a projection.
So people look at more general situations?
Added a new article
Another one
Added a paragraph in Generalizations about delta lenses which are a direct generalization of lenses satisfying laws. Also mentioned update-update lenses defined by Ahman-Uustalu, which are equivalent to cofunctors. Added four additional references to recent papers by Spivak, Johnson-Rosebrugh, Ahman-Uustalu, and myself.
I hope to come back and add more recent references, as well as add further generalizations including symmetric lenses.
Thanks for the additions, Bryce. You’ll see that itex oddly renders adjacent letters wrongly, so instead of you need , using a space between the letters.
At some point I should get a clearer understanding of what these devices are for.
At some point I should get a clearer understanding of what these devices are for.
Me, too. Ideally a perusal of the Idea-sections of this and related entries would clarify it. Currently it remains a little murky.
Re #13 and the meaning of lenses, perhaps David Spivak’s comparison of them to bundles (here) is useful.
Thanks for this pointer to Spivak 19! I have now read through it and found it useful.
But in that note, he is effectively saying that lenses are but a weird way to talk about a small fragment of (the categorical semantics of) dependent type theory.
Strong criticism of the concept of lenses on slide 14 (p. 62 of 144):
kinda weird quite floppy Totally not functorial, anything goes.
People use lens laws to try to mitigate the floppiness The lens laws are too strong, but without them lenses are too floppy.
Quite a devastating assessment.
Then his proposed rectification of the situation is insightful. But let’s see what the proposal really is: He speaks of “bundles” and uses fiber bundles as motivation and for illustration, but the local triviality condition on a fiber bundle is decidedly not part of the story here: His “bundles” are “display maps”.
This becomes fully manifest on slide 22, p. 95 of 144, where he asks
What do we really need to create a lens-like world?
and his answer is effectively: a hyperdoctrine of dependent types!
Moreover, he explains, the lenses are but the “in-dependent” types among these dependent types (i.e. those whose display maps are trivial as bundles).
I admit that this one talk note by David Spivak is the only account of lenses that I have really read so far. But if this is anything to go by, then lenses are a red herring and people should be looking to dependent type theory and/or its categorical semantics.
Which he’s looking at in that blog post I mentioned. Again the extra cases of his jump monad seem to concern fragments of dependent type theory.
There is a recent blog post by Jules Hedges which discusses “dependent lenses”, which are essentially what David Spivak is introducing in those slides. Basically, a dependent lens should be thought of as a morphism between polynomial functors which are “one variable”.
I have added the following paragraph to the Idea-section:
An insightful explanation and critique of the concept of “lenses” is offered in Spivak ACT19, where it is argued that the notion may and should be regarded as a small fragment (namely that of trivial display maps) of the general notion of (categorical semantics for) dependent types, such as discussed at hyperdoctrine and related entries.
By the way, it’s a bit sad that the entry lens (computer science) doesn’t even define the morphisms between lenses. Maybe whoever thinks about making any further addition to the discussion of lenses/optics on the Lab should first take 10 minutes to bring this central entry here into some minimum shape. (Myself, I really need to look into something else now…)
Now I’d be interested in seeing Spivak critique the notion of “optic”. ;-) Did he write about it?
One way to think about it is this:
Do we expect that the established vocabulary of category theory/type theory is incomplete? Do we expect that there are fundamental notions still to be formulated?
I’d expect that the answer is clearly No. While I can’t prove this, it means that if somebody comes along and initiates an industry on a seemingly new abstract category-theoretic concept not seen before, some sceptical care may be needed to avoid that the wheels be re-invented, and maybe not fully roundly shaped.
Indeed, the time-honored way to “apply category theory” goes the other way around: Instead of proliferating concept formation, one finds ever more ways of understanding the ever growing plethora of concepts that people invent as all being examples of a small number of universal constructions in category theory. Everything is a Kan extension, etc., whence the infamous phrase of “An X is just a B in C!” where “X” is from a plethora of concepts that people invent, while “B” is a basic concept of category theory, and “C” is the ambient category.
That’s what Spivak did here to lens theory: “A lens is just a trivial display map.”
Since we have just gained a new contributor in Bryce, who is a really nice guy, can we not just dump on the topic of his contributions?
whence the infamous phrase of “An X is just a B in C!” …. That’s what Spivak did here to lens theory: “A lens is just a trivial display map.”
It is all well and good in hindsight, but as you said on Twitter, Urs, the idea seems obvious in hindsight, but the process of arriving at it, especially in the context of the messy world of professional programmers and computer language designers, is non-trivial. And it goes the other way: to encourage the uptake of category-theoretic framework here, we don’t want another “A monad is a just a monoid in the category of endofunctors” moment. This is applied mathematics, and the proponents of the abstract picture need to phrase things in a way that makes sense for people at the coal-face, for whom a monoid is a scary object. Forget about “display maps” in a blah-category.
Personally, I find the emergence of cofunctors really intriguing, they are not what one would expect coming from pure category theory. And we can get to the point of including all the information on the page, including morphisms of lenses, when we get there. We all have unfinished pages lying around, and Bryce seems keen to contribute, so I don’t think the page is going to stay incomplete (which is, of course, the permanent state of the whole nLab!) for long.
Not sure what #25 is about – I am not reacting to anything Bryce said or wrote, nor have I even followed that.
Instead, I am reacting to the observation in #12, #13 that our entry didn’t explain the Idea of lenses, and then to mattecapu in #22 seemingly suggesting that Spivak’s take on it is not so relevant. I explained why it looks squarely relevant to me, and I stand by that.
(It seems a weird suggestion to me that the objective clarification of a topic on the Lab should be conditioned on whether a basic category-theoretic term might “scare” a reader.)
If anyone likes to lay out why Spivak’s POV on lenses is suboptimal and write a paragraph of an Idea-section for us on what they think the good perspective on lenses really is, I’d appreciate it and will read it with interest. Any such conceptual discussion – either way – is currently missing in our Lab entries (and in related entries on “optics in computer science”).
mattecapu in #22 seemingly suggesting that Spivak’s take on it is not so relevant.
If this is what I communicated, I apologise, since that’s not my opinion. His is certainly an important and far-reaching realization!
What I’m saying is, it doesn’t tell the full story. There’s a whole different direction of what it means to be a lens (arguably, a more natural one from the point of view of who created lenses in the first place) that Spivak’s generalisation misses. At least there’s an attitude to the concept of lens which can’t be reduced to ’a small fragment […] of the general notion of (categorical semantics for) dependent types’.
Also why go all the way to dependent types? Spivak’s proposed generalisation only needs an indexed category to work, no hyperdoctrinal facilities needed.
Might you have the energy to write a paragraph explaining “what it means to be a lens”, to you?
Regarding morphisms of lenses (and optics): they are the morphisms in their respective categories.
Of course one can come up with a ’2’-categorical augmentation. One direction is Myers and Spivak’s notion of ’charts’ between lenses which turns lenses into double category. Another is that of parametrised optics. A third is given by making the coend defining optics into a 2-coend, thereby turning the quotient into a groupoid.
I might write about this in the coming days.
There have been many interesting perspectives shared in this discussion, and I don’t have the energy to reply to them all. However, let me instead share some semblance of a plan for future improvements I hope to make to this page.
Add a Properties section which includes statements such as “lenses as algebras for a monad” and “lenses as algebras for a comonad” together with proof sketches and references for these results.
Perhaps a section titled “Categories of lenses” with two subsections titled Lenses as objects (where we look at lenses over a base and morphisms between them) and Lenses as morphisms where we can put the current material on the category .
Break the Generalizations section into two subsections titled Lenses without laws and Lenses with laws. These are both two very important threads, yet are quite different in flavour. For instance, Spivak’s generalisation, lenses in monoidal categories, bimorphic lenses, and optics all fall into the former category, while delta lenses, cofunctors, c-lenses (or split opfibrations) all fall into the latter.
Reorganise the references section, provide a short synopsis of each of the items, possibly separate into published papers and more informal work like blog posts and talk slides.
Thanks. Just to highlight that the question we bystanders have is more conceptual than technical: We are wondering: Why is the definition of lenses what it is? Why is it necessary to consider this definition? What is it good for? Why should one care?
(If we reject Spivak’s answer as inadequate, then I really don’t know the answer to these questions and would like to know.)
What might help is the statement of some property/theorem that holds for lenses, and then a list of examples that shows that this property/theorem subsumes a bunch of specific phenomena that arise in application or that are otherwise known to be relevant.
@BryceClarke that’s a very good plan!
Might you have the energy to write a paragraph explaining “what it means to be a lens”, to you?
Yes, I will. There’s already a bit of this in under ’Idea’, I’ll expand it. I’ll probably split it between this page and ’optic’, since not everything I say might be appropriate for vanilla lenses.
My outsider perspective is that the definition is like it is, because this is something that comes from functional programming and is really a nitty-gritty implementation thing, not necessarily just pure theory that happens to be nice. It’s like worrying about implementation details of a real-world type theory-based proof assistant, rather than just saying “it’s all just MLTT, what’s the matter?”
David, I wonder if you think about the implications of what you are saying in #25 and #33. Essentially you are claiming in #33 that lenses are not a theoretically worthwhile concept, and in #25 that those who publish about the subject are feeble applied mathematicians who must be protected from being confronted with their proper theoretical discussion. You probably mean to do good, but it seems counterproductive.
I was happy to learn from Spivak that lenses are but trivial dependent types, because that immediately gives them a strong theoretical status that immediately explains why they would come up in functional programming and immediately connects them right there to the category/type theoretic foundations whose myriad of incarnations we we are discussing in a multitude of guises here on the Lab. For instance, following Spivak I would be able to immediately recognize lenses in, say proper equivariant -bundle theory, and could maybe fruitfully interact with the lens community.
But if you are right in #33 then this ought not to happen, then lenses are but a random hack which I’d better ignore.
I think I’m not getting across what I’m trying to convey, never mind me.
Added a Properties section with three basic results in the literature: that lenses are algebras for a monad, that lenses in are equivalent to product projections, and that lenses in a Cartesian closed category are equivalent to coalgebras for a comonad.
Also tidied up the Definition section with definition and remark environments (there was previously an issue with the labeling) and also reorganized the references into two broad classes: papers and other material. The should be sorted in chronological order, but if the list keeps growing it may be better to sort by kind of lenses they discuss. I added in some missing doi links as well.
EDIT: duplicate comment
EDIT: duplicate comment
@Bryce
if you do one edit with a comment, then go and do some tweaking, you can leave the comment section blank, and make some edits to the auto-generated comment here to reflect any additional information you feel needs to be included.
Thanks. I think the issue was the original edit didn’t compile, and it took a couple of edits to fix, but I wasn’t aware this was also sending duplicate comments to the forum. I will be aware of this for the future!
@Bryce is Proposition 3.1 replacing the comment after Definition 2.1 regarding lenses as algebras of the ’possibility monad’? If yes I’ll delete it in favor of the more organized version.
Shifted the remarks which previously followed the definition in reply to #41. Made a separate section title for the category whose morphisms are lenses. Split the Generalizations section into two subsections for lenses with laws and lenses without laws; there still needs to be more examples placed here from the literature.
Hi Everyone,
I hope I’m not stepping on anybody’s toes with this edit, but I quite drastically re-wrote the introduction. I tried to remove the attitude (that there is something wrong or useless about the notion of lens), and to make clear right away that the name is used for two very different threads of thought — the lawful and lawless (aka polymorphic) lenses.
I didn’t add any math, though I would like to come back and explain how David Spivak’s generalized lenses work because I think they are very nice. Hopefully someone with a more enclycopaedic knowledge of the topic can come and organize all the various definitions which have been floating around — there are a lot.
I also separated the references to my and David’s (and Nelson Niu’s) books (since they are now separate books) which use (lawless, generalized) lenses for categorical systems theory.
Cheers, David
Thanks for this, David. (Lots of Davids around here.)
I wonder, is there any way to make the following less vague?:
situations where some structure is converted to a different form – a view – in such a way that changes made to the view can be reflected as updates to the original structure.
It seems to cover so much – representing a battlefield on a map, representing temperature by the height of a column,… Is there a distinctively lens-like situation?
linked Richard J. Wood
added hyperlink to categorical systems theory
In the Proposition (here) stating the equivalence of lenses to costate coalgebras, I have:
added the qualifier “well-behaved”,
added proper attribution to O’Connor,
fixed the grammar and adjusted wording for readability.
The list of references on this point I have expanded and then moved to a subsection “References – Relation to the costate comonad” (now here).
Finally I have added mentioning of this fact already in the third paragraph of the Idea-section (here).
While at it, I have tried to adjust the very first paragraph of the Idea-section for clarity and usefulness.
I have re-written the discussion of lenses as -modales (here),
observing how the proof of monadicity by Johnson, Rosebrugh & Wood 2010 generalizes from to any topos
and remarking that the monad in question is the possibility monad
and that the conclusion — namely that lawful lenses in with inhabited view are equivalent to plain objects in — is epistemically the statement (here) that “possibility-modales are the potentials”
I have touched the wording of the first couple of paragraphs of the Idea-section (here).
In particular, I removed the pointer to a blog post advertized as providing earlier references and instead added these earlier references:
Frank J. Oles, A category-theoretic approach to the semantics of programming languages, Syracuse University (1982) [pdf]
Frank J. Oles, Type algebras, functor categories and block structure, Algebraic methods in semantics (1986) 543–573, Daimi Report No. 156 (1983): [doi:10.7146/dpb.v12i156.7430, pdf]
Martin Hofmann, Benjamin Pierce, p. 12 in: Positive Subtyping, Information and Computation 126 1 (1996) 11-33 [doi:10.1006/inco.1996.0031]
(But I haven’t hunted down the relevant page number in Oles’ texts yet.)
added a remark (below the main definition) that Hofmann & Pierce 1996 thought of (what later came to be called) lenses as describing aspects of object-oriented programming.
Is it clear that was actually a typo, and not a reference to actegory? (In either case, the sentence should be clarified.)
1 to 60 of 60