View publication

Title A Reasonably Gradual Type Theory
Authors Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
Publication date August 2022
Abstract Gradualizing the Calculus of Inductive Constructions (CIC)
involves dealing with subtle tensions between normalization, graduality, and
conservativity with respect to CIC. Recently, GCIC has been proposed as a
parametrized gradual type theory that admits three variants, each
sacrificing one of these properties. For devising a gradual proof assistant
based on CIC, normalization and conservativity with respect to CIC are key,
but the tension with graduality needs to be addressed. Additionally, several
challenges remain: (1) The presence of two wildcard terms at any type---the
error and unknown terms---enables trivial proofs of any theorem,
jeopardizing the use of a gradual type theory in a proof assistant; (2)
Supporting general indexed inductive families, most prominently equality, is
an open problem; (3) Theoretical accounts of gradual typing and graduality
so far do not support handling type mismatches detected during reduction;
(4) Precision and graduality are external notions not amenable to reasoning
within a gradual type theory. All these issues manifest primally in CastCIC,
the cast calculus used to define GCIC. In this work, we present an extension
of CastCIC called GRIP. GRIP is a reasonably gradual type theory that
addresses the issues above, featuring internal precision and general
exception handling. By adopting a novel interpretation of the unknown term
that carefully accounts for universe levels, GRIP satisfies graduality for a
large and well-defined class of terms, in addition to being normalizing and
a conservative extension of CIC. Internal precision supports reasoning about
graduality within GRIP itself, for instance to characterize gradual
exception-handling terms, and supports gradual subset types. We develop the
metatheory of GRIP using a model formalized in Coq, and provide a prototype
implementation of GRIP in Agda.
Pages 931-959
Volume 6
Journal name Proceedings of the ACM Programming Languages
Publisher ACM Press (New York, NY, USA)
Reference URL View reference page