一句话：提出一个含对偶片段的依赖类型演算，并用去函数化/再函数化在函数式与面向对象风格间保持类型与语义地转换。
论文关注表达式问题：大多数类型容易扩展新的生产者或新的消费者，但难以同时扩展二者；这一区别对应数据导向/函数式程序与面向对象程序的不同可扩展性。依赖类型编程几乎只采用函数式模型，面向对象模型仍有待探索。作者不把依赖类型临时加到既有面向对象形式上，而是从第一性原理出发，利用对偶性从熟悉的数据导向语言出发，通过系统化的去函数化与再函数化推导其对偶片段。核心贡献是一个包含两个对偶语言片段的依赖类型演算，以及在这两个片段之间保持类型与语义的变换。作者实现了该语言与变换，并用其解释依赖类型编程中的多种构造如何作为一般对偶现象的特例。
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 general phenomenon of duality.
@article{paperbot2569,
title = {Deriving Dependently-Typed OOP from First Principles},
author = {David Binder and Ingo Skupin and Tim Süberkrüb and Klaus Ostermann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649846}
}