A type system for run-time identity functions
Master Project of José Padilla Cancio

Project description

In quantitative type theory (QTT), the 0 quantity can be used to annotate parts of a program that are only relevant at compile-time and thus should not appear in the compiled code. This has been used to considerable effect in the Idris 2 and Agda languages. However, while it allows for the erasure of the argument to a function call, it is not possible to indicate that the function being called itself should be erased during compilation.

The goal of this project is to extend QTT with a notion of run-time identity functions that return their argument unchanged (except for possibly some parts that are erased during compilation). Concretely, you will (1) develop the theoretical framework for a type theory with such functions, (2) implement it as an extension to the implementation of Agda or Idris 2, and (3) work out examples and case studies to investigate the practical usefulness of this feature.

Further reading

• Edwin Brady, Idris 2: Quantitative Type Theory in Practice (2021)