The expression problem highlights the challenge of extending types with new producers or consumers but not both simultaneously. This is evident in the difference between functional and object-oriented programming paradigms. Dependently typed programming follows the functional model and introduces an unexplored space in the programming language landscape. This paper explores dependently-typed object-oriented programming through duality, deriving a calculus with dual language fragments. The key contribution lies in the type- and semantics-preserving transformations between these fragments, achieved through defunctionalization and refunctionalization. The implementation of this language illuminates the concept of duality in explain various aspects of dependently typed programming.
https://arxiv.org/abs/2403.06707