Propositional equality for gradual dependently typed programming
Author
dc.contributor.author
Eremondi, Joseph
Author
dc.contributor.author
García, Ronald
Author
dc.contributor.author
Tanter, Eric Pierre
Admission date
dc.date.accessioned
2022-12-21T20:01:22Z
Available date
dc.date.available
2022-12-21T20:01:22Z
Publication date
dc.date.issued
2022
Cita de ítem
dc.identifier.citation
Proc. ACM Program. Lang., (2022) 6, No. ICFP, Article 96.
es_ES
Identifier
dc.identifier.other
10.1145/3547627
Identifier
dc.identifier.uri
https://repositorio.uchile.cl/handle/2250/189933
Abstract
dc.description.abstract
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for 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 refl is the only closed value of an equality type, a gradual extension of the Calculus of Inductive Constructions (CIC) with propositional equality violates static observational equivalences. Extensionally-equal functions should be indistinguishable at run time, but they can be distinguished using a combination of equality and type imprecision.
This work presents a gradual dependently typed language that supports propositional equality. We avoid the above issues by devising an equality type of which 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. We thus 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, weak canonicity, and the gradual guarantees of Siek et al., which ensure that reducing a program's precision introduces no new static or dynamic errors.
es_ES
Lenguage
dc.language.iso
en
es_ES
Publisher
dc.publisher
ACM
es_ES
Type of license
dc.rights
Attribution-NonCommercial-NoDerivs 3.0 United States