Gradualizing the Calculus of Inductive Constructions

As a well-behaved typed programming language, \(\mathsf {CIC}\) enjoys (type) Safety ( \(\mathcal {S}\) ), meaning that well-typed closed terms cannot get stuck, i.e., the normal forms of closed terms of a given type are exactly the canonical forms of that type. In \(\mathsf {CIC}\) , a closed canonical form is a term whose typing derivation ends with an introduction rule, i.e., an \(\lambda\) -abstraction for a function type, and a constructor for an inductive type. For instance, any closed term of type \(\mathsf{bool}\) is convertible (and reduces) to either \(\mathsf{true}\) or \(\mathsf{false}\) . Note that an open term can reduce to an open canonical form called a neutral term, such as \(\mathsf{not x}\) .

As a logically consistent type theory, \(\mathsf {CIC}\) enjoys (strong) Normalization ( \(\mathcal {N}\) ), meaning that any term is convertible to its (unique) normal form. \(\mathcal {N}\) together with \(\mathcal {S}\) imply canonicity: any closed term of a given type must reduce to a canonical form of that type. When applied to the empty type \(\mathsf{False}\) , canonicity ensures logical consistency: Because there is no canonical form for \(\mathsf{False}\) , there is no closed proof of \(\mathsf{False}\) . Note that \(\mathcal {N}\) also has an important consequence in \(\mathsf {CIC}\) . Indeed, in this system, conversion—which coarsely means syntactic equality up-to reduction—is used in the type-checking algorithm. \(\mathcal {N}\) ensures that one can devise a sound and complete decision procedure (a.k.a. a reduction strategy) in order to decide conversion, and hence, typing.

In the gradual setting, the two cornerstones \(\mathcal {S}\) and \(\mathcal {N}\) must be considered with care. First, any closed term can be ascribed the unknown type \(\mathsf{?}\) first and then any other type: For instance, \(\mathsf{0::?::bool}\) is a well-typed closed term of type \(\mathsf{bool}\) . ⁴ However, such a term cannot possibly reduce to either \(\mathsf{true}\) or \(\mathsf{false}\) , so some concessions must be made with respect to safety—at least, the notion of canonical forms must be extended.

Second, \(\mathcal {N}\) is endangered. The quintessential example of non-termination in the untyped lambda calculus is the term \(\Omega := \delta ~\delta\) where \(\delta := (\lambda ~ x.~x~x)\) . In the simply-typed lambda calculus (hereafter \(\mathsf {STLC}\) ), as in \(\mathsf {CIC}\) , self-applications like \(\delta ~\delta\) and \(x~x\) are ill-typed. However, when introducing gradual types, one usually expects to accommodate such idioms, and therefore in a standard gradually-typed calculus such as \(\mathsf {GTLC}\) Siek and Taha 2006, a variant of \(\Omega\) that uses \((\lambda ~ x : ?.~x~x)\) for \(\delta\) is well-typed and diverges, that is, admits no normal form. The reason is that the argument type of \(\delta\) , the unknown type \(?\) , is consistent with the type of \(\delta\) itself, \(? \rightarrow ?\) , and at runtime, nothing prevents reduction from going on forever. Therefore, if one aims at ensuring \(\mathcal {N}\) in a gradual setting, some care must be taken to restrict expressiveness.

Let us first address the elephant in the room: Why would one want to gradualize \(\mathsf {CIC}\) instead of simply postulating an axiom for any term (be it a program or a proof) that one does not feel like providing (yet)?

Indeed, we can augment \(\mathsf {CIC}\) with a general-purpose wildcard axiom \(\texttt {ax}\) :

The resulting theory, called \(\mathsf {CIC}\!+\!{ \texttt {ax}}\) , has an obvious practical benefit: we can use \(\mathsf{(_st A)}\) , hereafter noted \(\mathsf{_st_A}\) , as a wildcard whenever we are asked to exhibit an inhabitant of some type \(\mathsf{A}\) and we do not (yet) want to. This is exactly what admitted definitions are in \(\mathrm{Coq}\) , for instance, and they do play an important practical role at some stages of any \(\mathrm{Coq}\) development.

However, we cannot use the axiom \(\mathsf{_st_A}\) in any meaningful way as a value at the type level. For instance, going back to Example 1, one might be tempted to give to the \(\mathsf{filter}\) function on vectors the type \(\mathsf{forall A n (f : A -\gt bool), vec A n -\gt vec A _st_nat}\) , in order to avoid the complications related to specifying the size of the vector produced by \(\mathsf{filter}\) . The problem is that the term:

\(\mathsf{head nat _st_nat (filter nat 4 even [0; 1; 2; 3])}\) ,

does not typecheck because the type of the filtering expression, \(\mathsf{vec A _st_nat}\) , is not convertible to \(\mathsf{vec A (S _st_nat)}\) , as required by the domain type of \(\mathsf{head nat _st_nat}\) .

So the axiomatic approach is not useful for making dependently-typed programming any more pleasing. That is, using axioms goes in total opposition to the gradual typing criteria Siek et al. 2015 when it comes to the smoothness of the static-to-dynamic checking spectrum: given a well-typed term, making it “less precise” by using axioms for some subterms actually results in programs that do not typecheck or reduce anymore.

Because \(\mathsf {CIC}\!+\!{\texttt {ax}}\) amounts to working in \(\mathsf {CIC}\) with an initial context extended with \(\texttt {ax}\) , this theory satisfies normalization ( \(\mathcal {N}\) ) as much as \(\mathsf {CIC}\) , so conversion remains decidable. However, \(\mathsf {CIC}\!+\!{\texttt {ax}}\) lacks a satisfying notion of safety because there is an infinite number of open canonical normal forms (more adequately called stuck terms) that inhabit any type \(\mathsf{A}\) . For instance, in \(\mathsf{bool}\) , we not only have the normal forms \(\mathsf{true}\) , \(\mathsf{false}\) , and \(\mathsf{_st_bool}\) , but an infinite number of terms stuck on eliminations of \(\texttt {ax}\) , such as \(\mathsf{match _st_A with ...}\) or \(\texttt {ax}_{\mathbb {N}\rightarrow \mathbb {B}}\;1\) .

Pédrot and Tabareau 2018 present the exceptional type theory \(\mathsf {ExTT}\) , demonstrating that it is possible to extend a type theory with a wildcard term while enjoying a satisfying notion of safety, which coincides with that of programming languages with exceptions.

\(\mathsf {ExTT}\) is essentially \(\mathsf {CIC}\!+\!{{\rm \mathtt {err}}}\) , that is, it extends \(\mathsf {CIC}\) with an indexed error term \(\mathsf{raise_A}\) that can inhabit any type \(\mathsf{A}\) . But instead of being treated as a computational black box like \(\mathsf{_st_A}\) , \(\mathsf{raise_A}\) is endowed with computational content emulating exceptions in programming languages, which propagate instead of being stuck. For instance, in \(\mathsf {ExTT}\) we have the following conversion:

\(\mathsf{match raise_bool return nat with | true -\gt O | false -\gt 1 end}\) \(\equiv\) \(\mathsf{raise_nat}\) .

Notably, such exceptions are call-by-name exceptions, so one can only discriminate exceptions on positive types (i.e., inductive types), not on negative types (i.e., function types). In particular, in \(\mathsf {ExTT}\) , \(\mathsf{raise_A{}_-\gt {}_B }\) and \(\mathsf{fun _ : A =\gt raise_B}\) are convertible, and the latter is considered to be in normal form. So \(\mathsf{raise_A}\) is a normal form of \(\mathsf{A}\) only if \(\mathsf{A}\) is a positive type.

\(\mathsf {ExTT}\) has a number of interesting properties: It is normalizing ( \(\mathcal {N}\) ) and safe ( \(\mathcal {S}\) ), taking \(\mathsf{raise_A}\) into account as usual in programming languages where exceptions are possible outcomes of computation: The normal forms of closed terms of a positive type (e.g., \(\mathsf{bool}\) ) are either the constructors of that type (e.g., \(\mathsf{true}\) and \(\mathsf{false}\) ) or \(\mathsf{raise}\) at that type (e.g., \(\mathsf{err_bool}\) ). As a consequence, \(\mathsf {ExTT}\) does not satisfy full canonicity, but it does satisfy a weaker form of it. In particular, \(\mathsf {ExTT}\) enjoys (weak) logical consistency: Any closed proof of \(\mathsf{False}\) is convertible to \(\mathsf{raise_False}\) , which is discriminable at \(\mathsf{False}\) . It has been shown that we can still reason soundly in an exceptional type theory, either using a parametricity requirement Pédrot and Tabareau 2018, or more flexibly, using different universe hierarchies Pédrot et al. 2019.

It is also important to highlight that this weak form of logical consistency is the most one can expect in a theory with effects. Indeed, Pédrot and Tabareau 2020 have shown that it is not possible to define a type theory with full dependent elimination that has observable effects (from which exceptions are a particular case) and at the same time validates traditional canonicity. Settling for less, as explained in Section 2.2 for the axiomatic approach, leads to an infinite number of stuck terms, even in the case of booleans, which is in opposition to the type safety criterion of gradual languages, which only accounts for runtime type errors.

Unfortunately, while \(\mathsf {ExTT}\) solves the safety issue of the axiomatic approach, it still suffers from the same limitation as the axiomatic approach regarding type-level computation. Indeed, even though we can use \(\mathsf{raise_A}\) to inhabit any type, we cannot use it in any meaningful way as a value at the type level. The term:

\(\mathsf{head nat err_nat (filter nat 4 even [ 0 ; 1 ; 2 ; 3 ])}\) ,

does not typecheck, because \(\mathsf{vec A raise_nat}\) is still not convertible to \(\mathsf{vec A (S raise_nat)}\) . The reason is that \(\mathsf{raise_nat}\) behaves like an extra constructor to \(\mathsf{nat}\) , so \(\mathsf{S raise_nat}\) is itself a normal form, and normal forms with different head constructors ( \(\mathsf{S}\) and \(\mathsf{raise_nat}\) ) are not convertible.

Before going on with our exploration of the fundamental challenges in gradual dependent type theory, we review some key concepts and expected properties in the context of simple types Siek et al. 2015 New and Ahmed 2018 Garcia et al. 2016.

Static semantics. Gradually-typed languages introduce the unknown type, written ?, which is used to indicate the lack of static typing information Siek and Taha 2006. One can understand such an unknown type in terms of an abstraction of the set of possible types that it stands for Garcia et al. 2016. This interpretation provides a naive but natural understanding of the meaning of partially-specified types, for instance, \(\mathbb {B}\rightarrow ?\) denotes the set of all function types with \(\mathbb {B}\) as domain. Given imprecise types, a gradual type system relaxes all type predicates and functions in order to optimistically account for occurrences of ?. In a simple type system, the predicate on types is equality, whose relaxed counterpart is called consistency.⁵ For instance, given a function \(\mathsf{f}\) of type \(\mathbb {B}\rightarrow ?\) , the expression \(\mathsf{(f true) + 1}\) is well-typed because \(\mathsf{f}\) could plausibly return a number, given that its codomain is ?, which is consistent with \(\mathsf{nat}\) .

Note that there are other ways to consider imprecise types, for instance by restricting the unknown type to denote base types (in which case \(?\) would not be consistent with any function type), or to only allow imprecision in certain parts of the syntax of types, such as effects Bañados Schwerter et al. 2016, security labels Fennell and Thiemann 2013 Toro et al. 2018, annotations Thiemann and Fennell 2014, or only at the top-level Bierman et al. 2010. Here, we do not consider these specialized approaches, which have benefits and challenges of their own, and stick to the mainstream setting of gradual typing in which the unknown type is consistent with any type and can occur anywhere in the syntax of types.

Dynamic semantics. Having optimistically relaxed typing based on consistency, a gradual language must detect inconsistencies at runtime if it is to satisfy safety ( \(\mathcal {S}\) ), which therefore has to be formulated in a way that encompasses runtime errors. For instance, if the function \(\mathsf{f}\) above returns \(\mathsf{false}\) , then an error must be raised to avoid reducing to \(\mathsf{false + 1}\) —a closed stuck term, denoting a violation of safety. The traditional approach to do so is to avoid giving a direct reduction semantics to gradual programs, and instead, to elaborate them to an intermediate language with runtime casts, in which casts between inconsistent types raise errors Siek and Taha 2006. Alternatively—and equivalently from a semantics point of view—one can define the reduction of gradual programs directly on gradual typing derivations augmented with evidence about consistency judgments, and report errors when transitivity of such judgments is unjustified Garcia et al. 2016. There are many ways to realize each of these approaches, which vary in terms of efficiency and eagerness of checking Herman et al. 2010 Tobin-Hochstadt and Felleisen 2008 Siek and Wadler 2010 Siek et al. 2009 Toro and Tanter 2020 Bañados Schwerter et al. 2021.

Conservativity. A first important property of a gradual language is that it is a conservative extension of a related static typing discipline: The gradual and static systems should coincide on static terms. This property is hereafter called Conservativity ( \(\mathcal {C}\) ), and parametrized with the considered static system. For instance, we write that \(\mathsf {GTLC}\) satisfies \(\mathcal {C}_{/{\mathsf {STLC}}}\) . Technically, Siek and Taha 2006 prove that typing and reduction of \(\mathsf {GTLC}\) and \(\mathsf {STLC}\) coincide on their common set of terms (i.e., terms that are fully precise). An important aspect of \(\mathcal {C}\) is that the type formation rules and typing rules themselves are also preserved, modulo the presence of ? as a new type and the adequate lifting of predicates and functions Garcia et al. 2016. While this aspect is often left implicit, it ensures that the gradual type system does not behave in ad hoc ways on imprecise terms.

Note that, despite its many issues, \(\mathsf {CIC}\!+\!{ \texttt {ax}}\) (Section 2.2) satisfies \(\mathcal {C}_{/{\mathsf {CIC}}}\) : All pure (i.e., axiom-free) \(\mathsf {CIC}\) terms behave as they would in \(\mathsf {CIC}\) . More precisely, two \(\mathsf {CIC}\) terms are convertible in \(\mathsf {CIC}\!+\!{\texttt {ax}}\) iff they are convertible in \(\mathsf {CIC}\) . Importantly, this does not mean that \(\mathsf {CIC}\!+\!{\texttt {ax}}\) is a conservative extension of \(\mathsf {CIC}\) as a logic—which it clearly is not!

Gradual guarantees. The early accounts of gradual typing emphasized consistency as the central idea. However, Siek et al. 2015 observed that this characterization left too many possibilities for the impact of type information on program behavior, compared to what was originally intended Siek and Taha 2006. Consequently, Siek et al. 2015 brought forth type precision (denoted \(\mathsf{precise}\) ) as the key notion, from which consistency can be derived: Two types \(\mathsf{A}\) and \(\mathsf{B}\) are consistent if and only if there exists \(\mathsf{T}\) such that \(\mathsf{T precise A}\) and \(\mathsf{T precise B}\) . The unknown type ? is the most imprecise type of all, i.e., \(\mathsf{T precise ?}\) for any \(\mathsf{T}\) . Precision is a preorder that can be used to capture the intended monotonicity of the static-to-dynamic spectrum afforded by gradual typing. The static and dynamic gradual guarantees specify that typing and reduction should be monotone with respect to precision: losing precision should not introduce new static or dynamic errors. These properties require precision to be extended from types to terms. Siek et al. 2015 present a natural extension that is purely syntactic: A term is more precise than another if they are syntactically equal except for their type annotations, which can be more precise in the former.

The static gradual guarantee (SGG) ensures that imprecision does not break typeability:

The SGG captures the intuition that “sprinkling ? over a term” maintains its typeability. As such, the notion of precision \(\mathsf{precise}\) used to formulate the SGG is inherently syntactic, over as-yet-untyped terms: typeability is the consequence of the SGG theorem.

The dynamic gradual guarantee (DGG) is the key result that bridges the syntactic notion of precision to reduction: If \(\mathsf{t precise u}\) and \(\mathsf{t}\) reduce to some value \(\mathsf{v}\) , then \(\mathsf{u}\) reduces to some value \(\mathsf{v^{\prime }}\) such that \(\mathsf{v precise v^{\prime }}\) ; and if \(\mathsf{t}\) diverges, then so does \(\mathsf{u}\) . This property entails that \(\mathsf{t precise u}\) means that \(\mathsf{t}\) may error more than \(\mathsf{u}\) , but otherwise they should behave the same. Instead of the original formulation of the DGG by Siek et al. 2015, New and Ahmed 2018 appeal to the semantic notion of observational error-approximation to capture the relation between two terms that are contextually equivalent except that the left-hand side term may fail more.⁶

Using this semantic notion, the DGG simply states that term precision implies observational error-approximation:

While often implicit, it is important to highlight that the DGG is relative to both the notion of precision \(\mathsf{precise}\) and the notion of observations \(\mathsf{obsApprox}\) . Indeed, it is possible to study alternative notions of precisions beyond the natural definition stated by Siek et al. 2015. For instance, following the Abstracting Gradual Typing methodology Garcia et al. 2016, precision follows from the definition of gradual types as a concretization to sets of static types. This opens the door to justifying alternative precisions, e.g., by considering that the unknown type only stands for specific static types, such as base types. Additionally, variants of precision have been studied in more challenging typing disciplines where the natural definition seems incompatible with the DGG, see e.g., Igarashi et al. 2017. As we will soon see below, it can also be necessary in certain situations to consider another notion of observations.

Graduality. As we have seen, the DGG is relative to a notion of precision, but what should this relation be? To go beyond a syntactic axiomatic definition of precision, New and Ahmed 2018 characterize the good dynamic behavior of precision: The runtime checking mechanism used to define a gradual language, such as casting, should only perform type checking, and not otherwise affect behavior. Specifically, they mandate that precision gives rise to embedding-projection pairs (ep-pairs): The cast induced by two types related by precision forms an adjunction, which induces a retraction. In particular, going to a less precise type and back is the identity: For any term \(\mathsf{a}\) of type \(\mathsf{A}\) , and given \(\mathsf{A precise B}\) , then \(\mathsf{a::B::A}\) should be observationally equivalent to \(\mathsf{a}\) (recall from Footnote 4 that \(\mathsf{::}\) is a type ascription). For instance, \(\mathsf{1::?::nat}\) should be equivalent to \(\mathsf{1}\) . Dually, when gaining precision, there is the potential for errors: given a term \(\mathsf{b}\) of type \(\mathsf{B}\) , \(\mathsf{b::A::B}\) may fail. By considering error as the least precise term, this can be stated as \(\mathsf{b::A::B precise b}\) . For instance, with the imprecise successor function \(\mathsf{f := fun n:? =\gt (S n)::?}\) of type \(\mathsf{?-\gt ?}\) , we have \(\mathsf{f::nat-\gt bool::?-\gt ? precise f}\) , because the ascribed function will fail when applied.

Technically, the adjunction part states that if we have \(\mathsf{A precise B}\) , a term \(\mathsf{a}\) of type \(\mathsf{A}\) , and a term \(\mathsf{b}\) of type \(\mathsf{B}\) , then \(\mathsf{a precise b::A \lt =\gt a::B precise b}\) . The retraction part further states that \(\mathsf{t}\) is not only more precise than \(\mathsf{t::B::A}\) (which is given by the unit of the adjunction) but is equi-precise to it, noted \(\mathsf{t equiprecise t::B::A}\) . Because the DGG dictates that precision implies observational error-approximation, equi-precision implies observational equivalence, and so losing and recovering precision must produce a term that is observationally equivalent to the original one.

A couple of additional observations need to be made here, as they will play a major role in the development of this article:

In this article, we use the term Graduality ( \(\mathcal {G}\) ) for the DGG established with respect to a notion of precision that also induces embedding-projection pairs.

Extending the gradual approach to a setting with full dependent types requires reconsidering several aspects.

Newcomers: the unknown term and the error type. In the simply-typed setting, there is a clear stratification: \(?\) is at the type level, \(\mathsf{raise}\) is at the term level. Likewise, type precision, with ? as greatest element, is separate from term precision, with \(\mathsf{raise}\) as least element. In the absence of a type/term syntactic distinction as in \(\mathsf {CIC}\) , this stratification is untenable:

Revisiting safety. The notion of closed canonical forms used to characterize legitimate normal forms via safety ( \(\mathcal {S}\) ) needs to be extended not only with errors as in the simply-typed setting, but also with unknown terms. Indeed, as there is an unknown term \(\mathsf{?_A}\) inhabiting any type \(\mathsf{A}\) , we have one new canonical form for each type \(\mathsf{A}\) . In particular, \(\mathsf{?_bool}\) cannot possibly reduce to either \(\mathsf{true}\) or \(\mathsf{false}\) or \(\mathsf{raise_bool}\) , because doing so would collapse the precision order. Therefore, \(\mathsf{?_A}\) should propagate computationally, like \(\mathsf{raise_A}\) (Section 2.3).

The difference between errors and unknown terms is rather on their static interpretation. In essence, the unknown term \(\mathsf{?_A}\) is a dual form of exceptions: It propagates, but is optimistically comparable, i.e., consistent with, any other term of type \(\mathsf{A}\) . Conversely, \(\mathsf{raise_A}\) should not be consistent with any term of type \(\mathsf{A}\) . Going back to the issues we identified with the axiomatic (Section 2.2) and exceptional (Section 2.3) approaches when dealing with type-level computation, the term:

\(\mathsf{head nat ?_nat (filter nat 4 even [ 0 ; 1 ; 2 ; 3 ])}\) ,

now typechecks: \(\mathsf{vec A ?_nat}\) can be deemed consistent with \(\mathsf{vec A (S ?_nat)}\) , because \(\mathsf{S ?_nat}\) is consistent with \(\mathsf{?_nat}\) . This newly-brought flexibility is the key to support the different scenarios from the introduction. So let us now turn to the question of how to integrate consistency in a dependently-typed setting.

Relaxing conversion. In the simply-typed setting, consistency is a relaxing of syntactic type equality to account for imprecision. In a dependent type theory, there is a more powerful notion than syntactic equality to compare types, namely, conversion (Section 2.1): if \(\mathsf{t:T}\) and \(\mathsf{T == U}\) , then \(\mathsf{t:U}\) . For instance, a term of type \(\mathsf{T}\) can be used as a function as soon as \(\mathsf{T}\) is convertible to the type \(\mathsf{forall (a:A),B}\) for some types \(\mathsf{A}\) and \(\mathsf{B}\) . The proper notion to relax in the gradual dependently-typed setting is therefore conversion, not syntactic equality.

Garcia et al. 2016 give a general framework for gradual typing that explains how to relax any static type predicate to account for imprecision: for a binary type predicate \(\mathsf{P}\) , its consistent lifting \(\mathsf{Q(A,B)}\) holds iff there exist static types \(\mathsf{A^{\prime }}\) and \(\mathsf{B^{\prime }}\) in the denotation (concretization in abstract interpretation parlance) of \(\mathsf{A}\) and \(\mathsf{B}\) , respectively, such that \(\mathsf{P(A^{\prime },B^{\prime })}\) . As observed by Castagna et al. 2019, when applied to equality, this defines consistency as a unification problem. Therefore, the consistent lifting of conversion ought to be that two terms \(\mathsf{t}\) and \(\mathsf{u}\) are consistently convertible iff they denote some static terms \(\mathsf{t^{\prime }}\) and \(\mathsf{u^{\prime }}\) such that \(\mathsf{t^{\prime } == u^{\prime }}\) . This property is essentially higher-order unification, which is undecidable.

It is therefore necessary to adopt some approximation of consistent conversion (hereafter called consistency for short) in order to be able to implement a gradual dependent type theory. And there lies a great challenge: because of the absence of stratification between typing and reduction, the SGG already demands monotonicity for conversion, a demand very close to that of the DGG.⁷

Dealing with neutrals. Prior work on gradual typing usually only considers reduction on closed terms in order to establish results about the dynamics, such as the DGG. But in dependent type theory, conversion must operate on open terms, yielding neutral terms such as \(\mathsf{1::X::nat}\) where \(\mathsf{X}\) is a type variable, or \(\mathsf{x+1}\) where \(\mathsf{x}\) is of type \(\mathsf{nat}\) or \(\mathsf{?_Type}\) . Such neutral terms cannot reduce further, and can occur in both terms and types. Depending on the upcoming substitutions, neutrals can fail or not. For instance, in \(\mathsf{1::X::nat}\) , if \(\mathsf{?_Type}\) is substituted for \(\mathsf{X}\) , the term reduces to \(\mathsf{1}\) , but fails if \(\mathsf{bool}\) is substituted instead.

Importantly, less precise variants of neutrals can reduce more. For instance, both \(\mathsf{1::?_Type::nat}\) and \(\mathsf{?_nat+1}\) are less precise than the neutrals above, but do evaluate further (typically, to \(\mathsf{1}\) and to \(\mathsf{?_nat}\) , respectively). This interaction between neutrals, reduction, and precision spices up the goal of establishing DGG and \(\mathcal {G}\) . In particular, this re-enforces the need to consider semantic precision, because a syntactic precision is likely not to be stable by reduction: \(\mathsf{1::X::nat precise 1::?::nat}\) is obvious syntactically, but \(\mathsf{1::X::nat precise 1}\) is not.

DGG vs Graduality. In a dependently-typed setting, it is possible to satisfy the DGG while not satisfying the embedding-projection pairs requirement of \(\mathcal {G}\) . To see why, consider a system in which any term of type \(\mathsf{A}\) that is not fully-precise immediately reduces to \(\mathsf{?_A}\) . This system would satisfy \(\mathcal {C}\) , \(\mathcal {S}\) , \(\mathcal {N}\) , and ...the DGG. Recall that the DGG only requires reduction to be monotone with respect to precision, so using the most imprecise term \(\mathsf{?_A}\) as a universal redux is surely valid. This collapse of the DGG is impossible in the simply-typed setting because there is no unknown term: it is only possible when \(\mathsf{?_A}\) exists as a term. It is therefore possible to satisfy the DGG while being useless when computing with imprecise terms. Conversely, the degenerate system breaks the embedding-projection requirement of graduality stated by New and Ahmed 2018. For instance, \(\mathsf{1::?_Type::nat}\) would be convertible to \(\mathsf{?_nat}\) , which is not observationally equivalent to \(\mathsf{1}\) . Therefore, the embedding-projection requirement of graduality goes beyond the DGG in a way that is critical in a dependent type theory, where it captures both the smoothness of the static-to-dynamic checking spectrum, and the proper computational content of valid uses of imprecision.

Observational refinement. Let us come back to the notion of observational error-approximation used in the simply-typed setting to state the DGG. New and Ahmed 2018 justify this notion because in “gradual typing we are not particularly interested in when one program diverges more than another, but rather when it produces more type errors.” This point of view is adequate in the simply-typed setting because the addition of casts may only produce more type errors; in particular, adding casts can never lead to divergence when the original term does not diverge itself. Therefore, in that setting, the definition of error-approximation includes equi-divergence. The situation in the dependent setting is however more complicated, if the theory admits divergence. There exist non-gradual dependently-typed programming languages that admit divergence (e.g., Dependent Haskell Eisenberg 2016, Idris Brady 2013); we will also present one such theory in this article.

In a gradual dependent type theory that admits divergence, a diverging term is more precise than the unknown term \(?\) . Because the unknown term in itself does not diverge, this breaks the left-to-right implication of equi-divergence. Note that this argument does not rely on any specific definition of precision, just on the fact that the unknown term is the most imprecise term (at its type). Additionally, an error at a diverging type \(X\) may be ascribed to \(?_{[]}\) then back to \(X\) . Evaluating this roundtrip requires evaluating \(X\) itself, which makes the less precise term diverge. This breaks the right-to-left implication of equi-divergence.

To summarize, the way to understand these counterexamples is that in a dependent and non-terminating setting, the motto of graduality ought to be adjusted: More precise programs produce more type errors or diverge more. This leads to the following definition of observational refinement.

In this definition, errors and divergence are collapsed. Thus, in a gradual dependent theory that admits divergence, equi-refinement does not imply observational equivalence, because one term might diverge, while the other reduces to an error. Of course, if the gradual dependent theory is strongly normalizing, then both notions \(\preccurlyeq ^{obs}\) (Definition 2) and \(\sqsubseteq ^{obs}\) (Definition 4) coincide.

To sum up, we have seen four important properties that can be expected from a gradual type theory: safety ( \(\mathcal {S}\) ), conservativity with respect to a theory \(X\) ( \(\mathcal {C}_{/{X}}\) ), graduality ( \(\mathcal {G}\) ), and normalization ( \(\mathcal {N}\) ). Any type theory ought to satisfy at least \(\mathcal {S}\) . Unfortunately, we now show that mixing the three other properties \(\mathcal {C}\) , \(\mathcal {G}\) , and \(\mathcal {N}\) is impossible for \(\mathsf {STLC}\) , as well as for \(\mathsf {CIC}\) .

Preliminary: regular reduction. To derive this general impossibility result, by relying only on the properties and without committing to a specific language or theory, we need to assume that the reduction system used to decide conversion is regular, in that it only looks at the weak head normal form of subterms for reduction rules, and does not magically shortcut reduction, for instance based on the specific syntax of inner terms. As an example, \(\beta\) -reduction is not allowed to look into the body of the lambda term to decide how to proceed.

This property is satisfied in all actual systems we know of, but formally stating it in full generality, in particular without devoting to a particular syntax, is beyond the scope of this article. Fortunately, in the following, we need only rely on a much weaker hypothesis, which is a slight strengthening of the retraction hypothesis of \(\mathcal {G}\) . Recall that retraction says that when \(\mathsf{A precise B}\) , any term \(\mathsf{t}\) of type \(\mathsf{A}\) is equi-precise to \(\mathsf{t::B::A}\) . We additionally require that for any context \(\mathsf{C}\) , if \(\mathsf{C[t]}\) reduces at least \(k\) steps, then \(\mathsf{C[t::B::A]}\) also reduces at least \(k\) steps. Intuitively, this means that the reduction of \(\mathsf{C[t::B::A]}\) , while free to decide when to get rid of the embedding-to- \(\mathsf{B}\) -projection-to- \(\mathsf{A}\) , cannot use it to avoid reducing \(\mathsf{t}\) . This property is true in all gradual languages, where type information at runtime is used only as a monitor.

Gradualizing \(\mathsf {STLC}\) . Let us first consider the case of \(\mathsf {STLC}\) . We show that \(\Omega\) is necessarily a well-typed diverging term in any gradualization of \(\mathsf {STLC}\) that satisfies the other properties.

This result could be extended to all terms of the untyped lambda calculus, not only \(\Omega\) , in order to obtain the embedding theorem of \(\mathsf {GTLC}\) Siek et al. 2015. Therefore, the embedding theorem is not an independent property, but rather a consequence of \(\mathcal {C}\) and \(\mathcal {G}\) —that is why we have not included it as such in our overview of the gradual approach (Section 2.4).

Gradualizing \(\mathsf {CIC}\) . We can now prove the same impossibility theorem for \(\mathsf {CIC}\) , by reducing it to the case of \(\mathsf {STLC}\) . Therefore, this theorem can be proven for type theories others than \(\mathsf {CIC}\) , as soon as they faithfully embed \(\mathsf {STLC}\) .

The Fire Triangle in practice. In non-dependent settings, all gradual languages where ? is universal admit non-termination and therefore compromise \(\mathcal {N}\) . Garcia and Tanter 2020 discuss the possibility to gradualize \(\mathsf {STLC}\) without admitting non-termination, for instance, by considering that ? is not universal and denotes only base types (in such a system, \(\mathsf{? -\gt ? nprecise ?}\) , so the argument with \(\Omega\) is invalid). Without sacrificing the universal unknown type, one could design a variant of \(\mathsf {GTLC}\) that uses some mechanism to detect divergence, such as termination contracts Nguyen et al. 2019. This would yield a language that certainly satisfies \(\mathcal {N}\) , but it would break \(\mathcal {G}\) . Indeed, because the contract system is necessarily over-approximating in order to be sound (and actually imply \(\mathcal {N}\) ), there are effectively-terminating programs with imprecise variants that yield termination contract errors.

To date, the only related work that considers the gradualization of full dependent types with ? as both a term and a type, is the work on GDTL Eremondi et al. 2019. GDTL is a programming language with a clear separation between the typing and execution phases, like Idris Brady 2013. GDTL adopts a different strategy in each phase: for typing, it uses Approximate Normalization (AN), which always produces \(\mathsf{?_A}\) as a result of going through imprecision and back. This means that conversion is both total and decidable (satisfies \(\mathcal {N}\) ), but it breaks \(\mathcal {G}\) for the same reason as the degenerate system we discussed in Section 2.5 (notice that the example uses a gain of precision from the unknown type to \(\mathsf{nat}\) , so the example behaves just the same with AN). In such a phased setting, the lack of computational content of AN is not critical, because it only means that typing becomes overly optimistic. To execute programs, GDTL relies on standard \(\mathsf {GTLC}\) -like reduction semantics, which is computationally precise, but does not satisfy \(\mathcal {N}\) .

To explore the spectrum of possibilities enabled by the Fire Triangle of Graduality, we develop a general approach to gradualizing \(\mathsf {CIC}\) , and use it to define three theories, corresponding to different resolutions of the triangular tension between normalization ( \(\mathcal {N}\) ), graduality ( \(\mathcal {G}\) ), and conservativity with respect to \(\mathsf {CIC}\) ( \(\mathcal {C}_{/{\mathsf {CIC}}}\) ).

The crux of our approach is to recognize that, while there is not much to vary within \(\mathsf {STLC}\) itself to address the tension of the Fire Triangle of Graduality, there are several variants of \(\mathsf {CIC}\) that can be considered by changing the hierarchy of universes and its impact on typing—after all, \(\mathsf {CIC}\) is but a particular Pure Type System (PTS) Barendregt 1991.

In particular, we consider a parametrized version of a gradual \(\mathsf {CIC}\) , called \(\mathsf {GCIC}\) , with two parameters (Figure 3):

Based on these parameters, this work develops the following three variants of \(\mathsf {GCIC}\) , whose properties are summarized in Table 1 with pointers to the respective theorems—because \(\mathsf {GCIC}\) is one common parametrized framework, we are able to establish most properties for all variants at once:

Practical implications of \(\mathsf {GCIC}\) variants. Regarding the examples from Section 1, all three variants of \(\mathsf {GCIC}\) support the exploration of the type-level precision spectrum for the functions described in Examples 1, 3, and 4. In particular, we can define \(\mathsf{filter}\) by giving it the imprecise type \(\mathsf{forall A n (f : A -\gt bool), vec A n -\gt vec A ?_nat}\) in order to bypass the difficulty of precisely characterizing the size of the output vector. Any invalid optimistic assumption is detected during reduction and reported as an error.

Unsurprisingly, the semantic differences between the three \(\mathsf {GCIC}\) variants crisply manifest in the treatment of potential non-termination (Example 2), more specifically, self application. Let us come back to the term \(\Omega\) used in the proof of Theorem 6. In all three variants, this term is well-typed. In \(\mathsf {GCIC} ^{\mathcal {G}}\) , it reduces forever, as it would in the untyped lambda calculus. In that sense, \(\mathsf {GCIC} ^{\mathcal {G}}\) can embed the untyped lambda calculus just as GTLC Siek et al. 2015. In \(\mathsf {GCIC} ^{\mathcal {N}}\) , this term fails at runtime because of the strict universe check in the reduction of casts, which breaks graduality because \(\mathsf{?_Typei -\gt ? _Typei precise ?_Typei}\) tells us that the upcast-downcast coming from an ep-pair should not fail. A description of the reductions in \(\mathsf {GCIC} ^{\mathcal {G}}\) and in \(\mathsf {GCIC} ^{\mathcal {N}}\) is given in full details in Section 5.3. In \(\mathsf {GCIC} ^{\uparrow }\) , \(\mathsf{Omega}\) fails in the same way as in \(\mathsf {GCIC} ^{\mathcal {N}}\) , but this does not break graduality because of the shifted universe level on \(\Pi\) types. A consequence of this stricter typing rule is that in \(\mathsf {GCIC} ^{\uparrow }\) , \(\mathsf{?_Typei -\gt ?_Typei precise ?_Typej}\) for any \(j \gt i\) , but \(\mathsf{?_Typei -\gt ?_Typei nprecise ?_Typei}\) . Therefore, the casts performed in \(\Omega\) do not come from an ep-pair anymore and can legitimately fail.

Another scenario where the differences in semantics manifest is functions with dependent arities. For instance, the well-known C function \(\mathsf{printf}\) can be embedded in a well-typed fashion in \(\mathsf {CIC}\) : It takes as first argument a format string and computes from it both the type and number of later arguments. This function brings out the limitation of \(\mathsf {GCIC} ^{\uparrow }\) : Since the format string can specify an arbitrary number of arguments, we need as many \(\rightarrow\) , and \(\mathsf{printf}\) cannot typecheck in a theory where universes are not closed under function spaces. In \(\mathsf {GCIC} ^{\mathcal {N}}\) , \(\mathsf{printf}\) typechecks but the same problem will appear dynamically when casting \(\mathsf{printf}\) to \(?\) and back to its original type: The result will be a function that works only on format strings specifying no more arguments than the universe level at which it has been typechecked. Note that this constitutes an example of violation of graduality for \(\mathsf {GCIC} ^{\mathcal {N}}\) , even of the dynamic gradual guarantee. Finally, in \(\mathsf {GCIC} ^{\mathcal {G}}\) the function can be gradualized as much as one wants, without surprises.

Which variant to pick?. As explained in the introduction, the aim of this article is to shed light on the design space of gradual dependent type theories, not to advocate for one specific design. We believe the appropriate choice depends on the specific goals of the language designer, or perhaps more pertinently, on the specific goals of a given project, at a specific point in time.

The key characteristics of each variant are:

In the same way that systems like \(\mathrm{Coq}\) , Agda, or Idris support different ways to customize their semantics (such as allowing Type-in-Type, switching off termination checking, using the partial/total compiler flags)—and of course, many programming languages implementations supporting some sort of customization, GHC being a salient representative—one can imagine a flexible realization of \(\mathsf {GCIC}\) that give users the control over the two parameters we identify in this work, and therefore have access to all three \(\mathsf {GCIC}\) variants. Considering the inherent tension captured by the Fire Triangle of Graduality, such a pragmatic approach might be the most judicious choice, making it possible to gather experience and empirical evidence about the pros and cons of each in a variety of concrete scenarios.

As explained in Section 2.4, in a gradual language, whenever we reclaim precision, we might be wrong and need to fail in order to preserve safety ( \(\mathcal {S}\) ). In a simply-typed setting, the standard approach is to define typing on the gradual source language, and then to translate terms via a type-directed cast insertion to a target cast calculus, i.e., a language with explicit runtime type checks, needed for a well-behaved reduction Siek and Taha 2006 . For instance, in a call-by-value language, the upcast (loss of precision) \(\langle {?} {\ \Leftarrow \ } {\mathbb {N}} \rangle \,{10}\) is considered a (tagged) value, and the downcast (gain of precision) \(\langle {\mathbb {N}} {\ \Leftarrow \ } {?} \rangle \,{v}\) reduces successfully if \(v\) is such a tagged natural number, or to an error otherwise.

We follow a similar approach for \(\mathsf {GCIC}\) , which is elaborated in a type-directed manner to a second calculus, named, \(\mathsf {CastCIC}\) (Section 5.1). The interplay between typing and cast insertion is however more subtle in the context of a dependent type theory. Because typing needs computation, and reduction is only meaningful in the target language, \(\mathsf {CastCIC}\) is used as part of the typed elaboration in order to compare types (Section 5.2). This means that \(\mathsf {GCIC}\) has no typing on its own, independent of its elaboration to the cast calculus. ⁹

In order to satisfy conservativity with respect to \(\mathsf {CIC}\) ( \(\mathcal {C}_{/{\mathsf {CIC}}}\) ), ascriptions in \(\mathsf {GCIC}\) are required to satisfy consistency: For instance, \(\mathsf{true::?::nat}\) is well-typed by consistency (twice), but \(\mathsf{true::nat}\) is ill typed. Such ascriptions in \(\mathsf {CastCIC}\) are realized by casts. For instance \(0\mathrel {::}?\mathrel {::}\mathbb {B}\) in \(\mathsf {GCIC}\) elaborates (modulo sugar and reduction) to \(\langle {\mathbb {B}} {\ \Leftarrow \ } {?_{[]}} \rangle \,{\langle {?_{[]}} {\ \Leftarrow \ } {\mathbb {N}} \rangle \,{0}}\) in \(\mathsf {CastCIC}\) . A major difference between ascriptions in \(\mathsf {GCIC}\) and casts in \(\mathsf {CastCIC}\) is that casts are not required to satisfy consistency: A cast between any two types is well-typed, although of course it might produce an error.

Finally, standard presentations of \(\mathsf {CIC}\) use a standalone conversion rule, as usual in declarative presentations of type systems. To gradualize \(\mathsf {CIC}\) , we have to move to a more algorithmic presentation in order to forbid transitivity, otherwise all terms would be well-typed by way of a transitive step through \(\mathsf{?}\) . But \(\mathcal {C}_{/{\mathsf {CIC}}}\) demands that only terms with explicitly-ascribed imprecision enjoy its flexibility. This observation is standard in the gradual typing literature Siek and Taha 2006 2007 Garcia et al. 2016. As in prior work on gradual dependent types Eremondi et al. 2019, we adopt a bidirectional presentation of typing for \(\mathsf {CIC}\) (Section 4), which allows us to avoid accidental transitivity and directly derive a deterministic typing algorithm for \(\mathsf {GCIC}\) .

To inform the design and justify the reduction rules provided for \(\mathsf {CastCIC}\) , we build a syntactic model of \(\mathsf {CastCIC}\) by translation to \(\mathsf {CIC}\) augmented with induction-recursion Martin-Löf 1996 Dybjer and Setzer 2003 Ghani et al. 2015 (Section 6.1). From a type theory point of view, what makes \(\mathsf {CastCIC}\) peculiar is first of all the possibility of having errors (both “pessimistic” as \(\mathsf{raise}\) and “optimistic” as \(\mathsf{?}\) ), and the necessity to do intensional type analysis in order to resolve casts. For the former, we build upon the work of Pédrot and Tabareau 2018 on the exceptional type theory \(\mathsf {ExTT}\) . For the latter, we reuse the technique of Boulier et al. 2017 to account for \(\mathsf{typerec}\) , an elimination principle for the universe \(\mathsf{Type}\) , which requires induction-recursion to be implemented.

We call the syntactic model of \(\mathsf {CastCIC}\) the discrete model, in contrast with a semantic model motivated in the next subsection. The discrete model of \(\mathsf {CastCIC}\) captures the intuition that the unknown type is inhabited by “hiding” the underlying type of the injected term. In other words, \(\mathsf{?_Typei}\) behaves as a dependent sum \(\mathsf{Sigma A:Typei. A}\) . Projecting out of the unknown type is realized through type analysis ( \(\mathsf{typerec}\) ), and may fail (with an error in the \(\mathsf {ExTT}\) sense). Note that here, we provide a particular interpretation of the unknown term in the universe, which is legitimized by an observation made by Pédrot and Tabareau 2018: \(\mathsf {ExTT}\) does not constrain in any way the definition of exceptions in the universe. The syntactic model of \(\mathsf {CastCIC}\) allows us to establish that the reduction semantics enjoys strong normalization ( \(\mathcal {N}\) ), for the two variants \(\mathsf {CastCIC} ^{\mathcal {N}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) . Together with safety ( \(\mathcal {S}\) ), this gives us weak logical consistency for \(\mathsf {CastCIC} ^{\mathcal {N}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) .

As explained earlier (Section 2.5), we need two different notions of precision to deal with SGG and \(\mathcal {G}\) . At the source level ( \(\mathsf {GCIC}\) ), we introduce a notion of syntactic precision that captures the intuition of a more imprecise term as “the same term with subterms and/or annotated types replaced by ?”, and is defined without any assumption of typing. In \(\mathsf {CastCIC}\) , we define a notion of structural precision, which is mostly syntactic except that, in order to account for cast insertion during elaboration, it tolerates precision-preserving casts (for instance, \(\langle {A} {\ \Leftarrow \ } {A} \rangle \,{t}\) is related to \(t\) by structural precision). Armed with these two notions of precision, we prove elaboration graduality (Theorem 24), which is the equivalent of SGG in our setting: If a term \(t\) of \(\mathsf {GCIC}\) elaborates to a term \(t^{\prime }\) of \(\mathsf {CastCIC}\) , then a term \(u\) less syntactically precise than \(t\) in \(\mathsf {GCIC}\) elaborates to a term \(u^{\prime }\) less structurally precise than \(t^{\prime }\) in \(\mathsf {CastCIC}\) .

Because DGG is about the behavior of terms, it is technically stated and proven for \(\mathsf {CastCIC}\) . We show in Section 5.5 that DGG can be proven for \(\mathsf {CastCIC}\) (in its variants \(\mathsf {CastCIC} ^{\mathcal {G}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) ) on the structural precision. However, as explained in Section 2.4, we cannot expect to prove \(\mathcal {G}\) for these \(\mathsf {CastCIC}\) variants with respect to structural precision directly. In order to overcome this problem, we build an alternative model of \(\mathsf {CastCIC}\) called the monotone model (Sections 6.2– 6.5). This model endows types with the structure of an ordered set, or poset. In the monotone model, we can reason about the semantic notion of propositional precision and prove that it gives rise to embedding-projection pairs New and Ahmed 2018, thereby establishing \(\mathcal {G}\) for \(\mathsf {CastCIC} ^{\uparrow }\) (Theorem 32). The monotone model only works for a normalizing gradual type theory, thus we then establish \(\mathcal {G}\) for \(\mathsf {CastCIC} ^{\mathcal {G}}\) using a variant of the monotone model based on Scott’s model Scott 1976 of the untyped \(\lambda\) -calculus using \(\omega\) -complete partial orders (Section 6.7).

Syntax. The syntax of \(\mathsf {CastCIC}\) ¹⁰ extends that of \(\mathsf {CIC}\) (Section 4) with three new term constructors: the unknown term \({?_T}\) and dynamic error \({{\rm \mathtt {err}}_T}\) of type \({T}\) , as well as the cast \({\langle {T} {\ \Leftarrow \ } {S} \rangle \,{t}}\) of a term \({t}\) of type \({S}\) to type \({T}\) with casts associating to the right: \({\langle {S^{\prime }} {\ \Leftarrow \ } {S} \rangle \,{\langle {T} {\ \Leftarrow \ } {T^{\prime }} \rangle \,{t}}}\) is \({\langle {S^{\prime }} {\ \Leftarrow \ } {S} \rangle \,{\left(\langle {T^{\prime }} {\ \Leftarrow \ } {T} \rangle \,{t}\right)}}\) . We also compress successive ones in the following way: \({\langle {T^{\prime \prime } \Leftarrow T^{\prime }} {\ \Leftarrow \ } {T} \rangle \,{t}}\) is shorthand for \({\langle {T^{\prime \prime }} {\ \Leftarrow \ } {T^{\prime }} \rangle \,{\langle {T^{\prime }} {\ \Leftarrow \ } {T} \rangle \,{t}}}\) . The unknown term and dynamic error both behave as exceptions as defined in \(\mathsf {ExTT}\) Pédrot and Tabareau 2018. Casts keep track of the use of consistency during elaboration, implementing a form of runtime type-checking, raising the error \({{\rm \mathtt {err}}_T}\) in case of a type mismatch. We call static the terms of \(\mathsf {CastCIC}\) that do not use any of these new constructors—static \(\mathsf {CastCIC}\) terms correspond to \(\mathsf {CIC}\) terms.

Universe parameters. \(\mathsf {CastCIC}\) is parametrized by two functions, described in Figure 2, to account for the three different variants of \(\mathsf {GCIC}\) we consider (Section 3.1). The first function \(s_\Pi\) computes the level of the universe of a dependent product, given the levels of its domain and codomain (see the updated Prod rule in Figure 3). The second function \(c_\Pi\) controls the universe level in the reduction of a cast between \(? \rightarrow ?\) and \(?\) (see Figure 5).

Typing. Figure 3 gives the typing rules for the three new primitives of \(\mathsf {CastCIC}\) . Apart from the modified Prod rule, which uses the \(s_\Pi\) parameter, all other typing rules are exactly the same as in \(\mathsf {CIC}\) . When disambiguation is needed, we note this typing judgment as \(\vdash _{{\rm \mathtt {cast}}}\) . The typing rules Unk and Err say that both \({?_T}\) and \({{\rm \mathtt {err}}_T}\) infer \({T}\) when \({T}\) is a type. Note that in \(\mathsf {CastCIC}\) , as is sometimes the case in cast calculi Siek and Wadler 2010 New and Ahmed 2018, no consistency premise is required for a cast to be well-typed. Here, consistency only plays a role in \(\mathsf {GCIC}\) , but disappears after elaboration. Instead, we rely on the usual conversion, defined as in \(\mathsf {CIC}\) as the existence of \(\alpha\) -equal reducts for the reduction described hereafter. The Case rule only ensures that both the source and target of the cast are indeed types, and that the casted term indeed has the source type.

Reduction. The typing rules provide little insight on the new primitives; the interesting part really lie in their reduction behavior. The reduction rules of \(\mathsf {CastCIC}\) are given in Figure 5 (congruence rules omitted). Reduction relies on two auxiliary functions relating head constructors \(h \in {\rm Head}\) (Figure 4) to those terms that start with either \(\Pi\) , \([]\) or \(I\) , the set of which we call \({\rm Type}_{\mathsf {CastCIC}}\) . The first is the function \(\mathrm{head}\,\) , which returns the head constructor of a type. In the other direction, the germ¹¹ function \({\rm germ}_{i}\,h\) constructs the least precise type with head \(h\) at level \(i\) . In the case, where no such type exists (e.g., when \(c_\Pi (i) \lt 0\) ), this least precise type is the error.

The design of the reduction rules is mostly dictated by the discrete and monotone models of \(\mathsf {CastCIC}\) presented later in Section 6. Nevertheless, we now provide some intuition about their meaning. Let us start with rules Prod-Unk, Prod-Err, Match-Unk, and Match-Err. These rules specify the exception-like propagation behavior of both \({?}\) and \({{\rm \mathtt {err}}}\) at product and inductive types. Rules Ind-Unk and Ind-Err similarly propagate \({?}\) and \({{\rm \mathtt {err}}}\) when cast between the same inductive type, and rules Down-Unk and Down-Err do the same from the unknown type to any type \({X}\) .

Next are rules Prod-Prod, Ind-Ind, and Univ-Univ, which correspond to success cases of dynamic checks, where the cast is between types with the same head. In that case, casts are either completely erased when possible, or propagated. As usual in gradual typing, directly inspired by higher-order contracts Findler and Felleisen 2002, Prod-Prod distributes the function cast in two casts, one for the argument and one for the body; note the substitution in the source codomain in order to account for dependency. Also, because constructors and inductives are fully-applied, this Prod-Prod rule cannot be blocked on a partially-applied constructor or inductive. Regarding inductive types, the restriction to reduce only on constructors means that a cast between \({\mathbb {N}}\) and \({\mathbb {N}}\) is blocked until its argument term is a constructor, rather than disappearing right away as for the universe. We follow this somewhat non-optimal strategy to be consistent between inductive types, because for more complex inductive types such as lists, the propagation of casts on subterms cannot be avoided.

On the contrary, rule Head-Err specifies failure of a dynamic check when the considered types have different heads. Similarly, rules Dom-Err, Codom-Err specify that cast to or from the error type is always an error.

Finally, there are specific rules pertaining to casts to and from \({?}\) , showcasing its behavior as a universal type. Rules Prod-Germ and Ind-Germ decompose an upcast into \({?}\) as an upcast to a germ followed by an upcast from the germ to \({?}\) . This decomposition of an upcast to \({?}\) into a series of “atomic” upcasts from a germ to \({?}\) is a consequence of the way the cast operation is implemented in Section 6, but similar decompositions appear, e.g., in Siek et al. 2015, where the equivalent of our germs are called ground types. The side conditions guarantee that this rule is used when no other applies. Rule Up-Down erases the succession of an upcast to \({?}\) and a downcast from it. Note that in this rule the upcast \({\langle {?_{[]_i}} {\ \Leftarrow \ } {{\rm germ}_{h}\,i} \rangle \,{t}}\) works like a constructor for \({?_{[]_i}}\) and \({\langle {X} {\ \Leftarrow \ } {?_{[]_i}} \rangle \,{}}\) as a destructor—a view reflected by the canonical and neutral forms of Figure 7 for \({?_{[]}}\) .¹² Finally, rule Size-Err corresponds to a peculiar kind of error, which only happens due to the presence of a type hierarchy: \({?_{[]_i}}\) is only universal with respect to types at level \(i\) , and so a type might be of a level too high to fit into it. To detect such a case, we check whether \(A\) is a germ for a level that is below \(i\) , and when not throw an error.

Meta-Theoretical Properties. The typing and reduction rules just given ensure two of the meta-theoretical properties introduced in Section 2: \(\mathcal {S}\) for the three variants of \(\mathsf {CastCIC}\) , as well as \(\mathcal {N}\) for \(\mathsf {CastCIC} ^{\mathcal {N}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) . Before turning to these properties, let us establish a crucial lemma, namely, the confluence of the rewriting system induced by reduction.

Let us now turn to \(\mathcal {S}\) , which we prove using the standard progress and subject reduction properties Wright and Felleisen 1994. Progress describes a set of canonical forms, asserting that all terms that do not belong to such canonical forms are not in normal form, i.e., can take at least one reduction step. Figure 7 provides the definition of canonical forms, considering head reduction.

As standard in dependent type theories, we distinguish between canonical forms and neutral terms. Neutral terms correspond to (blocked) destructors, waiting for a substitution to happen, while other canonical forms correspond to constructors. Additionally, the notion of neutral terms naturally induces a weak-head reduction strategy that consists of either applying a top-level reduction or reducing the (only) argument of the top-level destructor that is in a neutral position.

The canonical forms for plain \(\mathsf {CIC}\) are given by the first three lines of Figure 7. The added rules deal with errors, unknown terms, and casts. First, an error \({{\rm \mathtt {err}}_t}\) or an unknown term \({?_t}\) is neutral when \({t}\) is neutral, and is canonical only when \({t}\) is \({[]}\) or \({I(\mathbf {a})}\) , but not a \(\Pi\) -type. This is because exception-like terms reduce on \(\Pi\) -types Pédrot and Tabareau 2018. Second, there is an additional specific form of canonical inhabitants of \({?_{[]}}\) : These are upcasts from a germ, which can be seen as a term tagged with the head constructor of its type, in a matter reminiscent of actual implementations of dynamic typing using type tags. As we explained when presenting Figure 5, these canonical forms work as constructors for \({?_{[]}}\) . Finally, the cast operation behaves as a destructor on the universe \({[]}\) —as if it were an inductive type of usual \(\mathsf {CIC}\) . This destructor first scrutinizes the source type of the cast. This is why the cast is neutral as soon as its source type is neutral. When the source type reduces to a head constructor, there are two possibilities. Either that constructor is \({?_{[]}}\) , in which case the cast scrutinizes its argument to be a canonical form \({\langle {?_{[]}} {\ \Leftarrow \ } {t} \rangle \,{{\rm germ}_{i}\,h}}\) and is neutral when this is not the case. In all other cases, it first scrutinizes the target type, so the cast is neutral when the target type is neutral. Finally, when both types have head constructors, the cast might still need its argument to be either a \(\lambda\) -abstraction or an inductive constructor to reduce.

Equipped with the notion of canonical forms, we can state \(\mathcal {S}\) for \(\mathsf {CastCIC}\) :

We now establish normalization of \(\mathsf {CastCIC} ^{\mathcal {N}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) , although the proof below relies on the discrete model defined in Section 6.1.

Now that \(\mathsf {CastCIC}\) has been described, we move on to \(\mathsf {GCIC}\) . The typing judgment of \(\mathsf {GCIC}\) is defined by an elaboration judgment from \(\mathsf {GCIC}\) to \(\mathsf {CastCIC}\) , based upon Figure 1, augmenting all judgments with an extra output: the elaborated \(\mathsf {CastCIC}\) term. This definition of typing using elaboration is required because of the intricate interdependency between typing and reduction exposed in Section 3.

Syntax. The syntax of \(\mathsf {GCIC}\) ¹³ extends that of \(\mathsf {CIC}\) with a single new term constructor \({?@\lbrace i\rbrace }\) , where \(i\) is a universe level. From a user perspective, one is not given direct access to the failure and cast primitives, those only arise through uses of \({?}\) .

Consistent conversion. Before we can describe typing, we should focus on conversion. Indeed, to account for the imprecision introduced by \({?}\) , elaboration employs consistent conversion to compare \(\mathsf {CastCIC}\) terms rather than usual conversion relation.

Thus \(\alpha\) -consistency is an extension of \(\alpha\) -equality that takes imprecision into account. Apart from the standard rules making \({?}\) consistent with any term, \(\alpha\) -consistency optimistically ignores casts, and does not consider errors to be consistent with themselves. The first point is to prevent casts inserted by the elaboration from disrupting valid conversions, typically between static terms. The second is guided by the idea that if errors are encountered at elaboration already, the term cannot be well behaved, so it must be rejected as early as possible and we should avoid typing it. The consistency relation is then built upon \(\alpha\) -consistency in a way totally similar to how conversion in Figures 1 and 5 is built upon \(\alpha\) -equality. Also note that this formulation of consistent conversion makes no assumption of normalization, and is therefore usable as such in the non-normalizing \(\mathsf {GCIC} ^{\mathcal {G}}\) .

An important property of consistent conversion, and a necessary condition for the conservativity of \(\mathsf {GCIC}\) with respect to \(\mathsf {CIC}\) ( \(\mathcal {C}_{/{\mathsf {CIC}}}\) ), is that it corresponds to conversion on static terms.

Elaboration. Elaboration from \(\mathsf {GCIC}\) to \(\mathsf {CastCIC}\) is given in Figure 9, closely following the bidirectional presentation of \(\mathsf {CIC}\) (Figure 1) for most rules, simply carrying around the extra elaborated terms. Note that only the subject of the judgment is a source term in \(\mathsf {GCIC}\) ; other inputs (that have already been elaborated), as well as outputs (that are to be constructed), are target terms in \(\mathsf {CastCIC}\) . Let us comment a bit on the specific modifications and additions compared to Figure 1.

The most salient feature of elaboration is the insertion of casts that mediate between merely consistent but not convertible types. They of course are needed in the rule Check where the terms are compared using consistency. But this is not enough: Casts also appear in the newly-introduced rules Inf-Univ? Inf-Prod? and Inf-Ind? for constrained inference, where the type \({?_{[]_i}}\) is replaced by the least precise type of the appropriate universe level having the constrained head constructor, which is exactly what the \({\rm germ}\) function gives us. Note that in the case of Inf-Univ? we could have replaced \({[]_i}\) with \({{\rm germ}_{i+1}\,[]_i}\) to make for a presentation similar to the other two rules. The role of these three rules is to ensure that a term of type \({?_{[]_i}}\) can be used as a function, or as a scrutinee of a match, by giving a way to derive constrained inference for such a term.

It is interesting to observe that the rules for constrained elaboration in a gradual setting bear a close resemblance with those described by Cimini and Siek 2016Section 3.3, where a matching operator is introduced to verify that an output type can fit into a certain type constructor—either by having that type constructor as head symbol or by virtue of being \(?\) . Such a form of matching was already present in our static, bidirectional system, because of the presence of reduction in types. In a way, both Cimini and Siek 2016 and Lennon-Bertrand 2021 have the same need of separating the inferred type from operations on it to recover its head constructor, and our mixing of both computation and gradual typing makes that need even clearer.

Rule Unk also deserves some explanation: \({?@\lbrace i\rbrace }\) is elaborated to \({?_{?_{[]_i}}}\) , the least precise term of the least precise type of the whole universe \({[]_i}\) . This avoids unneeded type annotations on \({?}\) in \(\mathsf {GCIC}\) . Instead, the context is responsible for inserting the appropriate cast, e.g., \({?\mathrel {::}T}\) elaborates to a term reducing to \({?_T}\) . We do not drop annotations altogether because of an important property on which bidirectional \(\mathsf {CIC}\) is built: any well-formed term should infer a type, not just check. Thus, we must be able to infer a type for \({?}\) . The obvious choice is to have \({?}\) infer \({?}\) , but this \({?}\) is a term of \(\mathsf {CastCIC}\) , and thus needs a type index. Because this \({?}\) is used as a type, this index must be \({[]}\) , and the universe level of the source \({?}\) is there to give us the level of this \({[]}\) . In a real system, this should be handled by typical ambiguity,¹⁴ alleviating the user from the need to give any annotations when using \({?}\) .

Direct properties. As the elaboration rules are completely syntax-directed, they immediately translate to an algorithm for elaboration. Coupled with decidability of consistency (Proposition 10), this makes elaboration decidable whenever \({\rm {\leadsto }^\ast }\) is normalizing; when \({\rm {\leadsto }^\ast }\) is not normalizing, the elaboration algorithm might diverge, resulting in only semi-decidability of typing (as in, for instance, Dependent Haskell Eisenberg 2016).

Let us now establish two important properties of elaboration that we can prove at this stage: elaboration is correct, insofar as it produces well-typed \(\mathsf {CastCIC}\) terms, and functional, in the sense that a given \(\mathsf {GCIC}\) term can be elaborated to at most one \(\mathsf {CastCIC}\) term up to conversion.

Because of the absence of a fixed, deterministic reduction strategy, the elaborated term is not unique. Indeed, since a type can be reduced to multiple product types in rule Section Prod, a term can infer multiple, different types, and since those appear later on in casts, the elaborated terms can differ by having different, albeit convertible, types in their casts. We thus state two theorems: One is uniqueness up to conversion, in case full reduction is used. The second is a strengthening if a weak-head reduction strategy is imposed for reduction.

(Recall that conversion \(\equiv\) in \(\mathsf {CastCIC}\) is defined (similarly as in \(\mathsf {CIC}\) ) as the existence of \(\alpha\) -equal reducts for the reduction given in Figure 5.)

Now that \(\mathsf {GCIC}\) has been entirely presented, let us come back to the important example of \({\Omega }\) , and explain in detail the behavior described in Section 3.1 for the three \(\mathsf {GCIC}\) variants.

Recall that \({\Omega }\) is the term \({\delta ~\delta }\) , with \({\delta } := {{\rm \lambda }x : ?@\lbrace i+1\rbrace . x~x}\) . We leave out the casts present in Sections 2 and 3, knowing that they will be introduced by elaboration. We also use \({?}\) at level \(i + 1\) , because \({?@\lbrace i+1\rbrace }\) , when elaborated as a type, becomes \({T} := {\langle {[]_i} {\ \Leftarrow \ } {?_{[]_{i+1}}} \rangle \,{?_{?_{[]_{i+1}}}}}\) , such that \({T} {\rm {\leadsto }^\ast }{?_{[]_i}}\) . For the rest of this section, we write \({?_{j}}\) instead of \({?_{[]_j}}\) to avoid stacked indices and ease readability.

If \(i = 0\) the elaboration of \({\delta }\) (and thus of \({\Omega }\) ) fails in \(\mathsf {GCIC} ^{\uparrow }\) and \(\mathsf {GCIC} ^{\mathcal {N}}\) , because the inferred type for \(x\) is \({T}\) , which reduces to \({?_0}\) . Then, because \(c_\Pi (0) = -1 \lt 0\) in both \(\mathsf {GCIC} ^{\uparrow }\) and \(\mathsf {GCIC} ^{\mathcal {N}}\) , rule Inf-Prod? does not apply and \({\delta }\) is deemed ill-typed, as is \({\Omega }\) .

Otherwise, if \(i \gt 0\) or we are considering \(\mathsf {GCIC} ^{\mathcal {G}}\) , \({\delta }\) can be elaborated, and we haveFrom this, we get that \({\Omega }\) also elaborates, namely (with \({\delta ^{\prime }}\) the elaboration of \({\delta }\) above)Let us now look at the reduction behavior of this elaborated term \({\Omega ^{\prime }}\) in the three systems: It reduces seamlessly when \(c_\Pi (i) = i\) ( \(\mathsf {GCIC} ^{\mathcal {G}}\) / \(\mathsf {CastCIC} ^{\mathcal {G}}\) ), while having \(c_\Pi (i) \lt i\) makes it fail ( \(\mathsf {GCIC} ^{\uparrow }\) / \(\mathsf {CastCIC} ^{\uparrow }\) and \(\mathsf {GCIC} ^{\mathcal {N}}\) / \(\mathsf {CastCIC} ^{\mathcal {N}}\) ). The reduction of \({\Omega ^{\prime }}\) in \(\mathsf {CastCIC} ^{\mathcal {G}}\) is as follows:The first step is the identity, simply replacing \({\Omega ^{\prime }}, c_\Pi (i),\) and the first occurrence of \({\delta ^{\prime }}\) by their definitions. The second reduces \({T}\) to \({?_i}\) . In the third, the casted \({\delta {}^{\prime }}\) is substituted for \({x}\) by a \(\beta\) step. Casts are finally simplified using Up-Down and Prod-Prod. At that point, the reduction has almost looped back to the second step, apart from the casts \({\langle {?_i} \Leftarrow {?_i}\rangle }\) in the first occurrence of \({\delta ^{\prime }}\) , which will simply accumulate through reduction, but without hindering divergence.

On the contrary, the normalizing variants have \(c_\Pi (i) \lt i\) , and thus share the following reduction path:The first step corresponds to the first three above, the only difference being the value of \(c_\Pi (i)\) . The reductions however differ in the next step because \({?_i \rightarrow ?_{i-1}} \ne {{\rm germ}_{i}\,\Pi }\) , so Prod-Germ applies before Up-Down. For the third step, note that \({?_{i-1} \rightarrow ?_{i-1}} = {{\rm germ}_{i}\,\Pi }\) , so that Down-Err applies in the rightmost sequence of casts. The last three steps of reduction then propagate the error by first using Prod-Germ, Up-Down, and Prod-Prod, then the \(\beta\) rule, and finally Down-Err, Err and a last \(\beta\) step. At a high-level, the error can be seen as a dynamic universe inconsistency, triggered by the invalid downcast highlighted on the first line.

Establishing the graduality of elaboration—the formulation of the SGG in our setting—is no small feat, as it requires properties about computations in \(\mathsf {CastCIC}\) that amount to the DGG. Indeed, to handle the typing rules for checking and constrained inference, it is necessary to know how consistency and reduction evolve as a type becomes less precise. As already explained in Section 3.4, we cannot directly prove graduality for a syntactic notion of precision. However, we can still show that this relation is a simulation for reduction. While weaker than graduality, this property implies the DGG and suffices to conclude that graduality of elaboration holds. The purpose of this section is to establish it. Our proof is partly inspired by the proof of DGG by Siek et al. 2015.¹⁵ We however had to adapt to the much higher complexity of \(\mathsf {CIC}\) compared to \(\mathsf {STLC}\) . In particular, the presence of computation in the domain and codomain of casts is quite subtle to tame, as we must in general reduce types in a cast before we can reduce the cast itself.¹⁶

Technically, we need to distinguish between two notions of precision, one for \(\mathsf {GCIC}\) and one for \(\mathsf {CastCIC}\) : (i) syntactic precision on terms in \(\mathsf {GCIC}\) , which corresponds to the usual syntactic precision of gradual typing Siek et al. 2015, (ii) structural precision on terms in \(\mathsf {CastCIC}\) , which corresponds to syntactic precision together with a proper account of casts. In this section, we concentrate on properties of structural precision in \(\mathsf {CastCIC}\) . We only state and discuss the various lemmas and theorems on a high level, and refer the reader to Appendix B.2 for the detailed proofs.

Structural precision for \(\mathsf {CastCIC}\) . As emphasized already, the key property we want to establish is that precision is a simulation for reduction, i.e., that less precise terms reduce at least as well as more precise ones. This property guides the quite involved definition we are about to give for structural precision: It is rigid enough to give the induction hypotheses needed to prove simulation, while being lax enough to be a consequence of syntactic precision after elaboration, which is the key point to establish elaboration graduality (Theorem 24), our equivalent of the static gradual guarantee.

Similarly to \(\sim _{\alpha }\) , precision can ignore some casts, in order to handle casts that might appear or disappear in one term but not the other during reduction. But in order to control what casts can be ignored, we impose some restriction on the types involved. In particular, we want to ensure that ignored casts would not have raised an error: e.g., We want to prevent \({0} \sqsubseteq _{\alpha }{\langle {\mathbb {B}} {\ \Leftarrow \ } {\mathbb {N}} \rangle \,{0}}\) . Thus, the definition of structural precision relies on typing, and to do this we need to record the contexts of the two compared terms. We do so by using double-struck letters to denote contexts where each variable is given two types, writing \({\mathbb {\Gamma }, x : A \mid A^{\prime }}\) for context extensions. We use \({\mathbb {\Gamma }_i}\) for projections, i.e., \({(\mathbb {\Gamma }, x : A \mid A^{\prime })_{1}} := {\mathbb {\Gamma }_{1}, x : A}\) , and write \({\Gamma \mid \Gamma ^{\prime }}\) for the converse pairing operation.

Although \({\mathbb {\Gamma }} \vdash {t}\sqsubseteq _{\leadsto }{t^{\prime }}\) is defined in a stepwise way, it is equivalent to the existence of \({s}\) and \({s^{\prime }}\) such that \({t} {\rm {\leadsto }^\ast }{s}\) , \({t^{\prime }} {\rm {\leadsto }^\ast }{s^{\prime }}\) and \({\mathbb {\Gamma }} \vdash {s} \sqsubseteq _{\alpha }{s^{\prime }}\) . The situation is the same as for consistency (respectively, conversion), which is the closure by reduction of \(\alpha\) -consistency (respectively, \(\alpha\) -equality). However, here definitional precision is also used in the definition of structural precision, in order to permit computation in types—recall that in a dependently-typed setting the two types involved in a cast may need to reduce before the cast itself can reduce—and thus the two notions are mutually defined.

Let us now explain the rules defining structural precision. Diagonal rules are completely structural, apart from the Diag-Fix rule, where typing assumptions provide us with the contexts needed to compare the predicates. More interesting are the non-diagonal rules. First, \({?_{T}}\) is greater than any term of the “right type”. This incorporates loss of precision (rule Unk), and accommodates for a small bit of cumulativity (rule Unk-Univ). This is needed because of technical reasons linked with possibility to form products between types at different levels. On the contrary, the error is smaller than any term (rule Err), even in its extended form on \(\Pi\) -types (rule Err-Lambda), with a typing premise similar to that of rule Unk. Finally, casts on the right-hand side can be ignored as long as they are performed on types that are less precise than the type of the term on the left (rule Case-R). Dually, casts on the left-hand side can be ignored as long as they are performed on types that are more precise than the type of the term on the right (rule Case-L).

Catch-up lemmas. The fact that structural precision is a simulation relies on a series of lemmas that all have the same form: under the assumption that a term \({t^{\prime }}\) is less precise than a term \({t}\) with a known head ( \({[]}\) , \({{\rm \Pi }}\) , \({I}\) , \({\lambda ,}\) or \({c}\) ), the term \({t^{\prime }}\) can be reduced to a term that either has the same head, or is some \({?}\) . We call these catch-up lemmas, as they enable the less precise term to catch up to the more precise one whose head is already known. Their aim is to ensure that casts appearing in a less precise term never block reduction, as they can always be reduced away.

The lemmas are established in a descending fashion: First, on the universe in Lemma 15, then on other types in Lemma 16, and finally on terms, namely, on \(\lambda\) -abstractions in Lemma 17 and inductive constructors in Lemma 18. Each time, the previously proven catch-up lemmas are used to reduce types in casts appearing in the less precise term, apart from Lemma 15, where the induction hypothesis of the lemma being proven is used instead.

Note that for Lemma 18, we need to deal with unknown terms specifically, which is not necessary for Lemma 17 because the unknown term in a \(\Pi\) -type reduces to a \(\lambda\) -abstraction.

Lemma 17 deserves a more extensive discussion, because it is the critical point where the difference between the three variants of \(\mathsf {CastCIC}\) manifests. In fact, it does not hold in full generality for \(\mathsf {CastCIC} ^{\mathcal {N}}\) . Indeed, the fact that \(i \le c_\Pi (s_\Pi (i,j))\) and \(j \le c_\Pi (s_\Pi (i,j))\) is used crucially to ensure that casting from a \(\Pi\) -type into \({?}\) and back does not reduce to an error, given the restrictions on types in Case-R. This is the manifestation in the reduction of the embedding-projection property New and Ahmed 2018. In \(\mathsf {CastCIC} ^{\mathcal {N}}\) , it holds only if one restricts to terms without \({?}\) , where such casts never happen. This is important with regard to conservativity, as elaboration produces terms with casts but without \({?}\) , and Lemma 17 ensures that for those precision is still a simulation, even in \(\mathsf {CastCIC} ^{\mathcal {N}}\) .

Note that in an actual implementation with typical ambiguity (Footnote 14), the case where \(i = 0\) would most likely not manifest: elaborating \({\left(({\rm \lambda }x : \mathbb {N}. \texttt {suc}(x))\mathrel {::}?\right)~0}\) would produce a fresh level that could be chosen high enough so as to prevent the error we just described. Only more involved situations like that of \({\Omega }\) (Section 5.3) would actually exhibit failures due to universe levels, which are precisely those unavoidable to ensure normalization.

Simulation. We finally come to the main property of this section, the advertised simulation. Remark that the simulation property needs to be stated (and proven) mutually for structural and definitional precision, but it is really informative only for structural precision (definitional precision is somehow a simulation by construction).

From this theorem, we get as direct corollaries the following properties, that are required to handle reduction (Corollary 21) and consistency (Corollary 22) in elaboration. Again those corollaries hold in \(\mathsf {GCIC} ^{\mathcal {G}}\) , \(\mathsf {GCIC} ^{\uparrow }\) , and for terms in \(\mathsf {GCIC} ^{\mathcal {N}}\) containing no \({?}\) .

We now have enough technical tools to prove most of the properties of \(\mathsf {GCIC}\) . We state those theorems in an empty context in this section to make them more readable, but they are of course corollaries of similar statements including contexts, proven by mutual induction. The complete statements and proofs can be found in Appendix B.3.

Conservativity with respect to \(\mathsf {CIC}\) . Elaboration systematically inserts casts during checking, thus even static terms are not elaborated to themselves. Therefore, we use a (partial) erasure function \(\varepsilon\) that translates terms of \(\mathsf {CastCIC}\) to terms of \(\mathsf {CIC}\) by erasing all casts. We also introduce the notion of erasability, characterizing terms that contain “harmless” casts, such that in particular the elaboration of a static term is always erasable.

Conservativity holds in all three systems, typeability being of course taken into the corresponding variant of \(\mathsf {CIC}\) : full \(\mathsf {CIC}\) for \(\mathsf {GCIC} ^{\mathcal {G}}\) and \(\mathsf {GCIC} ^{\mathcal {N}}\) , and \(\mathsf {CIC}^{\uparrow }\) for \(\mathsf {GCIC} ^{\uparrow }\) .

Elaboration Graduality. Next, we turn to elaboration graduality, the equivalent of the SGG of Siek et al. 2015 in our setting. We state it with respect to a notion of precision for terms in \(\mathsf {GCIC}\) , syntactic precision \(\sqsubseteq ^{\mathrm{G}}_{\alpha }\) , defined in Figure 11. Syntactic precision is the usual and expected source-level notion of precision in gradual languages: It is generated by a single non-trivial rule \({t} \sqsubseteq ^{\mathrm{G}}_{\alpha }{?@\lbrace i\rbrace }\) , and congruence rules for all term formers.

In contrast with the simply-typed setting, the presence of multiple unknown types \({?}\) , one for each universe level \({i}\) , requires an additional hypothesis relating elaboration and precision. We say that two judgments \({\tilde{t}} \sqsubseteq ^{\mathrm{G}}_{\alpha }{?@\lbrace i\rbrace }\) and \({\Gamma } \vdash {\tilde{t}} {\rm \rightsquigarrow }{t} {\rm \triangleright }{T}\) are universe adequate if the universe level \(j\) given by the well-formedness judgment \({\Gamma } \vdash {T} \blacktriangleright {\square } {\square _j}\) induced by correction of the elaboration satisfies \(i = j\) . More generally, \({\tilde{t}} \sqsubseteq ^{\mathrm{G}}_{\alpha }{\tilde{s}}\) and \({} \vdash {\tilde{t}} {\rm \rightsquigarrow }{t} {\rm \triangleright }{T}\) are universe adequate if for any subterm \({\tilde{t}_0}\) of \({\tilde{t}}\) inducing judgments \({\tilde{t}_0} \sqsubseteq ^{\mathrm{G}}_{\alpha }{?@\lbrace i\rbrace }\) and \({\Gamma _0} \vdash {\tilde{t}_0} {\rm \rightsquigarrow }{t} {\rm \triangleright }{T}\) , those are universe adequate. Note that this extraneous technical assumption on universe levels is not needed if we use typical ambiguity (Footnote 14), since universe levels are not given explicitly.

Dynamic Gradual Guarantee. Following Siek et al. 2015, using the fact that structural precision is a simulation (Theorem 20), we can prove the DGG for \(\mathsf {CastCIC} ^{\mathcal {G}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) (stated using the notion of observational refinement \(\sqsubseteq ^{obs}\) from Definition 4).

Note that Example 19 provides a counter-example to this theorem for \(\mathsf {CastCIC} ^{\mathcal {N}}\) , by choosing the context \({{\rm \mathtt {ind}}_{\mathbb {N}}(\bullet ~0,z.\mathbb {B},f.\mathtt {true},f.n.\mathtt {true})}\) , because in that context the function \({{\rm \lambda }x : \mathbb {N}. \texttt {suc}(x)}\) reduces to \({\mathtt {true}}\) while the less precise casted function reduces to \({{\rm \mathtt {err}}_{\mathbb {B}}}\) .

As observed in Section 2.4, graduality—and in particular the fact that precision induces ep-pair s —is inherently semantic, and thus cannot rely on the syntactic precision \(\sqsubseteq ^{\mathrm{G}}_{\alpha }\) introduced in this section. Therefore, we defer the proof of \(\mathcal {G}\) for \(\mathsf {CastCIC} ^{\uparrow }\) and \(\mathsf {CastCIC} ^{\mathcal {G}}\) to the next section, where the semantic notion of propositional precision is introduced.

The discrete model explains away the new term formers of \(\mathsf {CastCIC}\) (2) by a translation into \(\mathsf {CIC}\) using two important ingredients from the literature:

The latter ingredient for intensional type analysis requires the target theory of the translation to be an extension of \(\mathsf {CIC}\) with induction-recursion Dybjer and Setzer 2003, noted \(\mathsf {CIC^{IR}}\) . We write \(\leadsto _{\mathrm{IR}}\) and \({\vdash _{\mathrm{IR}}}\) to denote the reduction and typing judgments of \(\mathsf {CIC^{IR}}\) , respectively.

Inductive types. Following the general pattern of \(\mathsf {ExTT}\) , we interpret each inductive type \(I\) by an inductive type \(\ddot{I}\) featuring all constructors of \(I\) and extended with two new constructors \(\top _{\ddot{I}}\) and \(\bot _{\ddot{I}}\) , corresponding respectively to \(?_{I}\) and \({\rm \mathtt {err}}_I\) of \(\mathsf {CastCIC}\) . The constructors \(\top _{\ddot{I}}\) and \(\bot _{\ddot{I}}\) of \(\ddot{I}\) are called exceptional by opposition to the other constructors that we call non-exceptional. For instance, the inductive type used to interpret natural numbers, \(\ddot{\mathbb {N}}{}\) , thus has four constructors: The non-exceptional constructors 0 and \(\texttt {suc}\) , and the exceptional constructors \(\top _{\ddot{\mathbb {N}}}\) , \(\bot _{\ddot{\mathbb {N}}}\) . In the rest of this section, we only illustrate inductive types on natural numbers.

Universe and type-case. Case analysis on types is obtained through an explicit inductive-recursive description of the universes Martin-Löf 1984 McBride 2010 to build a type of codes \(\square \!\!\!\! \square _i\) described in Figure 12. Codes are noted with \(\widehat{\cdot }\) and the universe type contains codes for dependent product ( \(\widehat{\Pi }\) ), universes ( \(\widehat{\square \!\!\!\! \square }_j\) ), inductive types (e.g., \(\widehat{\mathbb {N}}\) ) as well as \(\widehat{?}_{}\) for the unknown type and \(\widehat{{\rm \mathtt {err}}_{}}\) for the error type. The main subtlety here is that the code \(\widehat{\Pi }\,A\,B\) is at level \(s_\Pi (i,j)\) when \(A\) is at \(i\) and \(B\) is a family at \(j\) , emulating the rule of Figure 3. Accompanying the inductive definition of \(\square \!\!\!\! \square _i\) , the recursively defined decoding function \(\mathrm{El}\) provides a semantics for these codes. The semantics of \(\widehat{\Pi }\) is given by the dependent product in the target theory, applying \(\mathrm{El}\) on the domain and the codomain of the code. The semantics of \(\widehat{\square \!\!\!\! \square }_j\) is precisely the type of codes \(\square \!\!\!\! \square _j\) . The semantics of \(\widehat{\mathbb {N}}\) is given by the extended natural numbers \(\ddot{\mathbb {N}}\) , explained above.

Intuitively, the semantics of \(\widehat{?}_{i}\) is that an inhabitant of the unknown type corresponds to a pair of a type and an inhabitant of that type. More precisely, we first define a notion of germ for codes where we stratify the head constructors \({\rm Head}\) (see Figure 4) according to the universe level \(i\) , e.g., \(\widehat{{\rm germ}}_{i}\,\Pi := \widehat{\Pi }\,\widehat{\square \!\!\!\! \square }_{c_\Pi (i)}\,(\lambda (x : \square \!\!\!\! \square _{c_\Pi (i)}).\widehat{\square \!\!\!\! \square }_{c_\Pi (i)})\) when \(c_\Pi (i) \ge 0\) , and its decoding to types \({\rm germ}_{i}\,h := \mathrm{El}\,(\widehat{{\rm germ}}_{i}\,h)\) . The unknown type \(\widehat{?}_{i}\) is then decoded to the extended dependent sum \({\ddot{\Sigma }}\, {\rm Head}_i \, {\rm germ}_{i}\,\) whose elements are either

Finally, the error type \(\widehat{{\rm \mathtt {err}}_{i}}\) is decoded to the unit type \(\mathtt {unit}\) containing a unique element \(\mathtt {()}\) .

Variants of \(\mathsf {CastCIC}\) . Crucially, the code for \(\Pi\) -types (Figure 12) depends on the choice made for \(s_\Pi (i,j)\) . Observe that for the choice of parameters corresponding to \(\mathsf {CastCIC} ^{\mathcal {G}}\) , the inductive-recursive definition of \(\square \!\!\!\! \square _i\) is ill-founded since \(c_\Pi (s_\Pi (i,i)) = s_\Pi (i,i)\) . We can thus inject \({\rm germ}{}_{s_\Pi (i,i)}\Pi = \mathrm{El}\,\widehat{?}_{}{s_\Pi (i,i)} \rightarrow \mathrm{El}\,\widehat{?}_{}{s_\Pi (i,i)}\) into \(\mathrm{El}\,\widehat{?}_{}{s_\Pi (i,i)}\) and project back in the other direction, exhibiting an embedding-retraction suitable to interpret the untyped \(\lambda\) -calculus and hence \(\Omega\) . ¹⁷

In order to maintain normalization, the construction of the unknown type and the universe therefore needs to be stratified, which is possible when \(c_\Pi (s_\Pi (i,i)) \lt s_\Pi (i,i)\) . This strict inequality occurs for both \(\mathsf {CastCIC} ^{\mathcal {N}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) . We then proceed by strong induction on the universe level, and note that thanks to the level gap, the decoding \(\mathrm{El}\,\widehat{?}_{i}\) of the unknown type at a level \(i\) can be defined solely from the data of smaller universes available by inductive hypothesis, without any reference to \(\square \!\!\!\! \square _i\) . We can then define the rest of the universe \(\square \!\!\!\! \square _i\) and the decoding function \(\mathrm{El}\) at level \(i\) in a well-founded manner, validating the strict positivity criterion of Agda’s termination checker.

Exceptions. The definition of exceptions \(?_{A}, {\rm \mathtt {err}}_{A} : \mathrm{El}~A\) at an arbitrary code \(A\) then follows by case analysis on the code, as shown in Figure 13. On the code for the universe, \(\widehat{\square \!\!\!\! \square }_j\) , we directly use the code for the unknown and the error types respectively. On codes that have an inductive interpretation— \(\widehat{\mathbb {N}}\) , \(\widehat{?}_{i}\) —we use the two added constructors. On the code for dependent functions, exceptions are defined by re-raising the exception at the codomain in a pointwise fashion. Finally, on the error type \(\widehat{{\rm \mathtt {err}}_{}}\) , exceptions are degenerated and forced to take the only value \(\mathtt {()}:\mathtt {unit}\) ¹⁸ of its interpretation as a type.

Casts. Equipped with exceptions and type analysis, we define \({\rm \mathtt {cast}}: {\rm \Pi }(A : \square \!\!\!\! \square _i)(B : \square \!\!\!\! \square _j). A \rightarrow B\) by induction on the universe levels and case analysis on the codes of the types \(A\) and \(B\) (Figure 14). In the total setting (when \(c_\Pi (s_\Pi (i,i)) \lt s_\Pi (i,i)\) ), the definition of \({\rm \mathtt {cast}}\) is well-founded: each recursive call happens either at a strictly smaller universe (the two cases for \(\widehat{\Pi }\) ) or on a strict subterm of the term being cast (case of inductives, i.e., \(\widehat{\mathbb {N}}\) and \(\widehat{?}_{}\) ). Note that each of the defining equations of \({\rm \mathtt {cast}}\) corresponds straightforwardly to a reduction rule of Figure 5.

Discrete translation. We can finally define the discrete syntactic model of \(\mathsf {CastCIC}\) in \(\mathsf {CIC^{IR}}\) (Figure 15). The translations \([{{-}}]\) and \([\![ {}{{-}}]\!] {}\) are defined by induction on the syntax of terms and types. A type \(A\) is translated to its corresponding code \([{{A}}]\) in \(\square \!\!\!\! \square _i\) when seen as a term, and is translated to the interpretation of this code \([\![ {}{{A}}]\!] {} := \mathrm{El}\,[{{A}}]\) when seen as a type. \(?_A\) and \({\rm \mathtt {err}}_A\) are directly translated using the exceptions defined in Figure 13. The following theorem shows that the translation is a syntactic model in the sense of Boulier et al. 2017.

As explained in Theorem 9, Theorem 26 implies in particular that \(\mathsf {CastCIC} ^{\uparrow }\) and \(\mathsf {CastCIC} ^{\mathcal {N}}\) are strongly normalizing.

The simplicity of the discrete model comes at the price of an inherent inability to characterize which casts are guaranteed to succeed, i.e., a graduality theorem. To overcome this limitation, we develop a monotone model on top of the discrete model where, by construction, each type \(A\) comes equipped with an order structure \(\sqsubseteq ^A\) —a reflexive, transitive, antisymmetric, and proof-irrelevant relation—modeling precision between terms. In particular, the exceptions \({\rm \mathtt {err}}_A\) and \(?_A\) correspond respectively to the smallest and greatest element of \(A\) for this order. We note \(\square ^\le\) for a universe of types equipped with the structure of a poset together with smallest and greatest elements. Each term and type constructor is enforced to be monotone with respect to these orders, providing a strong form of graduality. This implies in particular that such a model cannot be defined for \(\mathsf {CastCIC} ^{\mathcal {N}}\) because this type theory lacks graduality, as shown by Example 19.

As an illustration, the order on extended natural numbers (Figure 16) makes \(\bot _{\ddot{\mathbb {N}}}\) the smallest element and \(\top _{\ddot{\mathbb {N}}}\) the biggest element.¹⁹ The standard natural numbers – 0 or \(\texttt {suc}~n\) for a standard natural number \(n\) —then stand between failure and indeterminacy, but are never related to each other by precision. Indeed, in order to ensure conservativity with respect to \(\mathsf {CIC}\) , \(\sqsubseteq ^{\widehat{\mathbb {N}}{}}\) must coincide with \(\mathsf {CIC}\) ’s conversion on static closed natural numbers.

Beyond the precision order on types, the nature of dependency forces us to spell out what the precision between types entails. Following the analysis of New and Ahmed 2018, a relation \(A \sqsubseteq B\) between types should induce an ep-pair : A pair of an upcast \({\uparrow {} : A {\rightarrow } B}\) and a downcast \({\downarrow {} : B {\rightarrow } A}\) satisfying a handful of properties with gradual guarantees as a corollary.

Note, that here equiprecision of the retraction becomes an equality because of antisymmetry. Under these conditions, \(\uparrow _d : A \hookrightarrow B\) is injective, \(\downarrow _d : B \twoheadrightarrow A\) is surjective and both preserve bottom elements, explaining that we call \(d : A \vartriangleleft {} B\) an embedding-projection pair. The definition of ep-pair s is based on a relation rather than just its pair of representing functions to highlight the connection between ep-pair s and parametricity New et al. 2020. Assuming function extensionality, being an ep-pair is a property of the underlying relation: There is at most one pair \((\uparrow {}_d, \downarrow _d)\) representing the underlying relation of \(d\) . An ep-pair straightforwardly induces the following relations that will be used in later proofs.

Posetal families. By monotonicity, a family \(B : A \rightarrow \square ^\le\) over a poset \(A\) gives rise not only to a poset \(B\,a\) for each \(a \in A\) , but also to ep-pair s \(B_{a,a^{\prime }} : B\,a \vartriangleleft {} B\,a^{\prime }\) for each \(a \sqsubseteq ^A a^{\prime }\) . These ep-pair s need to satisfy functoriality conditions:In particular, this ensures that heterogeneous transitivity is well defined:

Dependent products. Given a poset \(A\) and a posetal family \(B\) over \(A\) , we can form the poset \({\rm \Pi }^{\text{mon}}{}\,A\,B\) of monotone dependent functions from \(A\) to \(B\) , equipped with the pointwise order. Its inhabitants are dependent functions \(f : {\rm \Pi }(a : A). B\,a\) such that \(a \sqsubseteq ^A a^{\prime } {\Rightarrow } B_{a,a^{\prime }}\,(f\,a, f\,a^{\prime })\) . Moreover, given ep-pair s \(d_A : A \vartriangleleft {} A^{\prime }\) and \(d_B : B \vartriangleleft {} B^{\prime }\) , we can build an induced ep-pair \(d_\Pi : {\rm \Pi }^{\text{mon}}{}\,A\,B \vartriangleleft {} {\rm \Pi }^{\text{mon}}{}\,A^{\prime }\,B^{\prime }\) with underlying relationThe general case where \(B\) and \(B^{\prime }\) actually depend on \(A, A^{\prime }\) is obtained with similar formulas, but a larger amount of data is required to handle the dependency: we refer to the accompanying Agda development for details.

Inductive types. Generalizing the case of natural numbers, the order on an arbitrary extended inductive type \(\ddot{I}\) uses the following scheme:

The precondition on subterms in the third case is unnecessary in simple cases and is kept to be uniform with definition of order on the monotone unknown type in the following section.

Similarly to dependent product, an ep-pair \(\mathbf {X} \vartriangleleft {} \mathbf {X^{\prime }}\) between the parameters of an extended inductive type \(\ddot{I}\) induces an ep-pair \(\ddot{I}\,\mathbf {X} \vartriangleleft {} \ddot{I}\,\mathbf {X^{\prime }}\) . For instance, ep-pair s \(d_A : A \vartriangleleft {} A^{\prime }\) and \(d_B : B \vartriangleleft {} B^{\prime }\) induce an ep-pair \(d_{{\ddot{\Sigma }}} : {\ddot{\Sigma }}\,A\,B \vartriangleleft {} {\ddot{\Sigma }}\,A^{\prime }\,B^{\prime }\) defined by \(d_{{\ddot{\Sigma }}}((a,b),(a^{\prime },b^{\prime })) := d_A(a,a^{\prime }) \wedge d_B(b,b^{\prime })\) .

The interpretation \(\ddot{?}_{i}\) of the unknown type in the monotone model should morally group together approximations of every type at the same universe level. Working in (bi)pointed orders, \(\ddot{?}_{i}\) can be realized as a coalesced sum Abramsky and Jung 1995Section 3.2.3 of the family \({\rm germ}_{i}\,h\) indexed by head constructors \(h \in {\rm Head}_i\) . A concrete presentation of \(\ddot{?}_{i}\) is obtained as the quotient of \({\ddot{\Sigma }}\, {\rm Head}_i \, {\rm germ}_{i}\,\) identifying \(\bot _{{\ddot{\Sigma }}\, {\rm Head}_i \, {\rm germ}_{i}\,}\) with any pair \(({h};{{\rm \mathtt {err}}_{\widehat{{\rm germ}}_{i}\,h}})\) . The equivalence classes of \(({h};{x})\) is noted as \([{h};{x}]\) , \(\bot _{{\ddot{\Sigma }}\, {\rm Head}_i \, {\rm germ}_{i}\,}\) as \(\bot _{\ddot{?}_{i}}\) and \(\top _{{\ddot{\Sigma }}\, {\rm Head}_i \, {\rm germ}_{i}\,}\) as \(\top _{\ddot{?}_{i}}\) . The obtained type \(\ddot{?}_{i}\) is then equipped with a precision relation defined by the rules:These rules ensure that the exceptions \(\bot _{\ddot{?}_{i}}\) and \(\top _{\ddot{?}_{i}}\) are respectively the smallest and biggest elements of \(\ddot{?}_{i}\) . Non-exceptional elements are comparable only if they have the same head constructor \(h\) and if so are compared according to the interpretation of that head constructor as an ordered type \({\rm germ}_{i}\,h\) . Because of the quotient, it is not immediate that this presentation of \(\sqsubseteq ^{\ddot{?}_{i}}\) is independent of the choice of representatives in equivalence classes and that it forms a proof-irrelevant relation. In the formal development, we define the relation by quotient-induction on each argument, thus verifying that it respects the quotient, and also show that it is irrelevant. This relies crucially on equality being decidable on head constructors when comparing \([{h};{x}]\) and \([{h^{\prime }};{x^{\prime }}]\) .

In order to globally satisfy \(\mathcal {G}\) , \(\ddot{?}_{i}\) should admit an ep-pair \({d_h : {\rm germ}_{i}\,h \vartriangleleft {} \ddot{?}_{i}}\) whenever we have a head constructor \(h \in {\rm Head}_i\) such that \(\widehat{{\rm germ}}_{i}\,h \sqsubseteq \widehat{?}_{i}\) (we return to that point in the next Section 6.4). Embedding an element \(x \in {\rm germ}_{i}\,h\) by \(\uparrow _{d_h}x = [{h};{x}]\) and projecting out of \({\rm germ}_{i}\,h\) by the following equations form a reasonable candidate:Note that we rely again on \({\rm Head}\) having decidable equality to compute the \(\downarrow {}_{d_h}\) . Moreover, \(\uparrow _{d_h} \dashv \downarrow _{d_h}\) should be adjoints; in particular, the following precision relation needs to hold:Since \(\sqsubseteq ^{\ddot{?}_{i}}\) should be antisymmetric, this is possible only if \([{h};{{\rm \mathtt {err}}_{{\rm germ}_{i}\,h}}]\) and \(\bot _{\ddot{?}_{i}}\) are identified in \(\ddot{?}_{i}\) , explaining why we have to quotient in the first place.

Following the discrete model, the monotone universe hierarchy is also implemented through an inductive-recursive datatype of codes \(\square \!\!\!\! \square _i\) together with a decoding function \(\mathrm{El}: \square \!\!\!\! \square _i \rightarrow \square\) , both presented in Figure 17. The precision relation \({\sqsubseteq } : \square \!\!\!\! \square _i \rightarrow \square \!\!\!\! \square _j \rightarrow \square\) presented below is an order (Theorem 28) on this universe hierarchy. The “diagonal” inference rules, providing evidence for relating type constructors from \(\mathsf {CIC}\) , coincide with those of binary parametricity Bernardy et al. 2012. Outside the diagonal, \(\widehat{{\rm \mathtt {err}}_{}}\) is placed at the bottom. More interestingly, the derivation of a precision proof \(A \sqsubseteq \widehat{?}_{}\) provides a unique decomposition of \(A\) through iterated germs directed by the relevant head constructors. For instance, in the gradual systems \(\mathsf {CastCIC} ^{\mathcal {G}}\) and \(\mathsf {CastCIC} ^{\uparrow }\) where the equation \(c_\Pi (s_\Pi (i,j)) = \max (i,j)\) holds for any universe levels \(i,j\) , the derivation of \((\widehat{\mathbb {N}}{} {\rightarrow } \widehat{\mathbb {N}}{}) {\rightarrow } \widehat{\mathbb {N}}{} \sqsubseteq \widehat{?}_{}\) canonically decomposes as

This unique decomposition is at the heart of the reduction of the cast operator given in Figure 5, and it can be described informally as taking the path of maximal length between two related types.²⁰ Such a derivation of precision \(A \sqsubseteq B\) gives rise through decoding to ep-pair s \(\mathrm{El}{}_\varepsilon \,(A {\sqsubseteq }B) : \mathrm{El}\,A \vartriangleleft {}\mathrm{El}\,B\) , with underlying relation noted \({ [_{A}]{\sqsubseteq }{_{B}}} : \mathrm{El}\,A \rightarrow \mathrm{El}\,B \rightarrow \square\) . This decoding function \(\mathrm{El}{}_\varepsilon\) is described on generators of \(\sqsubseteq\) at the bottom of Figure 17. \(\mathrm{El}{}_\varepsilon (\widehat{{\rm \mathtt {err}}_{}}\text{-}{\sqsubseteq })\) states that the unique value \(\mathtt {()}\) of \(\mathrm{El}\,\widehat{{\rm \mathtt {err}}_{}}= \mathtt {unit}\) is smaller than any other value. The diagonal cases \(\mathrm{El}{}_\varepsilon (\widehat{\mathbb {N}}\text{-}{\sqsubseteq })\) and \(\mathrm{El}{}_\varepsilon (\widehat{\square \!\!\!\! \square }\text{-}\sqsubseteq)\) reuse the order specified on the carrier. The ep-pair \(\mathrm{El}{}_\varepsilon (\widehat{?}_{}\text{-}{\sqsubseteq })\) between two unknown types \(\ddot{?}_{i} \vartriangleleft {} \ddot{?}_{j}\) at potentially distinct universe levels \(i \le j\) stipulate that \({\rm \mathtt {err}}_{\widehat{?}_{i}}\) and \(?_{\widehat{?}_{j}}\) are respectively smaller and greater than any other value, and that the comparison between two injected terms with same head is induced by their second component. Note that these rules are redundant since \(\ddot{?}_{}\) is obtained through a quotient. Functions \(f,f^{\prime }\) are related by \(\mathrm{El}{}_\varepsilon (\widehat{\Pi }\text{-}{\sqsubseteq })\) when they map related elements \(a [_{A}]{\sqsubseteq }{_{A^{\prime }}} a^{\prime }\) to related elements \(f\,a [_{B\,a}]{\sqsubseteq }{_{B^{\prime }\,a^{\prime }}}f^{\prime }\,a^{\prime }\) . Finally, \(\mathrm{El}{}_\varepsilon ({\rm Head}\text{-}{\sqsubseteq })\) embeds a type \(A\) into \(\ddot{?}_{}\) through its \(\mathrm{head}\,\) .

It is interesting to observe what happens in \(\mathsf {CastCIC} ^{\mathcal {N}}\) , where \(c_\Pi (s_\Pi (i,j)) \ne \max (i,j)\) , for instance on the previous example:So \(\widehat{\mathbb {N}}{} {\rightarrow } \widehat{\mathbb {N}}{}\) is not lower than \(\widehat{?}_{}\) in that setting.

One crucial point of the monotone model is the mutual definition of codes \(\square \!\!\!\! \square _i\) together with the precision relation, particularly salient on codes for \(\Pi\) -types: in \(\widehat{\Pi }\,A\,B\) , \(B : \mathrm{El}\,A \rightarrow \square \!\!\!\! \square _i\) is a monotone function with respect to the order on \(\mathrm{El}\,A\) and the precision on \(\square \!\!\!\! \square _i\) . This intertwining happens because the order is required to be reflexive, a fact observed previously by Atkey et al. 2014 in the similar setting of reflexive graphs. Indeed, a dependent function \(f : \Pi (a : \mathrm{El}\,A).\, \mathrm{El}\,(B\,a)\) is related to itself \(f [_{\widehat{\Pi }{}\,A\,B}]{\sqsubseteq }{_{\widehat{\Pi }{}\,A\,B}} f\) if and only if \(f\) is monotone.

The monotone translation \(\lbrace {{-}}\rbrace _{}\) presented in Figure 18 brings together the monotone interpretation of inductive types (e.g., \(\ddot{\mathbb {N}}\) ), dependent products, the unknown type \(\ddot{?}_{}\) as well as the universe hierarchy. Following the approach of New and Ahmed 2018, casts are derived out of the canonical decomposition through the unknown type using the property \((2)\) from Theorem 28:Note that this definition formally depends on a chosen universe level \(j\) for \(\widehat{?}_{}: \square \!\!\!\! \square _{j}\) , but the resulting operation is independent of this choice thanks to the section-retraction properties of ep-pair s . The difficult part of the model, the monotonicity of \({\rm \mathtt {cast}}\) , thus holds by design. However, the translation of some terms do not reduce as in \(\mathsf {CastCIC}\) : \({\rm \mathtt {cast}}\) can get stuck on type variables eagerly, e.g., on a Down-Err step.²² These reduction rules still hold propositionally though so that we have at least a model in an extensional variant of the target theory (i.e., in which two terms are definitionally equal whenever they are propositionally so).

We can further enhance this result using the fact that we assume functional extensionality in our target and can prove that the translation of all our types satisfy UIP. Under these assumptions, the conservativity results of Hofmann 1995 and Winterhalter et al. 2019 apply, so we can recover a translation targeting \(\mathsf {CIC^{IR}_{QIT}}\) .

It is unlikely that the principle that we demand in the target calculus \(\mathsf {CIC^{IR}_{QIT}}\) are optimal. We conjecture that a variation of the translation described here could be developed in \(\mathsf {CIC}\) extended only with induction-induction to describe the intensional content of the codes \(\square \!\!\!\! \square\) in the universe, and strict propositions Gilbert et al. 2019 following the construction of the setoid models of type theory Altenkirch 1999 Altenkirch et al. 2019 2021.

The precision order equipping each types of the monotone model can be reflected back to \(\mathsf {CastCIC}\) , giving rise to the propositional precision judgment:By the properties of the monotone model (Theorem 28), there is at most one witness up to propositional equality in the target that this judgment holds. This precision relation bears a similar relationship to the structural precision \(\sqsubseteq _{\alpha }\) as propositional equality with definitional equality in \(\mathsf {CIC}\) . On the one hand, propositional precision can be used to prove precision statements inside the target type theory, for instance we can show by a straightforward case analysis on \({b} : {\mathbb {B}}\) that \({b} : {\mathbb {B}} \vdash _{{\rm \mathtt {cast}}}{\texttt {if } b \texttt { then } A \texttt { else } A} [_{{\square }}]{\sqsubseteq }{_{{\square }}} {A}\) , a judgment that does not hold for syntactic precision. In particular, propositional precision is compatible with propositional equality, and a fortiori it is invariant by conversion in \(\mathsf {CastCIC}\) : if \({t} \equiv {t^{\prime }}\) , \({u} \equiv {u^{\prime }}\) and \({\Gamma } \vdash _{{\rm \mathtt {cast}}}{t} [_{{T}}]{\sqsubseteq }{_{{U}}} {u}\) then \({\Gamma } \vdash _{{\rm \mathtt {cast}}}{t^{\prime }} [_{{T}}]{\sqsubseteq }{_{{U}}} {u^{\prime }}\) . On the other hand, propositional precision is not decidable, thus not suited for typechecking, where structural precision has to be used instead.

With a similar method, we show that \(\mathsf {CastCIC} ^{\uparrow }\) satisfies graduality, which is the key missing point of Section 5 and the raison d’etre of the monotone model.

We conjecture that the target \(\mathsf {CIC^{IR}_{QIT}}\) mentioned in the above theorem and propositions is consistent relative to a strong enough metatheory,²³ that is the assumed inductive-recursive definition for the universe does not endanger consistency. As can be seen from the proof, this hypothesis allows to move from a contradiction internal to \(\mathsf {CIC^{IR}_{QIT}}\) to a contradiction in the ambient metatheory.

To prove graduality of \(\mathsf {CastCIC} ^{\mathcal {G}}\) , we need to provide a model accounting for both monotony and non-termination. The monotone model presented in the previous sections, which gives us graduality for \(\mathsf {CastCIC} ^{\uparrow }\) and can be related to the pointed model of New and Licata 2020Section 6.1, only accounts for terminating functions. In order to capture also non-termination, we can adapt the Scott model of New and Licata 2020Section 6.2 based on pointed \(\omega\) -cpo to our setting. We now explain the construction of the main type formers, overloading the notations from the previous sections.

Types are interpreted as bipointed \(\omega\) -cpos, that is as orders \((A, \sqsubseteq)\) equipped with a smallest element \({\rm \mathtt {err}}_A \in A\) , a largest element \(?_A \in A\) and an operation \(\sup _{i}\,a_i\) computing the suprema of countable ascending chains, i.e., sequences \((a_i)_{i\in \omega } \in A^\omega\) indexed by the ordinal \(\omega = \lbrace 0 \lt 1 \lt \cdots \rbrace\) such that \(a_i \sqsubseteq ^A a_j\) whenever \(i \lt j\) . A monotone function \(f : A \rightarrow B\) between \(\omega\) -cpos is called \(\omega\) -continuous if for any ascending chain \((a_k)_{k\in \omega }\) , \(\sup _k f\,a_k = f (\sup _k a_k)\) ; we write \(d : A \vartriangleleft ^\omega {} B\) for an ep-pair between \(\omega\) -cpos where \(\uparrow _d\) preserves suprema (the left adjoint \(\downarrow _d\) automatically preserves suprema).

A type-theoretical construction of the free \(\omega\) -cpo on a set is described in Bidlingmaier et al. 2019 Chapman et al. 2019 using quotient-inductive-inductive types (QIIT) Altenkirch et al. 2018 Kaposi et al. 2019. We can adapt this technique to provide an interpretation for inductive types, and in particular natural numbers, throwing in freely a new constructor \(\sup\) denoting the suprema of any chain of elements and quotienting by the appropriate (in)equations: the suprema of a chain is greater than any of its parts \(a_i \sqsubseteq \sup \,a_i\) and an element \(b\) that is greater than a chain \(\forall i, a_i \sqsubseteq b\) is greater than its suprema \(\sup a_i \sqsubseteq b\) . Functions \(f : A \rightarrow B\) between types are interpreted as continuous monotone maps, and the type \(A \rightarrow ^\omega B\) of continuous monotone functions is an \(\omega\) -cpo with suprema computed pointwise. As in Section 6.3, the construction of the \(\omega\) -cpo corresponding to the unknown type is intertwined with the universe hierarchy. Assuming by induction that we have \(\omega\) -cpos \(\square \!\!\!\! \square _0, \ldots , \square \!\!\!\! \square _i\) for universes at level lower than \(i\) , we follow the seminal work of Scott 1976 on domains and we take the unknown type \(\ddot{?}_{i+1}\) to be a solution to the recursive equation:The key techniques to build a solution to this equation in the setting of \(\omega\) -cpos are detailed in Smyth and Plotkin 1977 Wand 1979. In a nutshell, this construction amounts to iterate the assignment \(F(X) := \ddot{\mathbb {N}}+ (X \rightarrow ^\omega X) + \square \!\!\!\! \square _0 + \cdots + \square \!\!\!\! \square _i\) starting from the initial bipointed \(\omega\) -cpo \(\ddot{\mathbb {0}}\) —the free bipointed \(\omega\) -cpo on an empty type, consisting just of \(\bot _{\ddot{\mathbb {0}}} \sqsubseteq \top _{\ddot{\mathbb {0}}}\) —and to take the colimit of the induced sequence:For this construction to succeed, \(F\) should extend to an \(\omega\) -continuous functor on the category of \(\omega\) -cpos and \(\omega\) -continuous ep-pair s that moreover preserves countable sequential colimits as above so that the following hold:The construction of \(\ddot{?}_{i+1}\) as a fixpoint for \(F\) should be contrasted with the construction from Section 6.3 where we essentially describe explicitly a construction of \(\ddot{?}_{i+1} := F(\ddot{?}_{i})\) in the setting of bipointed posets. The existence of countable sequential colimits in the category of \(\omega\) -cpos and ep-pair s, as employed in Equation (5), is an interesting fact proved in Wand 1979Theorem 3.1, which we also use to equip the next universe of codes \(\square \!\!\!\! \square _{i+1}\) with an \(\omega\) -cpo structure. In brief, we adapt the inductive description of the universe of codes \(\square \!\!\!\! \square _i\) given in Figure 17 with an additional code \(\sup \,(A_k)_{k \in \omega } : \square \!\!\!\! \square _i\) for suprema of chains of codes \(A_k : \square \!\!\!\! \square _i\) , and decode it with the function \(\mathrm{El}\) satisfying \(\mathrm{El}\,(\sup \,(A_k)_{k \in \omega }) \cong \mathrm{colim}_k\, (\mathrm{El}~A_k)\) . However, the isomorphism above cannot be used as a definition because the definition of \(\mathrm{El}\) has to respect the quotiented nature of \(\square \!\!\!\! \square _i\) . In particular, when the chain is the constant chain \((\widehat{\mathbb {N}})_{k \in \omega }\) , \(\sup \,(\widehat{\mathbb {N}})_{k \in \omega } = \widehat{\mathbb {N}}\) and thus \(\mathrm{El}\,(\sup \,(\widehat{\mathbb {N}})_{k \in \omega })\) must also be equal to \(\ddot{\mathbb {N}}\) , which is different from \(\mathrm{colim}_k\, \ddot{\mathbb {N}}\) . Technically, we define \(\mathrm{El}\,A\) as its isomorphic image onto \(\ddot{?}_{i}\) , recovering a canonical choice for the inhabitants of \(\mathrm{El}\,(\sup \,(A_k)_{k \in \omega })\) .

Note that in contrast with the construction from Section 6.3 that depended on \({\rm germ}_{i}\,\) and hence \(\mathrm{El}_{i}\) , the present construction of \(\ddot{?}_{i}\) does not depend on the construction of \(\square \!\!\!\! \square _{i}\) and \(\mathrm{El}_i\) , cutting the non-wellfounded loop observed in Section 6.1.

The components that we describe assemble as a model of \(\mathsf {CastCIC} ^{\mathcal {G}}\) into \(\mathsf {CIC^{IR}_{QIT}}\) . In order to be able to prove DGG for \(\mathsf {CastCIC} ^{\mathcal {G}}\) , we first need to characterize the semantic interpretation of diverging terms of type \(\mathbb {B}\) in the model.

Relativizing the notion of precision \({\Gamma } \vdash _{{\rm \mathtt {cast}}}{t} [_{{T}}]{\sqsubseteq }{_{{S}}} {u}\) of the monotone model to use the order induced by this \(\omega\) -cpo model instead of the monotone model, we can replay the steps of Theorem 32 and derive graduality for \(\mathsf {CastCIC} ^{\mathcal {G}}\) .

Indexed inductive types make it possible to define structures that are intrinsically characterized by some property, which holds by construction, as opposed to extrinsically establishing such properties after the fact. There are two well-known alternatives to indexed inductive types for capturing properties intrinsically: type-level fixpoints, and “forded” inductive types.

In \(\mathsf {CIC}\) , these two alternative presentations of an indexed inductive type can be shown internally to be equivalent. But each of these presentations has advantages and drawbacks depending on the considered system and scenarios of use, so practitioners have different preferences in that respect. More important to us here, these presentations are not equivalent in \(\mathsf {GCIC}\) .

Constructors. The definition of \(\mathsf{FVec}\) above can directly be written in \(\mathsf {GCIC}\) , as it uses only inductive types with parameters (here the unit and product types and natural numbers). The vector constructors can be defined as

whose definitions typecheck because \(\mathsf{FVec}\) computes on its indices.

Behavior. Let us now look at the type computed at \(?_\mathbb {N}\) . Because \(?_\mathbb {N}\) is an exceptional term, the fixpoint has to return unknown in the universe: \(\mathsf{FVec A ?_nat ==* ?_Type}\) . This means that the mechanism for casting a vector into a vector with the unknown index is directly inherited from the generic mechanism for casting to the unknown type. Therefore, we get for free the following computation rules, because they involve embedding-projection pairs:

Similarly, the eliminator \(\mathsf{FVec_rect}\) can be defined by first matching on the index, and then on the vector and satisfies the computation rule of vectors when the index is non-exceptional. The only drawback of this encoding is that the behavior of the eliminator is not satisfactory when the index is unknown. Consider for instance the following term from Example 1, which unfortunately reduces to \(\mathsf{?_nat}\) :

This behavior occurs because the eliminator starts by matching on the index, which is unknown, and thus has to return the unknown itself.

Constructors. With the definition of the forded inductive type \(\mathsf{vec_eqdec}\) , the \(\mathsf{nil_eqdec}\) constructor can legitimately be used to inhabit \(\mathsf{vec_eqdec A ?_nat}\) , provided we have an inhabitant (possibly ?) of \(\mathsf{eq_nat 0 n}\) .

Note that we can provide the same vector interface as that of the indexed inductive type by defining the following constructor wrappers, using the term \(\mathsf{refl n}\) of reflexivity on \(\mathsf{eq_nat}\) :

and define the corresponding eliminator \(\mathsf{vec_rect^{\prime }}\) accordingly.

Behavior. The computational content of the eliminator on \(\mathsf{vec_eqdec A ?_nat}\) is more precise than with \(\mathsf{FVec}\) : the eliminator never matches on the proof of equality to produce a term, but only to guarantee that a branch is not accessible. Concretely, this means that we observe the expected reduction:

Again, the fact that upcasting to \(\mathsf{vec_eqdec A ?_nat}\) and then downcasting back is the identity relies on the \(\mathsf {CastCIC}\) mechanism on the unknown for the universe, but this time only for the type representing the decidable equality. Likewise, the example of \(\mathsf{filter}\) (Example 1) computes as expected:

On the other hand, an invalid assertion does not produce an error, but a term with an error in place of the equality proof:

where \(\mathsf{raise}\) is at type \(\mathsf{eq_nat 1 0}\) . Consequently, we have \(\mathsf{Dhead ?_nat (Dfilter nat 2 even [ 1 ; 3 ]) ==*}\) \(\mathsf{raise}\) , because the branch of \(\mathsf{Dhead}\) that deals with the \(\mathsf{nil}\) case matches on the (erroneous) equality proof. Invalid assertions are therefore very lazily observed, if at all, which is not satisfactory.

Finally, there is a drawback of using decidable equalities, which only manifests when working with the original vector interface ( \(\mathsf{nil^{\prime }}\) / \(\mathsf{cons^{\prime }}\) / \(\mathsf{vec_rect^{\prime }}\) ). In that case, the eliminator does not enjoy the expected computational rule on the constructor \(\mathsf{cons^{\prime }}\) . Because the eliminator is defined by induction on natural numbers, therefore it only reduces when the index is a concrete natural number, not a variable.

Extending \(\mathsf {GCIC}\) / \(\mathsf {CastCIC}\) with direct support for indexed inductive types can provide a fully satisfactory solution, in contrast to the two previously-exposed encodings that both have serious shortcomings. The idea is to reason about indices directly in the reduction of casts. Here, we expose this approach for the specific case of length-indexed vectors and leave a generalization to future work. Appendix E describes the extension for vectors in full details; here, we only present selected rules (Figure 19) and illustrate how reduction works.

Constructors. We add two new canonical forms, corresponding to the casts of \(\mathsf{nil}\) and \(\mathsf{cons}\) to \(\mathtt {vec}~A~?_{\mathbb {N}}\) : namely, \(\mathtt {nil}_?~A\) and \(\mathtt {cons}_?~A~a~n~v\) (Figure 19). Note that we cannot simply declare casts such as \(\langle {\mathtt {vec}~A~?_{\mathbb {N}}} {\ \Leftarrow \ } {\mathtt {vec}~A~n} \rangle \,{t}\) to be canonical, because they involve non-linear occurrences of types (here, \(A\) ).

Reduction rules. We add reduction rules to conduct casts between vectors in canonical forms. Figure 19 presents these rules when the argument of the cast is a \(\mathsf{cons}\) . Rule V-cons-? propagates the cast on the arguments, but using the newly-introduced \(\mathtt {cons}_?\) , effectively converting precise information to less precise information. Rule V-cons applies when both source and target indices are successors, and propagates the cast of the arguments, just like the standard rule for casting a constructor. As expected, Rule V-cons-nil raises an error when the indices do not match.

For the eliminator, there are two new computation rules, one for each new constructor: v-rectnilu and v-rect-consu. They both apply the eliminator to the underlying non-exceptional constructor, and then cast the result back to \(P~?_\mathbb {N}\) . Intuitively, these rules transfer the cast on vectors to a cast on the returned type of the predicate.

Behavior. Given these rules, we can actually realize the behavior described in Example 1. For instance, we have both

and coming back to Example 1, in all three \(\mathsf {GCIC}\) variants the term:

typechecks and reduces to \(\mathsf{0}\) . Additionally, as expected:

typechecks and fails at runtime. And similarly for Example 4.

Note that to be able to define the action of casts on vectors, we have crucially used the fact that it is possible to discriminate between \(\mathsf{0}\) , \(\mathsf{S n}\) , and \(?_\mathbb {N}\) in the reduction rule.

To summarize, the different approaches to define structures with intrinsic properties in \(\mathsf {GCIC}\) compare as follows:

Recall that fording is only an option in \(\mathsf {GCIC}\) when the indices pertain to a type with decidable equality; properly handling general propositional equality in a gradual type theory is an open question (Section 8.3). The constraint of indices being concretely forceable (for type-level fixpoints, direct support) are intuitively understandable and expected: gradual typing requires synthesizing dynamic checks; therefore, these checks need to be somehow computable.

In this work, we do not deal with the impredicative sort Prop, for multiple reasons. The models used in Section 6 to justify termination and graduality crucially rely on the predicativity of the universe hierarchy for the inductive-recursive definition of codes to be well-founded. Moreover, the results of Palmgren 1998Theorem 6.1 show that it is not possible to endow an impredicative universe with an inductive-recursive structure in a consistent and strongly-normalizing theory, hinting that it may be difficult to devise an inductively-defined cast function between types that belong to an impredicative universe. Additionally, it seems difficult to avoid the divergence of \(\Omega\) with an impredicative sort, as no universe levels can be used to prevent a self-application from being well-typed.

In most presentations of \(\mathsf {CIC}\) , and, in particular, its \(\mathrm{Coq}\) implementation, conversion satisfies an additional rule, called \(\eta\) -equality, which corresponds to an extensional property for functions:The difficulty of integrating \(\eta\) -equality in the setting of \(\mathsf {GCIC}\) is that the conversion we consider in \(\mathsf {CastCIC}\) is entirely induced by a notion of reduction: Two terms are convertible exactly when they have a common reduct up to \(\alpha\) -equivalence. It is well-known that \(\eta\) -equality cannot be easily modeled using a rewrite rule, as both \(\eta\) -expansion and \(\eta\) -reduction have significant drawbacks Goguen 2005, and so we would have to consider another approach to the one we took if we were to integrate \(\eta\) -equality. The most prominent alternative way is to define conversion as an alternation of reduction steps (for instance using a weak-head reduction strategy) not containing \(\eta\) and comparison of terms up to congruence and \(\eta\) -equality.

This approach has been recently formalized by Abel et al. 2018 in a fully-typed setting. That is, types participate crucially in the conversion relation: They are maintained during conversion, so that for instance comparison of terms at a \(\Pi\) -type systematically \(\eta\) -expands them before recursively calling conversion at the domain types. Defining a gradual variant of such a typed conversion might be quite interesting, but would require a significant amount of work.

On the contrary, a precise, formalized, account is still missing for \(\eta\) -equality for an untyped conversion as used in practice in the \(\mathrm{Coq}\) proof assistant and in \(\mathsf {GCIC}\) . The MetaCoq project, which aims at such a formalized account, leaves the treatment of \(\eta\) -equality to future work Sozeau et al. 2020. While we envision no specific issues to the adaptation to this approach to gradual typing once a clear and precise solution for \(\mathsf {CIC}\) itself has been reached, solving the issue in a satisfactory way for \(\mathsf {CIC}\) is obviously out of scope for this article. Thus, while it should in principle be possible to add \(\eta\) -equality to \(\mathsf {GCIC}\) , either via typed or untyped conversion, we leave this for future work.

In \(\mathsf {CIC}\) , propositional equality \(\mathsf{eq A x y}\) , corresponds to the Martin-Löf identity type Martin-Löf 1975, with a single constructor \(\mathsf{refl}\) for reflexivity, and the elimination principle known as \(\mathsf{J}\)

together with the conversion rule:

For the sake of exposing the problem, suppose that we can define this identity type in \(\mathsf {GCIC}\) , while still satisfying canonicity, conservativity with respect to \(\mathsf {CIC}\) and graduality. This means that for an equality \(\mathsf{t = u}\) involving closed terms \(\mathsf{t}\) and \(\mathsf{u}\) of \(\mathsf {CIC}\) , there should only be three possible canonical forms: \(\mathsf{refl A t}\) whenever \(\mathsf{t}\) and \(\mathsf{u}\) are convertible terms (of type \(\mathsf{A}\) ), as well as \(\mathsf{raise}\) and \(\mathsf{?}\) .

Just under these assumptions, we can show that there exist two functions that are pointwise equal in \(\mathsf {CIC}\) , and hence equal by extensionality, but are no longer equivalent in \(\mathsf {GCIC}\) / \(\mathsf {CastCIC}\) . Consider the two functions \(\mathsf{id_nat}\) and \(\mathsf{add0}\) below:

In \(\mathsf {CIC}\) , these functions are not convertible, but they are observationally equivalent. However, they would not be observationally equivalent in \(\mathsf {GCIC}\) . To see why, consider the following term:

We have \(\mathsf{test id_nat ==* true}\) because, by \(\mathcal {G}\) , \(\mathsf{refl id_nat::?_Type::id_nat = id_nat ==* refl id_nat}\) . However, because \(\mathsf{add0}\) is not convertible to \(\mathsf{id_nat}\) , \(\mathsf{refl id_nat::id_nat = add0}\) cannot possibly reduce to \(\mathsf{refl}\) , and thus would need to reduce either to \({\rm \mathtt {err}}\) or ?; and so does \(\mathsf{test add0}\) .

This means that a model for such a gradual type theory would need to be intensional, conversely to the extensional models usually used to justify type theories. Studying such a model as well as exploring alternatives approaches to propositional equality in a gradual type theory are interesting venues for future work.

We state and prove a handful of standard, technical properties of \(\mathsf {CastCIC}\) , that are useful in the next sections. They should not be very surprising, the main specific point here is their formulation in the bidirectional setting.

Structural lemmas. Let us start our lemmas by counterparts to the weakening and substitution lemmas for precision.

Catch-up lemmas. With these structural lemmas at hand, let us turn to the proofs of the catch-up lemmas.

Simulation.