Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.
Metadata: arXiv. Abstracts retain their original authors’ rights.
In the conversation
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
Apologies for the jargon, but there isn't room in a comment box for a detailed explanation.
"The Essence of the Iterator Pattern" posed an open problem in type theory as to whether or not "lawful traversals", of type `∀ F:Applicative. (X -> F X) -> (B -> F B)` could appear for anything other than what is called a "finitary container"[1], B := ∃S. X^(P S) where the (P S) is a natural number (or equivalently a polynomial functor B := ∃n. C_n * X^n). Or rather, there was an open question as to what laws are needed so that "lawful traversals" would imply that B is a finitary container.
Eventually I came up with a fairly long proof[2] that the original laws proposed in "The…
Read the full comment
Essence of the Iterator Pattern" were in fact adequate to ensure that B is a finitary container. Mauro Jaskelioff[3] rewrote my proof in the language of category theory to be few lines long: use Yoneda lemma twice and a few other manipulations.
Anyhow, the upshot of reframing this as a simple argument in Category Theory meant that, with the help of James Deikun, I was able go generalize the argument to other types of containers. In particular I was able to device a new kind of "optic" for "Naperian containers" (also known as a representable functors) which are of the form B:=P->X (aka containers with a fixed shape).
Since then people have been able to come up with a whole host of classes of containers, optics for those classes, representations for those optics, and a complete characterization of operations available for those classes of containers, and how to make different container classes transparently composable with each other[4].
For example, we know that finitary containers are characterized by their traversal function (i.e the essence of the iterator pattern). Naperian containers are characterized by their zip function. Unary containers are characterized by a pair of getter and setter functions, something implicitly understood by many programmers. And so on.
I don't know if all this means that people should learn category theory. In fact, I really only know the basics, and I can almost but not quite follow "Doubles for Monoidal Categories"[5]. But now-a-days I have an "optical" view of the containers in, and forming, my data structures, slotting them into various named classes of containers and then knowing exactly what operations are available and how to compose them.
[0]https://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator...
[1]https://en.wikipedia.org/wiki/Container_(type_theory)
[2]https://github.com/coq-contribs/traversable-fincontainer
[3]https://arxiv.org/abs/1402.1699
[4]https://arxiv.org/abs/2001.07488
[5]https://golem.ph.utexas.edu/category/2019/11/doubles_for_mon...
There are infinitely many, so all is out, but the standard ones are covered here: https://oleg.fi/gists/posts/2017-04-18-glassery.html
Page 10 of this paper has a table with references to some more exotic optics, though it's going to be hard to parse without some category theory: https://arxiv.org/pdf/2001.07488.pdf
Plenty of serious researchers in top universities are studying the intersection of mathematics and functional programming, and I don't think that they're somehow not 'real mathematicians'.
Here's a paper by the author of this post, formalising a popular Haskell pattern in category theory: https://arxiv.org/abs/2001.07488
EDIT: switched to non-PDF link.
Fast compilation is important when compilation occurs at runtime, such as query compilers in modern database systems and WebAssembly virtual machines in modern browsers.
The recent discovery of the Spectre and Meltdown attacks represents a watershed moment not just for the field of Computer Security, but also of Programming Languages.
This paper presents a personal view of the evolution of six generations of Smalltalk in which the author played a part, starting with Smalltalk-72 and progressing through Smalltalk-80 to Squeak and Etoys.