Symmetric Dependent Data and Codata Types

David Binder


Date: Wed, March 13, 2024
Time: 12:00
Room: Turing


In the first part I am going to present the wider context of my research: designing programming languages with equal support for data and codata types. Codata types are known in the proof assistant community because they are a natural choice for modelling coinductive types such as streams. There are other reasons, however, why one might want to have codata types in a programming language: 1) Codata types are important for modelling non-strict data types such as lazy pairs, since codata types naturally model demand-driven computation. 2) Codata types are essential if the language contains linear types or other modalities. The pair type, for example, splits into two different pair types in linear logic, with one of them corresponding to a data type and the other to a codata type. 3) Data and codata types have different extensibility properties which correspond exactly to the expression problem: Data types can easily be extended with new consumers and codata types with new producers, but not vice versa.

In the second part I am going to present the content of our recent article “Deriving Dependently-Typed OOP from First Principles”, which is going to be published at OOPSLA 2024. We designed and implemented a dependently-typed programming language with the following properties: 1) The language only contains user-defined data and codata types. In particular, the function type and the Pi-type are not built into the language but defined by the programmer. 2) We implemented defunctionalization and refunctionalization which allow to transform any data type into a codata type, and vice versa. We proved soundness for the language and these transformations, and used it to develop various examples and case studies. Defunctionalization and refunctionalization also impose certain constraints on the design of the language, which I will describe.

Lastly, I am going to discuss some directions of research which we left open and plan to pursue in the future.

Previous: |
Next: |