Deriving Dependently-Typed OOP from First Principles

This paper tackles the expression problem in the context of dependent types by showing that functional and object-oriented programming are dual paradigms rooted in data and codata. Rather than extending OOP with dependent types in an ad-hoc way, the authors derive a dual, dependently typed object-oriented calculus using defunctionalization and refunctionalization. The result is a language with two semantically equivalent fragments—functional and object-oriented—connected by type- and semantics-preserving transformations, expanding the theoretical foundations and extensibility of typed programming languages.