Type preserving closure conversion of languages with dependent types hasproved difficult. It took until 2018 to get the first solution to theproblem, and that solution relies on language constructs custom-made for thepurpose and does not support the customary tower of universes. There arebasically three sources of difficulty. The first of them occurs when weneed to close over variables which appear also in the type of the function, and can be solved with singleton types or translucent types. The seconddifficulty is the fact that closure conversion inevitably requires some formof impredicativity since a function can close over free variables thatbelong to a higher universe than itself. None of the existing forms ofimpredicativity (other than those known to be inconsistent) satisfy theneeds of closure conversion with a tower of universes. And the lastdifficulty is that closure conversion exposes internal details of functions, and those details affect the definitional equality of (converted) functions, thereby breaking type preservation. In this paper we investigate what is necessary to solve those three problemswhen implementing a type preserving closure conversion for a dependently typed-calculus with a tower of universes without relying on custom-madeconstructs in the target language, or more precisely while relying onconstructs that are as generic as possible. Concretely, we use equalityproofs to solve the first problem, a new form of impredicativity for thesecond, and quotient types for the third. While these functionalities werenot custom-made for the purpose of closure conversion, we show how thosehigh-level features need to be adjusted to accommodate a lower-levellanguage where functions need to be closed.
Monnier et al. (Wed,) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: