论文标题
依赖光学器件
Dependent Optics
论文作者
论文摘要
从混合光学元件到函子镜头的各种双向数据登录器可以在独特的框架依赖性光学元件中形式化。从两个索引类别开始，这些类别编码向前和向后方向允许的地图，我们定义了依赖性光学的类别，并在其具有共同点的假设下建立。索引类别的不同选择对应于不同的光学家族：我们讨论依赖性镜头和棱镜以及封闭的依赖光学元件。我们介绍了tambara表示的概念，并使用它来对光学类别类别进行违反函数进行分类，从而将光学的分配器编码推广到依赖性情况。
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.
