A wide variety of bidirectional data accessors, ranging from mixed optics to functor lenses, can be formalized within a unique framework-dependent optics. Starting from two indexed categories, which encode what maps are allowed in the forward and backward directions, we define the category of dependent optics and establish under what assumptions it has coproducts. Different choices of indexed categories correspond to different families of optics: we discuss dependent lenses and prisms, as well as closed dependent optics. We introduce the notion of Tambara representation and use it to classify contravariant functors from the category of optics, thus generalizing the profunctor encoding of optics to the dependent case.
翻译:包括混合光学与函子透镜在内的多种双向数据访问器,均可在一个统一框架——依赖光学——内形式化。从两个索引范畴出发(分别编码前向与后向允许的映射),我们定义了依赖光学范畴,并确定了其在何种假设下具有余积。不同索引范畴的选择对应不同的光学族:我们讨论了依赖透镜与棱镜,以及封闭依赖光学。我们引入Tambara表示的概念,并利用其对来自光学范畴的反变函子进行分类,从而将光学的对子编码推广至依赖情形。