一句话:用 Yoneda 引理从具体 getter/setter 表示推导 profunctor optics,阐明 lens/prism 的可组合表示。
本文是一篇 functional pearl,讨论 profunctor optics——一种可组合地表示双向数据访问器(如 lens 及其对偶 prism)的方式。Profunctor 表示利用高阶函数与高阶 kind 的类型构造器类,但其与常见的 getter/setter 具体表示之间的关系并不显然。作者从具体表示出发推导出 profunctor 表示,说明这一推导本质上是 Yoneda 引理的一个相当直接的运用。通过该推导,论文厘清了两种表示之间的对应关系,帮助读者理解 profunctor optics 的可组合性;反过来,也为理解范畴论中重要的 Yoneda 引理提供了直觉。
Profunctor optics are a neat and composable representation of bidirectional data accessors, including lenses, and their dual, prisms. The profunctor representation exploits higher-order functions and higher-kinded type constructor classes, but the relationship between this and the familiar representation in terms of "getter" and "setter" functions is not at all obvious. We derive the profunctor representation from the concrete representation, making the relationship clear. It turns out to be a fairly direct application of the Yoneda Lemma, arguably the most important result in category theory. We hope this derivation aids understanding of the profunctor representation. Conversely, it might also serve to provide some insight into the Yoneda Lemma.
@article{paperbot279,
title = {What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)},
author = {Guillaume Boisseau and Jeremy Gibbons},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236779}
}