View publication

Title Propositional Equality for Gradual Dependently-Typed Programming
Authors Joseph Eremondi, Ronald Garcia, Éric Tanter
Publication date August 2022
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.
Pages 165-193
Volume 6
Journal name Proceedings of the ACM Programming Languages
Publisher ACM Press (New York, NY, USA)
Reference URL View reference page