Towards a unified framework for Functional Optics implementation and verification

这个项目属于EPSRC编程语言研究领域的福尔斯。模块化是好的软件工程的核心。在结构化数据的背景下，模块性通常来自复合数据类型，即由基本形状（和、积、映射）组成的数据类型。然而，尽管复合数据类型是模块化的，但操作它们并不那么直接：对于给定的复合数据类型，通常需要逐个编写组合子。近年来，已经出现了一类工具，以通用的方式解决这个问题，称为函数引用或函数光学。从双向编程文献[1]中的透镜的简单概念概括，功能光学定义了组合子族以查询，访问和修改某些基本形状[3][9]。它们共同概括了一些著名的编程模式，如迭代器[2]和折叠[4]，并允许它们以任意方式组合，同时确保类型安全。这些工具在函数式程序员的工具箱中变得越来越常见，特别是在Haskell中，它们的大部分开发都发生在那里。尽管光学在软件开发领域很受欢迎，但学术界对光学的关注却很少。该项目旨在通过为光学研究提供理论基础和基础来缩小这一差距。利用范畴论的先进推理技术[7][6]和最近对光学代数结构的见解[8][5]，该项目旨在开发一个用于指定光学的通用代数框架，以及光学良好性定律的统一描述，以允许对用光学构造的程序进行模块化验证。它的目标是为光学和使用它们的程序的推理提供一个基础，该项目涉及EPSRC编程语言领域，并与其目标保持一致，以帮助开发可靠和强大的软件系统。该项目将在计算机科学系的Jeremy Gibbons教授的监督下实现。参考文献[1] J. Nathan Foster et al.“Combinators for Bi-directional Tree Transformations：A Linguistic Approach to the View Update Problem”.在：SIGPLAN Not. (Jan. 2005年）。[2]杰里米·吉本斯和布鲁诺·塞萨尔·多斯桑托斯·奥利维拉。迭代器模式的本质在：Journal of Functional Programming 19.3-4（2009），pp. 377-402. DOT：10.1017/S0956796809007291。网址：http：//www.comlab.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf。[3]爱德华·克梅特Haskell透镜库。网址：https://hackage.haskell.org/package/lens。[4]爱德华·克梅特Haskell透镜库：Control.Lens.Fold.网址：https://hackage.haskell.org/package/透镜/docs/Control-透镜-Fold.html。[5]巴托什·米莱夫斯基Profunctor Optics：The Categorical View. URL：https://bartoszmilewski.com/2017/ 07/07/profunctor-optics-the-categorical-view/. [6]nLab：Coalgebra.网址：https://ncatlab.org/nlab/show/coalgebra。[7]nLab：结束。网址：https://ncatlab.org/nlab/show/end。[8]马修·皮克林杰里米·吉本斯尼古拉斯·吴Profunctor Optics - Modular Data Accessors. 2017. [9]PureScript透镜库。网址：https://pursuit.purescript.org/packages/purescript-profunctor-lenses/2.2。0.

This project falls within the EPSRC Programming Languages research area.Modularity is at the heart of good software engineering. It allows for efficient software development, and enables reasoning about correctness at scale.In the context of structured data, modularity usually comes from compound data types, i.e. data types made of the composition of elementary shapes (sums, products, mappings). However, even though compound data types are modular, manipulating them is less directly so: one usually needs to write combinators on a case-by-case basis for a given compound datatype.The recent years have seen the development of a class of tools to solve this problem in a generic way, called functional references, or functional optics. Generalizing from the simple idea of a lens from the bidirectional programming literature[1], functional optics define families of combinators to query, access and modify certain elementary shapes[3][9]. Together they generalize well-known programming patterns such as iterators[2] and folds[4], and allow them to be composed in arbitrary ways while ensuring type safety.These tools are becoming more and more common in the functional programmer's toolbox, especially in Haskell where most of their development has taken place. Despite their popularity in the software development world, optics have yet received little attention from the academic world. This project will aim at closing this gap by bringing theoretical grounding and foundation to the study of optics.Using advanced reasoning techniques from category theory[7][6] and recent insights into the algebraic structure of optics[8][5], this project aims at developing a generic algebraic framework for specifying optics, as well as a unified description of optics well-behavedness laws to allow for modular verification of programs constructed with optics. Its objectives are providing a base for reasoning about optics and programs that use them, in addition to enabling specification of both efficient and correct implementations of those combinators.This project relates to the EPSRC Programming Languages area and aligns with its objective to help development of reliable and robust software systems.This project will be realized under the supervision of Prof. Jeremy Gibbons at the Department of Computer Science of the University of Oxford.References[1] J. Nathan Foster et al. "Combinators for Bi-directional Tree Transformations: A Linguistic Approach to the View Update Problem". In: SIGPLAN Not. (Jan. 2005).[2] Jeremy Gibbons and Bruno César dos Santos Oliveira. "The Essence of the Iterator Pattern". In: Journal of Functional Programming 19.3-4 (2009), pp. 377-402. DOT: 10.1017/S0956796809007291. URL: http: //www.comlab.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf.[3] Edward Kmett. Haskell Lens library. URL: https://hackage.haskell.org/package/lens.[4] Edward Kmett. Haskell Lens library: Control.Lens.Fold. URL: https://hackage.haskell.org/package/ lens/docs/Control-Lens-Fold.html. [5] Bartosz Milewski. Profunctor Optics: The Categorical View. URL: https://bartoszmilewski.com/2017/ 07/07/profunctor-optics-the-categorical-view/.[6] nLab: Coalgebra. URL: https://ncatlab.org/nlab/show/coalgebra.[7] nLab: End. URL: https://ncatlab.org/nlab/show/end.[8] Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. "Profunctor Optics - Modular Data Accessors". 2017.[9] Purescript Lens library. URL: https://pursuit.purescript.org/packages/purescript-profunctor-lenses/2.2. 0.