从第一性原理推导依赖类型面向对象编程——附补充附录的扩展版
Deriving Dependently-Typed OOP from First Principles -- Extended Version with Additional Appendices
AI总结：
针对依赖类型编程仅遵循函数式模型、缺乏面向对象范式探索的问题，本文基于对偶性原理，从面向数据语言出发通过去函数化与再函数化推导得出包含双对偶片段的依赖类型演算，实现了语言及转换并阐释了相关构造的对偶性本质。
摘要：
表达式问题描述了这样一种情况：大多数类型可以轻松通过生成该类型的新方式或消费该类型的新方式进行扩展，但无法同时通过两者扩展。例如，当抽象语法树被定义为代数数据类型时，可以轻松添加新的消费器（如print或eval）来扩展，但添加新的构造子则需要修改所有现有的模式匹配。表达式问题是阐明函数式或面向数据的程序（可通过新消费器轻松扩展）与面向对象程序（可通过新生成器轻松扩展）之间差异的一种方式。这种可通过新生成器或新消费器扩展的程序之间的差异，在依赖类型编程中同样存在，但有一个核心区别：依赖类型编程几乎完全遵循函数式编程模型而非面向对象模型，这使得编程语言领域中一个有趣的空间尚未被探索。在本文中，我们通过对偶性原理从第一性原理出发进行推导，以此探索依赖类型面向对象编程领域。也就是说，我们并非以临时的方式为现有的面向对象形式体系添加依赖类型，而是从一种熟悉的面向数据语言出发，通过系统地使用去函数化（defunctionalization）和再函数化（refunctionalization）推导出其对偶片段。我们的核心贡献是一种包含两个对偶语言片段的依赖类型演算。我们提供了这两个语言片段之间保持类型和语义的转换：去函数化和再函数化。我们已经实现了该语言和这些转换，并借助这一实现解释了依赖类型编程中的各种构造可以被解释为对偶现象的特殊实例的多种方式。
英文摘要：
The expression problem describes how most types can easily be extended with new ways to produce the type or new ways to consume the type, but not both. When abstract syntax trees are defined as an algebraic data type, for example, they can easily be extended with new consumers, such as print or eval, but adding a new constructor requires the modification of all existing pattern matches. The expression problem is one way to elucidate the difference between functional or data-oriented programs (easily extendable by new consumers) and object-oriented programs (easily extendable by new producers). This difference between programs which are extensible by new producers or new consumers also exists for dependently typed programming, but with one core difference: Dependently-typed programming almost exclusively follows the functional programming model and not the object-oriented model, which leaves an interesting space in the programming language landscape unexplored. In this paper, we explore the field of dependently-typed object-oriented programming by deriving it from first principles using the principle of duality. That is, we do not extend an existing object-oriented formalism with dependent types in an ad-hoc fashion, but instead start from a familiar data-oriented language and derive its dual fragment by the systematic use of defunctionalization and refunctionalization. Our central contribution is a dependently typed calculus which contains two dual language fragments. We provide type- and semantics-preserving transformations between these two language fragments: defunctionalization and refunctionalization. We have implemented this language and these transformations and use this implementation to explain the various ways in which constructions in dependently typed programming can be explained as special instances of the phenomenon of duality.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
