Dependent Data and Codata Types
Assigned to Florian Engel.
User-defined data and codata types are two dual and complementary ways to specify types and their inhabitants. Data types specify canonical producers which are built up by constructors, and non-canonical consumers which are formed by pattern matching on constructors. Codata types specify canonical consumers which are built up by destructors, and non-canonical producers which are built up by copattern matching on destructors. For example, using (indexed) codata types it is possible to replace a builtin (dependent) function type by a user defined type.
The thesis consists in (1) a survey of existing work in extending dependent type theories by coinductive types, and (2) adapting existing dependent inductive/coinductive type theories to the Ouroboro framework. The ultimate goal of the project is to pave the way to a definition of typed, dependent de- and refunctionalization.