ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Mon 12 Sep 2022 15:50 - 16:10 at Linhart - (Gradual) Type Theory Chair(s): Jesper Cockx

Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for \textit{imprecise} types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a central feature of type theory: propositional equality. Lennon-Bertrand et al. show that, when the reflexive proof $\mathit{refl}$ is the only closed value of an equality type, a gradual extension of CIC with propositional equality violates static observational equivalences. Extensionally-equal functions should be indistinguishable at run time, but the combination of equality and type imprecision allows for contexts that distinguish extensionally-equal but syntactically-different functions.

This work presents a gradually typed language that supports propositional equality. We avoid the above issues by devising an equality type where $\mathit{refl}$ is not the only closed inhabitant. Instead, each equality proof is accompanied by a term that is at least as precise as the equated terms, acting as a witness of their plausible equality. These witnesses track partial type information as a program runs, raising errors when that information shows that two equated terms are undeniably inconsistent. Composition of type information is internalized as a construct of the language, and is deferred for function bodies whose evaluation is blocked by variables. By deferring, we ensure that extensionally equal functions compose without error, thereby preventing contexts from distinguishing them. We describe the challenges of designing consistency and precision relations for this system, along with solutions to these challenges. Finally, we prove important metatheory: type-safety, conservative embedding of CIC, canonicity up to termination, and the gradual guarantees of Siek et al., which ensure that reducing a program’s precision introduces no new static or dynamic errors.

#### Mon 12 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

 15:50 - 16:50 (Gradual) Type TheoryICFP Papers and Events at Linhart Chair(s): Jesper Cockx TU Delft 15:5020mTalk Propositional Equality for Gradual Dependently Typed ProgrammingICFP Papers and EventsJoseph Eremondi University of British Columbia, Ronald Garcia University of British Columbia, Éric Tanter University of Chile DOI 16:1020mTalk A Reasonably Gradual Type TheoryICFP Papers and EventsKenji Maillard Inria Nantes & University of Chile, Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile DOI 16:3020mTalk A completely unique account of enumerationICFP Papers and EventsCas van der Rest Delft University of Technology, Wouter Swierstra Utrecht University, Netherlands DOI