本文提出了一种新颖的方法，从第一原理推导出依赖类型的面向对象编程（OOP）。
题为“从基本原理推导依赖类型 OOP”，由德国图宾根大学和德国 IPAI 的 Aleph Alpha Research 的 David Binder、Ingo Skupin、Tim Süberkrüb 和 Klaus Ostermann 撰写。该论文探讨了依赖类型面向对象编程 (OOP) 的概念，以及如何使用二元性、去功能化和重新功能化的原理系统地推导它。
现有OOP问题：
大多数类型能够通过新的方式生成类型、或使用类型来轻松扩展，但不能同时实现两者。体现了类型的生产和消费两难：
- 函数式编程在扩展类型等消费者方面是易用的，但是创建或生产新类型不容易。
- 而 OOP 在扩展新类型的生产者方面是易用的，但是消费使用不易用。
突破口：
- 依赖类型编程：主要遵循函数式编程模型的依赖类型编程可以从结合面向对象原则中受益。函数式编程在类型依赖方面向OOP学习。
函数式编程 vs. 面向对象编程：
- 本文将函数式编程定义为使用代数数据类型和模式匹配进行的编程，
- 而面向对象编程则是针对接口进行编程来定义的，对应于类型理论中的共数据和共模式匹配概念。
使用对偶原理从第一原理推导出依赖类型的面向对象编程领域。
- 也就是说，我们不会临时扩展现有的具有依赖类型的面向对象形式，
- 而是从熟悉的面向数据语言开始，通过系统地使用去函数化和重新函数化来获得其对偶片段。
去函数化和重新函数化：
用于系统地从函数性语言片段派生出面向对象语言片段。
- 去函数化通过用数据类型构造函数和顶级应用函数替换高阶函数来消除高阶函数，
- 而重新函数化则重新引入高阶函数。
作者从熟悉的面向数据语言入手，通过系统地使用去函数化和重函数化，推导出其对偶片段。
- 核心贡献是一个包含两个对偶语言片段的依赖类型演算。
- 论文提供了在去函数化和重函数化这两个语言片段之间的类型和语义保留转换
作者已经实现了这一语言及其转换，并利用这一实现解释了依赖类型编程中的构造如何被视为对偶性的特殊实例。
方法论：对偶原理:
- 对偶原理指的是通过某种对应关系,将一种数学结构或概念转化为另一种结构或概念的方法. 如果A的对偶是B,那么B的对偶也是A.
- 几何中的应用:在射影平面上,如果将一个定理中的"点"和"直线"互换,得到的新命题仍然成立,这就是射影几何中的对偶原则
对偶原理是数学中的一个重要概念，特别是在布尔代数和集合论中：
在布尔代数中的应用：
- 在布尔代数中，语句的对偶是通过将 AND (•) 与 OR (+) 互换，将 0 与 1 互换而得到的。
- 例如，如果 A • 0 = 0 为真，则其对偶 A + 1 = 1 也为真。
集合论应用：
- 在集合论中，并集（∪）与交集（∩）互换，全集（U）与零集（∅）互换。
- 例如，A ∪ (B ∩ A) = A 的对偶是 A ∩ (B ∪ A) = A
对偶原理的意义在于：
- 为原问题提供了一个下界,有助于评估解的质量。
- 在某些情况下,求解对偶问题比原问题更容易。
- 为解决复杂优化问题提供了理论基础和实用工具
对偶原理的重要性在于它提供了一种新的思维方式,让我们可以从不同的角度看待问题,有时能够简化复杂问题的求解过程.