从基本原理推导依赖类型的面向对象编程——扩展版本及附录 (arxiv.org)

本文探讨了依赖类型的面向对象编程领域，从熟悉的基于数据语言开始，通过系统的反函数化和再函数化，推导出其对偶片段。论文的核心贡献是一个包含两种对偶语言片段的依赖类型演算，并提供这两种语言片段之间的类型和语义保留转换：反函数化和再函数化。