Deriving Dependently-Typed OOP from First Principles

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.

To top