# Gradual Indexed Inductive Types

Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter

► To cite this version:

Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter. Gradual Indexed Inductive Types. Proceedings of the ACM on Programming Languages, 2024, 8 (ICFP), pp.544-572. 10.1145/3674644 . hal-04681546

HAL Id: hal-04681546

https://inria.hal.science/hal-04681546v1

Submitted on 26 May 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

# Gradual Indexed Inductive Types

MARA MALEWSKI, University of Chile, Chile

KENJI MAILLARD, Inria, France

NICOLAS TABAREAU, Inria, France

ÉRIC TANTER, University of Chile, Chile

Indexed inductive types are essential in dependently-typed programming languages, enabling precise and expressive specifications of data structures and properties. Recognizing that programming and proving with dependent types could benefit from the smooth integration of static and dynamic checking that gradual typing offers, recent efforts have studied gradual dependent types. Gradualizing indexed inductive types however remains mostly unexplored: the standard encodings of indexed inductive types in intensional type theory, e.g., using type-level fixpoints or subset types, break in the presence of gradual features; and previous work on gradual dependent types focus on very specific instances of indexed inductive types.

This paper contributes a general framework, named PUNK, specifically designed for exploring the design space of gradual indexed inductive types. PUNK is a versatile framework, enabling the exploration of the space between eager and lazy cast reduction semantics that arise from the interaction between casts and the inductive eliminator, allowing them to coexist and interoperate in a single system.

Our work provides significant insights into the intersection of dependent types and gradual typing, by proposing a criteria for well-behaved gradual indexed inductive types, systematically addressing the outlined challenges of integrating these types. The contributions of this paper are a step forward in the quest for making gradual theorem proving and gradual dependently-typed programming a reality.

**CCS Concepts:** • **Theory of computation** → **Type theory; Type structures.**

**Additional Key Words and Phrases:** Gradual typing, proof assistants, dependent types

## ACM Reference Format:

Mara Malewski, Kenji Maillard, Nicolas Tabareau, and Éric Tanter. 2024. Gradual Indexed Inductive Types. *Proc. ACM Program. Lang.* 8, ICFP, Article 255 (August 2024), 29 pages. https://doi.org/10.1145/3674644

## 1 Introduction

Indexed inductive types play a pivotal role in dependently-typed programming languages due to their versatility in expressing complex data structures and logical properties [Chlipala 2013; Pierce et al. 2015] and are therefore a predominant feature of languages such as Idris [Brady 2013] and proof assistants such as Coq [The Coq Development Team 2020], Lean [de Moura et al. 2015], and Agda [Norell 2007]. These types extend the capabilities of traditional inductive types by allowing constructor types to depend on terms, enabling precise and expressive specifications of data and program behavior. Some canonical examples of indexed inductive types include bounded natural numbers, length-indexed lists (called vectors), heterogeneous lists, Martin-Löf's propositional

Authors' Contact Information: Mara Malewski, University of Chile, PLEIAD Lab, Computer Science Department (DCC), Santiago, Chile, smalewsk@dcc.uchile.cl; Kenji Maillard, Inria, Gallinette Project-Team, Nantes, France, kenji.maillard@inria.fr; Nicolas Tabareau, Inria, Gallinette Project-Team, Nantes, France, nicolas.tabareau@inria.fr; Éric Tanter, University of Chile, PLEIAD Lab, Computer Science Department (DCC), Santiago, Chile, etanter@dcc.uchile.cl.

<figure><img src="image_3.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

© 2024 Copyright held by the owner/author(s).

ACM 2475-1421/2024/8-ART255

https://doi.org/10.1145/3674644

<footnote>*This work is partially funded by ANID/Doctorado Nacional/2021-21210982 and Inria Équipe Associée GRAPA.</footnote>
equality [Martin-Löf 1971], and lambda calculus terms indexed over names in scope. This expressive power makes dependently-typed languages invaluable not only for theorem proving but also for general-purpose programming: programmers can leverage indexed inductive types to encode intricate invariants and constraints within the type system, leading to safer and more reliable code. As programming languages, dependently-typed languages empower developers to write certified software by either including correctness proofs along the code (extrinsic style) or by extending data structures with invariants and using the type system to enforce correctness (intrinsic style); the latter approach uses indexed inductive types extensively.

While dependently-typed languages offer immense power, they are often quite challenging to use. The intricate type system and the need to express program properties at the type level creates a steep learning curve for both developers entering the realm of formal verification and mathematicians looking to mechanize their work.

Gradual typing is a discipline that provides flexibility by enabling the smooth transition between statically and dynamically typed code and vice versa [Siek and Taha 2006]. Code can be made more dynamic by using imprecise types, i.e., the unknown type ? or types with unknown components, such as ? → N. Conversely, code can be made more static by replacing occurrences of the unknown type with static types. Imprecision is checked optimistically by the typechecker, and type safety is ensured by inserting runtime checks—usually called casts—to detect any type error that may arise during execution. The smooth transition provided by gradual typing is captured by a couple of properties called the *gradual guarantees*, which state that typing and reduction are monotone with respect to precision [Siek et al. 2015b]. Gradual typing has been successfully applied to a wide range of type systems and programming language features. The impact of gradual typing is not limited to academia, as its ideas are being adopted by various mainstream programming languages, such as TypeScript, Flow, and Racket, among others.

There have been several attempts to integrate some degree of dynamic typing into dependently-typed languages [Dagand et al. 2018; Ou et al. 2004; Tanter and Tabareau 2015]. One remarkable effort to bring gradual typing to dependently-typed languages is the gradual dependently-typed language GDTL [Eremondi et al. 2019]. GDTL uses the Abstracting Gradual Typing methodology [Garcia et al. 2016] to gradualize the predicative variant of the calculus of constructions (CC<sub>ω</sub>) with call-by-value semantics. GDTL has two distinct phases, a compile-time phase that optimistically approximates type checking (*approximate normalization*) and a runtime phase that, while being exact, may fail or diverge. Since GDTL allows for non-termination it is more suited for dependently-typed programming than for theorem proving.

Another notable effort is the Gradual Calculus of Inductive Constructions (GCIC) [Lennon-Bertrand et al. 2022]. GCIC brings gradual typing to a restricted version of Calculus of Inductive Constructions (CIC) that supports parametrized inductive types, not indexed inductive types in general. Lennon-Bertrand et al. [2022] have established that it is impossible for any gradual language to achieve a conservative extension of CIC, strong normalization, and graduality simultaneously. Graduality [New and Ahmed 2018], in this context, refers to a semantic formulation of the dynamic gradual guarantee where losing and then recovering precision yields an equivalent term. GCIC comes in three different variants, each one dropping one of these properties while maintaining the other two: GCIC<sup>N</sup> drops graduality, GCIC<sup>G</sup> drops strong normalization, and GCIC<sup>↑</sup> drops the conservative extension with respect to CIC.

GCIC has been recently extended in two separate directions. On the one hand, Eremondi et al. [2022] extend GCIC<sup>G</sup> with support for propositional equality. Like GDTL, their intention is to make a gradual dependently-typed language rather than a gradual theorem prover, hence they choose to sacrifice strong normalization. On the other hand, GRIP [Maillard et al. 2022] explores
the space of gradual theorem proving by extending GCICN with an internalized notion of precision. GRIP features two universe hierarchies, one for gradual types and terms, whose reduction can raise an exception (either error or the unknown term), and another for pure (non-gradual) strict propositions [Gilbert et al. 2019]. Since the internalized notion of precision lives in the propositional universe, it is possible to reason in a logically consistent way about gradual programs. Although graduality does not hold universally in GRIP, the authors identify a subset of the language, called the monotone fragment, for which graduality holds and can be internally established. Outside of the monotone fragment are the Π types that produce terms of a universe and, more relevant to this work, the catch operator that serves as the eliminator of inductive types in an exceptional type theory [Pédrot and Tabareau 2018].

Despite the many advances in gradual type theories summarized above, none of these theories supports gradual indexed inductive types in general. In the gradual setting, handling indexed inductive types presents distinct challenges. On the one hand, traditional methods for encoding these types, such as type-level fixpoints and subset types, do not behave as expected when interacting with the unknown type and casts. On the other hand, direct approaches have either focused in a specific indexed inductive type [Eremondi et al. 2022] or ad-hoc mechanisms restricted to indices with decidable equality [Lennon-Bertrand et al. 2022]. This lack of support is a serious limitation considering the importance of indexed inductive types in all kinds of development with proof assistants such as Coq, Lean and Agda. This work tackles this challenge by extending GRIP with a general notion of gradual indexed inductive types. Interestingly, we observe that there is no unique or generally better way to deal with casts on indices at runtime: there are just different possible semantics for cast reduction, with different tradeoffs, just like there are different possible semantics for higher-order casts in standard gradually-typed languages [Siek et al. 2009].

Among the many behaviors one may consider for multiple consecutive casts, we concentrate on three options in this paper: free, meet, and forgetful. These approaches correspond to cast reduction semantics already studied in the gradual typing literature [Greenberg 2017; Siek and Wadler 2010] and exhibit different behaviors with respect to the interaction of cast sequences and elimination. First, the simplest option is to account for every possible cast in the sequence; we call this the *free* (F) cast reduction semantics. In particular this means that casts on constructors do not reduce and simply accumulate. Second, one can choose to accumulate intermediate casts using a special construct called a *meeting* (M) to store the accumulated meet (i.e., greatest lower bound with respect to precision) of the indices of the targets of the casts.<fnref n="1" /> This technique has the advantage of ensuring cast space efficiency, as any cast sequence is represented in a single meeting, faithfully respecting every cast in the original sequence. A third option, which is also space efficient, is to drop intermediate casts and just keep the outermost one. This semantics is called *forgetful* (U) [Greenberg 2017] because it forgets (possibly invalid) intermediate casts. Here is an example of the expected cast reduction rules for the three semantics, where the empty vector nil of type $V A 0$ is first cast to $V A 1$ and then to its original type:

$$ \begin{align*} \langle V A 0 \leftarrow V A 1 \leftarrow V A 0 \rangle \text{nil} &\stackrel{\sim}{\rightarrow} \text{(normal form)} \qquad (F) \\ \langle V A 0 \leftarrow V A \text{ err}_N \leftarrow V A 0 \rangle \text{nil} &\stackrel{\sim}{\rightarrow} \langle V A 0 \leftarrow V A \text{ err}_N \rangle \text{nil} \qquad (M) \\ \langle V A 0 \leftarrow V A 0 \rangle \text{nil} &\stackrel{\sim}{\rightarrow} \text{(free)} \qquad (U) \end{align*} $$

We observe that these cast reduction semantics can be characterized in terms of *precision* (⊑) through the interaction of the eliminator (called catch) and casts. This difference in behavior divides the space of possible semantics for indexed inductive types into three distinct classes depending on

<footnote n="1">¹This construct was previously known in the literature as a *thirstsome* [Siek and Wadler 2010]. In cooperation with the original authors, we choose to rebrand to avoid the double entendre. The new name *meeting* was suggested by Phil Wadler.</footnote>
which property they satisfy. Inductive types satisfy *equiprecise elimination* when they commute perfectly (i.e., moving casts in and out of catch does not affect precision), *overprecise elimination* when they gain precision when moving casts to the outside of the catch, and *underprecise elimination* when they lose precision by doing so. For instance, the forgetful semantics exhibits an overprecise eliminator: casting a constructor before eliminating it may fail less than casting after eliminating. For example, let us consider a function $f: \Pi(A: \Box)(n:N), \forall A n \rightarrow \text{if (is\_err } n\text{) then err\_err\_\Box \text{ else N}}$ on forgetful vectors that returns $err_{err\_\Box}$ when the index $n$ is $err_N$ and 0 otherwise. Because forgetful inductives drop intermediate casts, casting nil before applying it to $f$ is less precise than casting after its application instead. In the following example, the cast through $\forall A err_N$ is ignored and the reduction proceeds successfully:

$$ 
\begin{aligned}
f(\langle \forall A 0 \equiv \forall A err_N \equiv \forall A 0 \rangle \text{nil}) &\rightarrow f(\langle \forall A 0 \equiv \forall A 0 \rangle \text{nil}) \rightarrow \langle N \equiv N \rangle (f \text{ nil}) \\
&\rightarrow \langle N \equiv N \rangle 0 \rightarrow 0
\end{aligned}
$$

However, when casting on the motive after applying $f$, the cast does go through $err\_\Box$ and fails:

$$ \langle N \equiv \text{err\_\Box} \equiv N \rangle (f \text{ nil}) \rightarrow \langle N \equiv \text{err\_\Box} \equiv N \rangle 0 \rightarrow \text{err}_N $$

To explore these different semantics in a unified way we devise the notion of an *index accumulator*, a data structure used to accumulate the indices of the targets when casting terms of an indexed inductive types. The three examples above can be interpreted using different index accumulators: the free semantics can be interpreted using a list to accumulate every index, the meet semantics can be interpreted using a pair holding the accumulated precision meet [Siek and Wadler 2010] together with the outermost index, and the forgetful semantics can be interpreted using an option type to record the index of the outermost cast, if any. Rewriting the previous examples using index accumulators (in blue) we get the following:

$$ 
\begin{aligned}
\langle \forall A 0 \equiv \forall A 1 \equiv \forall A 0 \rangle \text{nil} &\rightarrow \text{nil} [0, 1] & (F) \\
&\rightarrow \text{nil} (0, \text{err}_N) & (M) \\
&\rightarrow \text{nil} (\text{some } 0) & (U)
\end{aligned}
$$

Apart from the way that indices of casts are accumulated, all semantics share most of their typing and reduction rules. We abstract indexed inductive definitions into a framework, called PUNK, parametrized by an abstract index accumulator. We give a formal definition of index accumulators as a type inhabited by a distinguished term that represents the absence of casts and an action over indices used to accumulate them. For instance, the free index accumulator is a list of indices, where the distinguished term is the empty list and the action is appending an index to the head of the list. Precision on index accumulators must reflect the fact that they are used to accumulate casts and therefore should internalize properties of precision such as monotonicity and retraction [Maillard et al. 2022]. The index accumulator abstraction enables us to prove general properties, such as subject reduction and graduality, for any concrete semantics of gradual indexed inductive types, as long as its corresponding index accumulator satisfies certain properties.

As indexed inductive types are widely used in both theorem proving and dependently-typed programming, this work is an important step in the quest for making gradual theorem provers and gradual dependently-typed programming languages a reality.

### Contributions.

* We explore the design space of indexed inductive types, identify various semantics and characterize them in three different classes, based on the interaction between elimination and casts, in terms of precision (§ 3).

* We propose the PUNK framework, an extension of GRIP with gradual indexed inductive types, supporting multiple cast semantics (§ 5).
* We formally establish the metatheory of PUNK and provide instances for the three classes of inductive families (§6).

## 2 Background on Gradual Dependent Type Theory

In this section we give an overview on the work that this articles builds upon, its base gradual type theory and some previous approaches to gradual indexed inductive types.

### 2.1 The Gradualized Calculus of Inductive Constructions (GCIC)

Lennon-Bertrand et al. [2022] introduced GCIC, an extension of the Calculus of Inductive Constructions (CIC), which incorporates gradual typing to the language. Like in a gradually typed lambda calculus, GCIC has an unknown type $?\square$, optimistically representing any type, and an ascription operator $t :: B$ that allow to treat a term $t$ as if it had type $B$ regardless of the actual type of $t$. This permits the construction of terms like $u \triangleq (\lambda(x : ?\square).\text{not } x) 0$ that, although optimistically well-typed, informally correspond to a run-time failure that dynamically enforce typing invariants.

In GCIC, the semantics are defined by elaboration into a cast calculus named CASTCIC. This calculus extends CIC, introducing two exceptional terms $err_A$ and $?_A$ that represent runtime errors and unknown terms for any given type $A$, respectively. Additionally, CASTCIC introduces a casting operator $\langle B \leftarrow A \rangle t$ coercing a term $t$ of type $A$ to a term of type $B$. As an example, the previous GCIC expression $u$ elaborates in CASTCIC to $(\lambda(x : ?\square).(\text{not } \langle B \leftarrow ?\square \rangle t))(\langle ?\square \leftarrow \mathbb{N} \rangle 0)$. Casts in CASTCIC then reduce by comparing their source and target type, failing dynamically when a mismatch is found. In the running example, after $\beta$-reducing the top-most redex, we obtain not $\langle B \leftarrow ?\square \rangle$ ($\langle ?\square \leftarrow \mathbb{N} \rangle 0$) that reduces to not $err_B$ because 0 is not a canonical form of type $B$. A gradual dependent type system introduces a new challenge since computations involving exceptional terms may appear in types.

CASTCIC features a single hierarchy of universes, denoted as Type or $\square$. The calculus supports simple inductive types like $\mathbb{N}$ or $\mathbb{B}$, as well as parameterized types like list. However, it does not offer a generalized support for indexed inductive types. In CASTCIC, every type includes exceptional terms in the form of runtime errors ($err$) and unknown terms (?), with the following typing rules:

$$ \frac{\Gamma \vdash A : \square_\ell}{\Gamma \vdash err_A : A} $$

$$ \frac{\Gamma \vdash A : \square_\ell}{\Gamma \vdash ?_A : A} $$

These exceptional terms follow a *call-by-name* semantics [Pédrot and Tabareau 2018], implying that errors and unknown terms do not propagate unless they are forced in a computation. For example, $(\lambda(x : \mathbb{N}).0) \text{ err}_\mathbb{N}$ reduces to 0 rather than propagating $\text{err}_\mathbb{N}$. Exceptional terms are considered canonical forms for positive types, while for negative types, they propagate exceptions when observed. For instance $\text{err}_\mathbb{N} \rightarrow \text{err}_\mathbb{N}$ reduces to $(\lambda(x : \mathbb{N}).\text{err}_\mathbb{N})$.

Furthermore, CASTCIC includes the previously mentioned cast operator $\langle B \leftarrow A \rangle t$, allowing terms of one type to be interpreted as another. The typing rule for casts its the expected one:

$$ \frac{\Gamma \vdash A : \square_\ell \quad \Gamma \vdash B : \square_\ell \quad \Gamma \vdash t : A}{\Gamma \vdash \langle B \leftarrow A \rangle t : B} $$

Throughout this paper we use the notation $\langle C \leftarrow B \leftarrow A \rangle t$ as a shorthand for two consecutive casts $\langle C \leftarrow B \rangle \langle B \leftarrow A \rangle t$.

**The fire triangle of graduality.** Lennon-Bertrand et al. [2022] study three properties, apart from subject reduction, that can be expected from a gradual type theory: normalization, conservativity with respect to a theory, and graduality. Normalization ensures the logical consistency of the system and is a desirable property for any type theory, especially when used as the underlining theory of
a theorem prover. The other two properties are part of the *gradual guarantees* [Siek et al. 2015a], a group of properties expected from every gradually -typed language. Conservativity with respect to a static system states that the semantics of the gradual and static systems coincide on their common terms. Finally, graduality [New and Ahmed 2018] ensures that dynamic checks, such as casts, should only perform type checking: successful casts cannot affect the behavior of a program and invalid ones should fail more. However, the *Fire Triangle of Graduality* [Lennon-Bertrand et al. 2022] states that any gradual type theory cannot simultaneously satisfy the three properties. Consequently, GCIC and CASTCIC come in three variants, each one sacrificing one property.

## 2.2 Internal Notion of Precision

Maillard et al. [2022] present GRIP, an extension of CASTCICN—the normalizing variant that sacrifices graduality as a global property—that introduces an internal representation of precision. This allows the user to reason about precision and graduality of terms within the type theory itself. To this end, they introduce an additional hierarchy of universes, denoted Prop, beside that of gradual types. Prop is a proof-irrelevant hierarchy of universes dedicated to *pure* propositions: propositions that can be *about* exceptional terms (*err* or ?) but cannot be *inhabited* by these exceptional terms. Prop hosts two key relations for internal reasoning about precision: *term precision* and *type precision*. Term precision, noted $a_{A \sqsubseteq B} b$, states that the term *a* of type *A* is more precise than *b* of type *B* as terms, with the unknown term $?_B$ as a top element and $err_A$ as a bottom element. Term precision is an heterogeneous relation, i.e., the types *A* and *B* are not required to be the same. Type precision, noted $A \sqsubseteq_\ell B$, states that *A* is more precise than *B* as types at universe level *l*. This distinction circumvents the *Fire Triangle*: the unknown type is not a top element for type precision and term precision for types: $A \sqsubseteq \Box$, $B$ only holds when *A* is more precise than *B* as a term, and are bounded by the unknown type $?_\Box$ (i.e., $A \sqsubseteq_\ell B \wedge B \sqsubseteq_\ell ?_\Box$).

The precision relations live in the pure fragment of GRIP and therefore forbid *exceptional* proofs. Precision is a transitive relation, but unlike in more simple type systems, only the *gradual terms* (i.e., terms for which graduality holds) are related to themselves, or *self-precise*. In particular, functions are self-precise when they are *monotone* with respect to precision (i.e., they map related inputs to related outputs). We write $A \sqsubseteq$ when a type *A* is self-precise at the level of types and $a \sqsubseteq_A$ when a term *a* of type *A* is self-precise as a term. Precision cannot be reflexive in general because it would break conservativity of the system with respect to CIC, forbidding non-monotone functions, such as a dependently-typed `printf` function. Instead, precision is *quasi-reflexive*, meaning that if two terms are related by precision, then both are self-precise.

Since GRIP admits non-self-precise terms and can consistently reason about the precision of programs, the authors consider a general eliminator *catch* for inductive types that provide branches for exceptional inhabitants [Pédrot et al. 2019]. These exceptional branches allow the user to handle exceptions as they see fit. Therefore, *catch* makes it possible to define non-monotone functions: e.g., consider $f : \mathbb{B} \to \mathbb{B}$ that matches on a boolean, swaps $err$ and ? (i.e., $f err_\mathbb{B} \to ?_\mathbb{B}$ and $f ?_\mathbb{B} \to err_\mathbb{B}$) and is the identity on pure booleans. However, *catch* is monotone whenever each constructor branch falls between the error branch and the unknown branch in terms of precision [Maillard et al. 2022]. Under mild assumptions on the precision of the motive and branches, a monotone eliminator *elim* not mentioning the exceptional cases can then be systematically derived from *catch* by forwarding the exceptions.

## 2.3 Basics of Indexed Inductive Types

Now we turn our focus to the main subject of this paper, namely indexed inductive types. In simple terms, indexed inductive types are just a *shape* plus an *index*. By shape we mean the basic
<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 1. Encodings of indexed inductive types in Coq</figcaption></figure>

structure of inhabitants of the type, for example, the shape of `list N`, lists of natural numbers, is a finite (thanks to the constructor `nil`) sequence of numbers (using the constructor `cons`). The constructors completely describe the shape of their inductive type, meaning that every closed term of the inductive must be convertible to one of its constructors. This enables the use of case analysis to eliminate the terms of an inductive type and more importantly it induces an induction principle to establish properties of these terms. Indices, on the other hand, constrain the terms inhabiting an indexed inductive type, encoding properties and invariants of the inductive data. For example, we can encode sized list of `A` as a type `V A n` indexed by a natural number `n` where constructors are annotated with their size: the empty list `nil` has length 0 and cons'ing a new element on top of a list increases the length of the list by 1. Indices are specially useful to eliminate impossible cases when reasoning using induction. For instance, we can define the function `hd` in Coq that extracts the head of a vector with at least one element like this:

<figure><img src="image_6.png" /></figure>

This function is defined by case analysis on the vector argument `v`; if the vector is a `cons` it returns its content, but if the vector is empty (i.e., it is `nil`) there is no content to extract! The latter case does not need to be considered since the type of the function makes it impossible to apply it to an empty vector.

Incorporating explicit support for indexed inductive types in a type theory that already accommodates standard inductive types is not strictly essential for their definition. This can be achieved by leveraging the existing features within the system (e.g., see $V_{eq}$ in Figure 1). However, this approach can result in reduced logical strength, leading to diminished expressiveness and the introduction of potential inconsistencies. For instance, without the capability for large elimination—namely, the ability to construct a type depending on the structure of an inductive type—there are certain types and functions related to these types that cannot be adequately expressed (e.g., see $V_{fix}$ in Figure 1). For instance, the absence of large elimination precludes the definition of a type family over booleans that is inhabited exclusively in the true fiber. Furthermore, this limitation extends to function definitions; specifically, the `hd` function cannot be defined, as its correct application necessitates a `V` with a length strictly greater than zero to ensure subject reduction.

Previous approaches to indexed inductive types in CASTCIC. Although Lennon-Bertrand et al. [2022] presents a way to define non indexed inductive types and indexed inductive types with forceable indices, they argue that extending CASTCIC with a general notion of indexed inductive types is not trivial. Their approach is to extend indexed inductive type definitions with extra constructors that represent casts to the unknown index. For instance, the definition of the type `V` for lists indexed by their length is extended with two new constructors `nil`? representing $\langle V A?_N \leftarrow V A 0 \rangle$ `nil` and `cons`? representing $\langle V A?_N \leftarrow V A (S n) \rangle$ `cons n x xs`. Cast on constructors to imprecise indices reduce to their imprecisely indexed counterparts and vice versa on cast from imprecise indices.

<figure><img src="image_7.png" /></figure>

This approach does not generalize to arbitrary indices because the reduction rules discriminate the indices of the cast, here $?_N$ and 0. Indices taken in a function type or an arbitrary type, like in the case of propositional equality, cannot be discriminated in this fashion.
Eremondi et al. [2022] solves this problem for propositional equality $x =_A y$, by extending refl with a new argument $w$, more precise than both indices $x, y : A$, that serves as a witness of the casts that have been performed on the equality proof. In this approach, casts on refl are performed without matching on the target's index and are instead accumulated in the witness using the meet of the indices of the casts. For this reason, they define an operator, called composition, that computes the meet with respect to precision of any two terms. This operation is defined for every type, even dependent products.

The elimination of propositional equality via the J rule performs the substitution as usual and then casts the result to and from the predicate applied to the witness. If $M$ is a predicate over $A$, $a$ and $b$ two terms of type $A$, $t$ an instance of $Ma$, and refl$_w$ a proof of $a =_A b$ with witness $w$, the reduction for J is defined as follows:

$$J(A, x.Mx, a, b, t, \mathrm{refl}_w) \rightsquigarrow \langle Mb \Leftarrow Mw \rangle \langle Mw \Leftarrow Ma \rangle t$$

Using propositional equality it is possible to define indexed inductive types out of parametrized inductive types using fording,<fnref n="2" /> that is, using a proof of equality to enforce that the constructors have the correct index. For instance, in the definition for vectors the index $\mathbb{N}$ becomes a parameter ($n : \mathbb{N}$) and the type of each constructor is now guarded by an equality constraint on $n$:

Inductive $V(A : \square) (n : \mathbb{N}) : \square :=$

| nil : $n = 0 \rightarrow VAn$

| cons : $\forall (m : \mathbb{N}), n = S m \rightarrow A \rightarrow VAm \rightarrow VAn$.

Note that this approach requires the definition of inductive types with non-uniform parameters (i.e., parameters that can vary in recursive occurrences of the inductive type). Moreover, this approach reflects the cast reduction semantics of propositional equality. In this paper, we explore multiple cast reduction semantics and provide a direct approach instead of relying on this encoding.

# 3 Overview of Gradual Indexed Inductive Types and Punk

Since previous approaches to gradual indexed inductive types have shortcomings, we pursue here a general and proper treatment of these suitable for a gradual proof assistant. In this section we give a high level presentation of our solution for supporting indexed inductive types in a gradual type theory. In §3.1, we address the question of encoding gradual indexed inductive types using features already available in type theory, exhibiting their limitations, and devise well-behavedness criterion in §3.2. Then, we explore some possible semantics for gradual indexed inductive types (§3.3) and finish by giving an overview of our solution (§3.4).

## 3.1 Encodings Are Not Satisfactory

Fixpoint encoding. Inductive types indexed on inductive indices sometimes admit an encoding as a type level fixpoint in a non-gradual type theory [Brady et al. 2004]. In that situation, the type family is defined as a Type-valued recursive function by induction on indices. For example, the fixpoint encoding of vectors $V_{fix}$ (Figure 1) is defined by mapping the index 0 to the unit type $\top$ with a single element for the argument-less constructor nil, and $S^n$ to the product $A \times V_{fix} A^n$ for cons, which takes an element of type $A$ and a vector of length $n$ to produce a vector of length $S^n$.

However, in a gradual setting this encoding admits more terms than one would expect on unknown indices. For instance, the type $V_{fix} A ?_N$ is convertible to the unknown type $?\square$: any term of any type can be cast to a valid vector of unknown index (e.g., $\langle?\square \Leftarrow \mathbb{N}\rangle 0 : V_{fix} \mathbb{B} ?_N$). The introduction of these extra inhabitants break the expected shape of the type, since it will be

<footnote n="2">²This technique was invented by Coquand for his work on the proof assistant ALF in the 1990s, as a way to reduce indexed inductive types to parametrized inductive types and an equality type. The name fording was first coined by McBride [1999].</footnote>
inhabited by constructors other than nil and cons. On the other hand, nil and cons are still the only non exceptional canonical forms with indices 0 and $S n$, respectively, thus respecting the constraints enforced by the indices.

*Subset type encoding.* Subset types {$a : A \mid M a$} represent elements of a carrier type A satisfying some predicate $M : A \to \text{Prop}$, that is the subset of the inhabitants $a$ of A for which $M a$ holds. Terms of a subset type are tuples $(a, p)$ consisting of a term $a : A$ and a proof $p : M a$.

In non-gradual type theories it is possible to encode an indexed inductive type as the subset of a non-indexed inductive type with the same shape whose elements satisfy the properties represented by their indices [Caglayan 2021]. For instance, vectors can be encoded as a list together with a proof that it has the correct size ($V_{eq}$ in Figure 1).

In contrast, subset types do not behave well in a gradual type theory. The core issue lies in the incompatibility of propositions with gradual operations. Essentially, any gradual proposition is inhabited by exceptional proofs making the system inconsistent and logically unsound: $⊥$ is trivially provable by $?⊥$. Moreover, casts between gradual propositions would need to synthesize proofs on the fly. Since arbitrary proofs cannot be synthesized in a computable and total fashion, Maillard et al. [2022] define cast between gradual propositions to always reduce to an exception.

Therefore, gradual subset types cannot enforce properties over terms, and the corresponding encoding of indexed inductive types does not maintain the invariants associated to the indices across casts. For instance, it would be easy to construct an empty vector with index 1 as $(\text{nil}, \text{err}_{\text{length nil}=1})$. Since, using this encoding, the index of an inductive type says nothing about its inhabitants, indexed inductive types degenerate into regular non-indexed inductive types (e.g., vectors become equivalent to lists).

## 3.2 Requirements for Gradual Indexed Inductive Types

Informally, the encodings presented in the previous section do not provide the invariants expected from indexed inductive types. We identify two criteria to guarantee that an implementation of gradual indexed inductive types do not exhibit these issues. These criteria, *index relevance* and *shape relevance*, correspond to the two key characteristics of indexed inductive types, their shape and index.

*Definition 3.1 (Index relevance).* A self-precise type family $X : A \to \Box_{\ell'}$ over $A : \Box_{\ell}$ is index relevant when precision-related instances of $X$ imply relatedness of the indices:

$$ \forall (a, a' : A) . X a \sqsubseteq_{\ell'} X a' \to a \sqsubseteq_{A} a' $$

In categorical language, $X$ is full and faithful, when viewed as a functor from the precision preorder on the domain $A$ to the type precision preorder.

For instance, the inductive family $\mathbb{V}$ of vectors is index relevant if $\mathbb{V} A m \sqsubseteq_{\ell} \mathbb{V} A n$ implies $m \sqsubseteq_{\mathbb{N}} n$. As we saw in §3.1, encoding indexed inductive types as subset types cannot be index relevant.

*Definition 3.2 (Shape relevance).* A self-precise type family $X : A \to \Box_{\ell'}$ over $A : \Box_{\ell}$ is shape relevant if its image $\{X a\}_{a : A} : \Box_{\ell'}$ in the universe is both upward and downward closed with respect to precision:

$$ \forall (a : A) . a \sqsubseteq_{A} \to T \sqsubseteq_{\ell} X a \to (\exists (a' : A), T = X a') \lor (T = \text{err}_{\Box_{\ell'}}) $$

$$ \forall (a : A) . a \sqsubseteq_{A} \to X a \sqsubseteq_{\ell} T \to (\exists (a' : A), T = X a') \lor (T = ?_{\Box_{\ell'}}) $$

Put simply, an inductive is shape relevant if it is only related by precision with the error type $\text{err}_{\Box}$, the unknown type $?_{\Box}$ and itself, possibly applied to different parameters and indices. This criterion excludes degenerated cases such as $\mathbb{N} \sqsubseteq_{\ell} \mathbb{V} A ?_{\mathbb{N}}$ and ensures that inductive types are
Inductive $\mathbf{vec}(A : \Box) : N \to \Box :=$
| nil : $\mathbf{vec} A 0$
| $\mathbf{cons} : \forall (n : N), A$
  $\to \mathbf{vec} A n \to \mathbf{vec} A (S n)$.

Definition $f\_ty(n: N): \Box :=$
catch n with
| 0 $\Rightarrow$ list $N$ | $err_N$ $\Rightarrow$ $err_\Box$
| $S$ $\Rightarrow$ list $\mathbb{B}$ | $unk_N$ $\Rightarrow$ $err_\Box$ end.

Fixpoint $\mathbf{len}\{A n\} (v : \mathbf{vec} A (S n)) : N :=$
catch v with
| nil $\Rightarrow$ 0 | $err \Rightarrow$ $err_N$
| $\mathbf{cons\_v}$ $\Rightarrow$ $S(\mathbf{len} v)$ | $unk \Rightarrow$ $err_N$ end.

Definition $f\{A n\} (v : \forall A n) : f\_ty n :=$
catch v with
| nil $\Rightarrow$ [0] | $err \Rightarrow$ $err$
| $\mathbf{cons\_v}$ $\Rightarrow$ [true] | $unk \Rightarrow$ $unk$ end.

<caption>Fig. 2. Definitions illustrating the behaviors of cast on GIIT in Gallina (Coq).</caption>

not inhabited by canonical forms of other types, a condition violated by fixpoint encodings (§3.1). Conversely, the approaches to gradual indexed inductive types discussed in §2.3 satisfy both criteria. We consider essential to ensure that the definition of well-behaved inductives encompasses the prior research on gradual indexed inductive types.

Apart from these two criteria, we also need to ensure that the gradual indexed inductive types satisfy the relevant gradual properties, in particular inductive type constructors must be self-precise. Following Maillard et al. [2022], self-precision for a type family $X : A \to \Box$ mandates that any two elements $a, a' : A$ related by precision $a \underset{A}{\sqsubseteq} a'$ yield precision-related types $X a \sqsubseteq_X a'$, that in turn need to preserve *graduality* [New and Ahmed 2018].

*Definition 3.3 (Graduality).* Cast between types related by precision $X \sqsubseteq_\ell Y$ induce an embedding-projection pair, meaning a Galois connection $\langle Y \leftarrow X \rangle \leftrightarrow \langle X \leftarrow Y \rangle$ with respect to precision such that $\langle Y \leftarrow X \rangle \circ \langle X \leftarrow Y \rangle \supseteq \mathrm{id}_X$.

## 3.3 Possible Semantics for Gradual Indexed Inductive Types

As we saw in §1, there are many valid semantics for gradual indexed inductive types, and it is not clear if one is better than the other. These different inductive definitions can be classified according to their eliminator's interaction with casts, up to precision. Since precision is asymmetric, we identify three primary behaviors: preservation of precision (equiprecise elimination), gain in precision (underprecise elimination), and loss of precision (overprecise elimination), explicitly excluding the case when there is no relation. In the following, we explore how inductive types from each of these classes behave, illustrated with examples. In each example we observe the behavior of the three semantics for vectors illustrated in the introduction.

### 3.3.1 Eliminating with a Constant Motive.
We start with a simple example: computing the length of the vector $\langle V \mathbb{B} 0 \equiv V \mathbb{B} 1 \equiv V \mathbb{B} 0 \rangle$ nil using the function $\mathbf{len}$ provided in Figure 2.

*Free vectors.* Casts on free vectors do not reduce, delegating the task of evaluating casts to the result of an elimination:

$$ \mathrm{len}(\langle V \mathbb{B} 0 \equiv V \mathbb{B} 1 \equiv V \mathbb{B} 0 \rangle \mathrm{nil}) \rightsquigarrow \langle N \leftarrow N \leftarrow N \rangle (\mathrm{len nil}) \rightsquigarrow \langle N \leftarrow N \leftarrow N \rangle 0 \rightsquigarrow 0 $$

*Meet vectors.* Casts on meet vectors reduce to a meeting and then propagates the casts:

$$ \begin{align*} \mathrm{len}(\langle V \mathbb{B} 0 \equiv V \mathbb{B} 1 \equiv V \mathbb{B} 0 \rangle \mathrm{nil}) &\rightsquigarrow \mathrm{len}(\langle V \mathbb{B} 0 \equiv V \mathbb{B} \ \mathrm{err}_N \equiv V \mathbb{B} 0 \rangle \mathrm{nil}) \\ &\rightsquigarrow \langle N \leftarrow N \leftarrow N \rangle (\mathrm{len nil}) \rightsquigarrow \langle N \leftarrow N \leftarrow N \rangle 0 \rightsquigarrow 0 \end{align*} $$
**Forgetful vectors.** Forgetful vectors ignore intermediate casts and so maintain at most one cast:

$$ 
\begin{align*}
\text{len}(\langle \mathbf{VB}0 \equiv \mathbf{VB}1 \equiv \mathbf{VB}0 \rangle \text{nil}) &\rightsquigarrow \text{len}(\langle \mathbf{VB}0 \equiv \mathbf{VB}0 \rangle \text{nil}) \\
&\rightsquigarrow \langle \mathbf{N} \equiv \mathbf{N} \rangle (\text{len nil}) \rightsquigarrow \langle \mathbf{N} \equiv \mathbf{N} \rangle 0 \rightsquigarrow 0
\end{align*}
$$

It is interesting to note that because the motive of the elimination ($\lambda_{\_\_}.\mathbf{N}$) does not depend on the index, the three semantics are equivalent.

**3.3.2 Eliminating with a Dependent Motive.** Let us examine a more interesting example. The function $f$ (Figure 2) operates on vectors with a return type $f\_ty$ that actually depends on the vector index. This function maps $0$ to $\text{list } \mathbf{N}$, $\mathbf{S}n$ to $\text{list } \mathbf{B}$, and exceptional naturals $\text{err}_\mathbf{N}$ and $?_\mathbf{N}$ to their corresponding exceptional types $\text{err}_\square$ and $?\square$. The function $f$ transforms the empty vector $\text{nil}$ to a singleton list $[0]$, cons vectors to $[\text{true}]$, and propagates exceptional terms. Recall that in exceptional type theory, exceptions are by-name [Pédrot et al. 2019], meaning that terms may have exceptions as subterms. In particular, this means that $[\text{err}_\mathbf{N}]$ is a normal form and does not reduce to $\text{err}_{\text{list}\mathbf{N}}$. Given that $f$'s return type is dependent, applying our three vector semantics to $f \ \mathbf{v}$ reveals varied outcomes.

**Free vectors.** In the free semantics every cast is taken into account and, after propagating the casts outside of the eliminator, an intermediate cast through $\text{list } \mathbf{B}$ remains. Since we only perform casts between lists, the shape of the list is preserved (i.e., it stays a singleton), but the inner cast fails because the parameters are incompatible, resulting in a singleton list with an error inside.

$$ 
\begin{align*}
f \langle \mathbf{VB}0 \equiv \mathbf{VB}1 \equiv \mathbf{VB}0 \rangle \text{nil} \\
&\rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{list } \mathbf{B} \equiv \text{list } \mathbf{N} \rangle (f \text{ nil}) \rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{list } \mathbf{B} \equiv \text{list } \mathbf{N} \rangle [0] \\
&\rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{list } \mathbf{B} \rangle [\langle \mathbf{B} \equiv \mathbf{N} \rangle 0] \rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{list } \mathbf{B} \rangle [\text{err}_\mathbf{B}] \rightsquigarrow [\text{err}_\mathbf{N}]
\end{align*}
$$

**Meet vectors.** Meet semantics consolidate intermediate casts into one, through the accumulated meet of their indices, here represented by $0 \sqcap 1 \rightsquigarrow \text{err}_\mathbf{N}$. After propagating the casts out of the eliminator, the intermediate cast goes through $\text{err}_\square$ because $f\_ty$ propagates the exception. In contrast to the free semantics, the structure of the list is not preserved.

$$ 
\begin{align*}
f \langle \mathbf{VB}0 \equiv \mathbf{VB}1 \equiv \mathbf{VB}0 \rangle \text{nil} \\
&\rightsquigarrow f \langle \mathbf{VB}0 \equiv \mathbf{VB} \text{ err}_\mathbf{N} \equiv \mathbf{VB}0 \rangle \text{nil} \rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{err}_\square \equiv \text{list } \mathbf{N} \rangle (f \text{ nil}) \\
&\rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{err}_\square \equiv \text{list } \mathbf{N} \rangle [0] \rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{err}_\square \rangle \text{err}_{\text{err}_\square} \rightsquigarrow \text{err}_{\text{list}\mathbf{N}}
\end{align*}
$$

**Forgetful vectors.** In the forgetful semantics the intermediate cast through $\mathbf{VB}1$ is dropped allowing the computation to recover from what could have been an invalid state.

$$ 
\begin{align*}
f \langle \mathbf{VB}0 \equiv \mathbf{VB}1 \equiv \mathbf{VB}0 \rangle \text{nil} &\rightsquigarrow f \langle \mathbf{VB}0 \equiv \mathbf{VB}0 \rangle \text{nil} \\
&\rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{list } \mathbf{N} \rangle (f \text{ nil}) \rightsquigarrow \langle \text{list } \mathbf{N} \equiv \text{list } \mathbf{N} \rangle [0] \rightsquigarrow [0]
\end{align*}
$$

Interestingly, the outcomes of these semantics are distinguished by their precision levels. Specifically, meet vectors yield more precise results than free vectors, which in turn are more precise than those from forgetful semantics: $\text{err}_{\text{list},\mathbf{N}} \subseteq [\text{err}_\mathbf{N}] \subseteq [0]$.

This illustrates the fact that each of these semantics belongs to a unique class of inductive types—free vectors to equiprecise elimination, meet vectors to underprecise elimination, and forgetful vectors to overprecise elimination. Importantly, this classification extends beyond vectors, applying to all indexed inductive types and highlighting the nuanced behavior of these three semantic approaches.
<figure><img src="image_8.png" /></figure>

<table><caption>Fig. 3. Defining components for an indexed inductive type</caption><thead><tr><th>Name</th><th>Description</th><th>Well-formedness</th></tr></thead><tbody><tr><td>Param</td><td>Parameters of the inductive I</td><td> Param tele</td></tr><tr><td>Idx<sup>ρ</sup></td><td>Indices of the inductive I</td><td> Param Idx<sup>ρ</sup> tele</td></tr><tr><td>#actors</td><td>Number of constructors of the inductive I</td><td>#actors ∈ N</td></tr><tr><td>Arg<sub>c</sub><sup>ρ</sup></td><td>Arguments of the constructor c</td><td> Param Arg<sub>c</sub><sup>ρ</sup> tele</td></tr><tr><td>#indargs<sub>c</sub></td><td>Number of inductive arguments of c</td><td>#indargs<sub>c</sub> ∈ N</td></tr><tr><td>IndArg<sub>c,k</sub><sup>ρ</sup></td><td>Arguments of the k-th inductive argument of c</td><td> Param, Arg<sub>c</sub><sup>ρ</sup> IndArg<sub>c,k</sub><sup>ρ</sup> tele</td></tr><tr><td>arg_idx<sub>c,k</sub><sup>ρ</sup></td><td>Indices of the k-th inductive argument of c</td><td> Param, Arg<sub>c</sub><sup>ρ</sup>, IndArg<sub>c,k</sub><sup>ρ</sup> arg_idx<sub>c,k</sub><sup>ρ</sup> : Idx<sup>ρ</sup></td></tr><tr><td>ctr_idx<sub>c</sub><sup>ρ</sup></td><td>Indices of the constructor c</td><td> Param, Arg<sub>c</sub><sup>ρ</sup> ctr_idx<sub>c</sub><sup>ρ</sup> : Idx<sup>ρ</sup></td></tr></tbody></table>

<figure><img src="image_9.png" /><figcaption>Fig. 4. Defining components for the type family of vectors.</figcaption></figure>

*Forgetful inductives.* Forgetful inductives drop any intermediate cast and their accumulator holds only the target of the outermost cast if any. To this end, they accumulate indices using an option type where *none* stands for the absence of casts and *some* holds the index of its only cast when needed. Therefore the expected cast reduction rule for forgetful vectors is encoded as follows.

$$ (\mathbb{V}\mathbb{B}0 \leftarrow \mathbb{V}\mathbb{B}1 \leftarrow \mathbb{V}\mathbb{B}0) (\text{nil none}) \rightsquigarrow (\mathbb{V}\mathbb{B}0 \leftarrow \mathbb{V}\mathbb{B}1) (\text{nil (some 1)}) \rightsquigarrow \text{nil (some 0)} $$

The semantics that we explore in this paper use non-indexed inductive types as their index accumulators, however our framework is more general and it is not restricted to such types.

*Summary.* We saw that there is not a unique way to give semantics to gradual indexed inductive types. There is a degree of freedom regarding how casts commute with the eliminator up to precision and we have identified three meaningful alternatives. Each of these options gives rise to a class of indexed inductive types. PUNK supports each of these classes with a specific instance: free, forgetful, and meet inductives. The semantic differences are captured by different choices of an index accumulator.

*A note on language design.* A specific gradual proof assistant can decide to either embrace a given accumulator semantics once and for all, or opt to allow programmers to configure this choice, either globally or on a case-by-case basis. In the latter option, the choice of the accumulator semantics can be made independently for each gradual indexed inductive type. In theory, one can even support two implementations of the same inductive family with different accumulator semantics; however, in that case, the two families are unrelated by precision, so any cast between them fails. As a formal framework designed to study these semantics, PUNK is agnostic with respect to this issue.
$\Gamma \vdash t : T$

II-TY
$\Gamma \vdash p : \mathbf{Param} \qquad \Gamma \vdash i : \mathbf{Index}^p$

$\Gamma \vdash \mathbb{I} pi : \Box \ell$

II-CTOR
$\Gamma \vdash p : \mathbf{Param} \qquad \Gamma \vdash a : \mathbf{Arg}_c^p$

$\forall j < \#\mathbf{indargs}_c, \Gamma \vdash r_j : \Pi(x_j : \mathbf{IndArg}_{c,j}^p a), \mathbb{I} p (\mathbf{arg\_idx}_c^p a x_j)$

II-ELIM
$\Gamma \vdash p : \mathbf{Param} \qquad \Gamma \vdash M : \Pi(i : \mathbf{Index}^p), \mathbb{I} pi \to \Box \ell'$

$\forall k < \#\mathbf{actors}, \Gamma \vdash h_{c_k} : \mathbf{Branch}_{c_k}^p M \qquad \Gamma \vdash i : \mathbf{Index}^p \qquad \Gamma \vdash t : \mathbb{I} pi$

$t \rightsquigarrow t$

canonical $t$

II-ELIM-CTOR: $\mathrm{elim}^p M \overrightarrow{h_{c_k}} i (c^p a \overrightarrow{r_j}) \rightsquigarrow h_c a \overrightarrow{r_j} t_j$

$t_j \triangleq \lambda(x_j : \mathbf{IndArg}_{c,j}^p a), \mathrm{elim}^p M \overrightarrow{h_{c_k}} (\mathbf{arg\_idx}_{c,j}^p a x_j)(r_j x_j)$

EVALUATION CONTEXTS
$C ::= \dots | \mathrm{elim}^p M \overrightarrow{h_{c_k}} i C$

RED-CONG
$t \rightsquigarrow t'$
$C[t] \rightsquigarrow C[t']$

canonical $c^p a \overrightarrow{r_j}$

<caption>Fig. 5. Typing and reduction rules for static inductive types.</caption>

## 4 Syntax and Semantics of Indexed Inductive Families

General formal accounts of indexed inductive types are notationally demanding. In this section, we fix notations for indexed inductive types in CIC, and give their static and dynamic semantics. These notations are employed to present gradual indexed inductive types in subsequent sections.

An inductive definition specify a type constructor **I**, term constructors **c** that serve as the canonical inhabitants of the inductive type, and an eliminator **elim** that consumes inductive terms of type **I** via case analysis with one branch for each of the inductive's term constructors.

The typing rules for static indexed inductive types (Figure 5) use a collection of metafunctions associated to the inductive definition (Figure 3).<fnref n="3" /> Most metafunctions are parameterized by an instance *p* of the telescope of parameters **Param**. As an illustration, the components for the type family of vectors is shown in Figure 4.

**Introduction.** An inductive type family **I** is introduced as a type **I** *pi* using Rule **I-TY** with substitutions *p* and *i* for the telescopes of parameters and indices. A term of that type is formed through a constructor $c^p a \overrightarrow{r_j}$ (Rule **I-CTOR**) where *p* is an instantiation of the parameters, *a* an instantiation of the non-inductive arguments and each $r_j$ for $j \in \{0, \dots, \#\mathbf{indargs}_c\}$ is an inductive argument. The indices of the constructor are computed out of *a* and each inductive argument use the same instantiation of parameters but possibly different indices. Note that we force the inductive arguments to be strictly positive.

**Elimination.** The eliminator **elim** performs case analysis on a term of an indexed inductive type. It consists of a motive **M**: $\Pi(i : \mathbf{Index}^p), \mathbb{I} pi \to \Box$, the return type of the elimination; a method $h_{c_k}$ for each constructor $c_k$, that prescribes the behavior of **elim** on that constructor; and a term to be eliminated together with its index. Each branch takes both the non-inductive and inductive arguments of the constructor, and then the induction hypotheses induced by these inductive arguments.

<footnote n="3">³Inductive definitions are typically carried in a typing signature $\Sigma$ along the typing judgement and queried through the metafunctions. To simplify the notations we omit these signatures, and often let inductive annotation **I** implicit.</footnote>
$$
\begin{align*}
\text{Branch}_c^p M \triangleq & \Pi(a : \mathbf{Arg}_c^p) && \text{non-inductive arguments} \\
& (\forall j, (r_j : \Pi(x_j : \mathbf{IndArg}_{c,j}^p a), \mathbf{I} p(\mathbf{arg\_idx}_{c,j}^p ax_j))) && \text{inductive arguments} \\
& (\forall j, (\Pi(x_j : \mathbf{IndArg}_{c,j}^p a), M(\mathbf{arg\_idx}_{c,j}^p ax_j) (r_j x_j))), && \text{induction hypotheses} \\
& M(\mathbf{ctr\_idx}_c^p a) (c^p a \overrightarrow{r_j}) &&
\end{align*}
$$

The constructors are the only canonical forms (Figure 5) and there is just one reduction rule: the elimination of constructors (II-ELIM-CTOR) that applies the correct branch and uses recursive calls to the eliminator as the induction hypotheses.

5 PUNK: A Framework for Gradual Inductive Family Definitions

We describe a framework called PUNK providing a schema for gradual indexed inductive types.<fnref n="4" />
The reduction semantics of casts for each gradual indexed inductive type is derived uniformly from
an index accumulator (§5.1). Section §5.2 provides instances of index accumulators to recover the
free, forgetful and meet reduction semantics of casts illustrated in the introduction. The static and
dynamic semantics are then derived in §5.3 for any choice of an index accumulator, as well as the
extension of internal precision for gradual indexed inductive types (§5.4).

**5.1 Index Accumulators**

*Definition 5.1 (Index Accumulator)*. An index accumulator (*Acc*<sup>*p*</sup>, ⊗<sup>*p*</sup>, 1<sup>*p*</sup>) over a telescope of parameters **Param** and indexing type family **Idx**<sup>*p*</sup> consist of (1) a gradual type family **Acc**<sup>*p*</sup> over *p* : **Param**, (2) a self-precise action ⊗<sup>*p*</sup> : **Idx**<sup>*p*</sup> × **Acc**<sup>*p*</sup> → **Acc**<sup>*p*</sup>, (3) a distinguished self-precise family of terms 1<sup>*p*</sup> : **Acc**<sup>*p*</sup>, satisfying the following precision inequations

$$
i_1 \otimes i_3 \otimes i_2 \otimes acc \sqsubseteq i_1 \otimes i_2 \otimes acc \qquad i_1 \sqsubseteq i_3, i_2 \sqsubseteq i_3, (i_2 \otimes acc)^{\sqsubseteq}, i_1, i_2, i_3 \in \mathbf{Idx}^p, acc \in \mathbf{Acc}^p \quad (1)
$$

$$
i_1 \otimes i_2 \otimes acc \sqsubseteq i_2 \otimes acc \qquad i_1 \sqsubseteq i_2, (i_2 \otimes acc)^{\sqsubseteq}, i_1, i_2 \in \mathbf{Idx}^p, acc \in \mathbf{Acc}^p \quad (2)
$$

$$
i_1 \otimes acc \sqsubseteq i_2 \otimes i_1 \otimes acc \qquad i_1 \sqsubseteq i_2, (i_1 \otimes acc)^{\sqsubseteq}, i_1, i_2 \in \mathbf{Idx}^p, acc \in \mathbf{Acc}^p \quad (3)
$$

Since every component of an index accumulator are systematically parametrized by an instance
*p*: **Param** of the telescope of parameters, we will omit it in the rest of the section. In particular,
we identify **1**: **Acc** with a single term and call it the empty accumulator. The inequalities in
Definition 5.1 reflects properties featured by precision on the universe of types in [Maillard et al.
2022]: Equation (1) is the upper-decomposition property, Equation (2) reflects that downcasts gain
precision, and Equation (3) reflects that upcasts lose precision. As a gradual family, **Acc** is also
inhabited by the exceptional terms that play no role in the formalization of indexed inductive types.

We are specifically interested in index accumulators whose elements can be interpreted as
sequences of indices. To that end, we observe that list of indices form the underlying type family
of an indexed accumulator Acc<sub>F</sub> that has an interesting property with respect to other index
accumulators: it is the universal index accumulator with a unique map I to any other index
accumulator. This can be phrased as a categorical property in the category of index accumulators,
with monotone structure-preserving functions – meaning that empty is mapped to empty and
actions to actions – as morphisms.

LEMMA 5.2 (INITIAL INDEX ACCUMULATOR). The initial index accumulator $Acc_F$ exists and has
list $\mathbf{Idx}^p$ as its underlying type. Moreover, precision for the free index accumulator admit an inductive
presentation for self-precise **Param**, $p$: **Param** and $\mathbf{Idx}^p$ presented in Figure 6.

The unique morphism $\mathbf{I}$ from $Acc_F$ to any index accumulator $Acc$ is the fold of the action starting
from the empty accumulator: $\mathbf{I}_{Acc}^p \quad acc \triangleq \quad \mathbf{fold} \otimes_{Acc} 1^p \quad Acc \quad acc$.

<footnote n="4">⁴The name PUNK comes from our naming convention for the branch for the unknown term for an eliminator with motive P.</footnote>
This explicit description of $Acc_F$ provides in particular a function $hd : Acc_F \to \text{option } Idx^p$ returning the head of a non-empty list. We can now turn to index accumulators whose elements can be interpreted as list of indices.

**Definition 5.3 (Listable Index Accumulator).** An index accumulator **Acc** is *listable* if the unique map $\mathbb{r} : Acc_F \to Acc$ has a left inverse $s : Acc \to Acc_F$ that preserves the empty element and partially preserve the action

$$ s^p 1 \rightsquigarrow^* [] \qquad (4) $$

$$ \mathbf{hd}(s(i \otimes acc)) \rightsquigarrow^* \text{ some } i \quad \forall i : \mathbf{Idx}, acc : \mathbf{Acc} \qquad (5) $$

A listable index accumulator is a retract of the initial index accumulator $Acc_F$ with retraction $\mathbb{r}$ and section $s$. Equation (4) is required for PUNK to be a conservative extension of CIC by ensuring that uncast terms are well-typed. Equation (5) is required for subject reduction by ensuring that casting a constructor (Rule GII-CTOR-CAST) has the correct type. Note that $s$ need not preserve the action. Indeed, $s$ preserves the action if and only if it is an inverse of $\mathbb{r}$, so $Acc$ and $Acc_F$ are then isomorphic. To support other semantics (e.g., forgetful), we weaken this requirement.

A listable index accumulator **Acc** can be queried for the last element accumulated through a function **get**: $\mathbf{Idx}^p \to \mathbf{Acc} \to \mathbf{Acc}$ defined as

$$ \mathbf{get} i acc \triangleq \mathbf{match} \mathbf{hd} (s acc) \mathbf{with} \text{none} \Rightarrow i | \text{some } i' \Rightarrow i' \text{ end} $$

## 5.2 Examples of Index Accumulators

We describe three different instances of listable index accumulators (Figure 6) corresponding to the three classes of cast reduction behavior identified in the introduction.

**The Free accumulator $Acc_F$.** The initial index accumulator $Acc_F$ faithfully accumulates every indices without losing any precision. By initiality, the precision on $Acc_F$ consist of exactly those relations derivable from the inequations Eqs. (1) to (3) and the congruence rules given by self-precision of $1^p$ and $\otimes$. It is listable with $s_{Acc_F} = \text{id}_{Acc_F}$.

**The Meet accumulator $Acc_M$.** $Acc_M$ follow the design of meet and combines intermediate casts using their meet with respect to precision, keeping at most two casts without any loss in precision. Meet accumulators provide a faithful optimization of the free semantics, meaning that they can error-approximate it using at most two casts.

The carrier of $Acc_M$ has two inhabitants, zero and two carrying the corresponding number of elements of $\mathbf{Idx}^p$, and representing respectively the absence of casts and a meeting. zero is the empty accumulator and the action accumulates the meet of the indices in the second argument of two. Here, the meet operation $\sqcap$ is inspired from the composition operator of Eremondi et al. [2022] that computes the greatest lower bound with respect to precision of any two terms. In the setting of GRIP, because not every term is self-precise, the specification of $\sqcap$ needs to be relativized to self-precise types and terms

$$ \text{For } T \sqsubseteq, \quad t_1^{\sqsubseteq_T} \wedge t_2^{\sqsubseteq_T} \quad \rightarrow \quad t_1 \sqcap t_2 \quad T \sqsubseteq_T \quad t_1 \wedge t_1 \sqcap t_2 \quad T \sqsubseteq_T \quad t_2. $$

The section $s$ returns all the accumulated indices and ensures that the corresponding list of indices has length at most two. The precision on $Acc_M$ stipulates that the two inhabitants are self-precise ($Acc_M$- zero and $Acc_M$- two).

**The Forgetful accumulator $Acc_U$.** $Acc_U$ discards any intermediate index and only preserves the last cast index, using the option type with inhabitants none and some as its underlying representation. The empty accumulator is none while the action always returns some of the newly
Free accumulator $Acc_F$

$Acc_F^p \triangleq \text{list } Idx^p$

$i \otimes_F acc \triangleq i :: acc$

$1_F^p \triangleq []$

$Acc_F-\sqsubseteq$-NIL

[] ⊑ []

$Acc_F-\sqsubseteq$-CONS

$i_1 \sqsubseteq i_2 \quad acc_1 \sqsubseteq acc_2$

$i_1 :: acc_1 \sqsubseteq i_2 :: acc_2$

$Acc_F-\sqsubseteq$-RET

$i_1 \sqsubseteq i_3 \quad i_2 \sqsubseteq i_3 \quad acc^\sqsubseteq$

$i_1 :: i_3 :: i_2 :: acc \sqsubseteq i_1 :: i_2 :: acc$

$Acc_F-\sqsubseteq$-DOWN

$i_1 \sqsubseteq i_2 \quad acc^\sqsubseteq$

$i_1 :: i_2 :: acc \sqsubseteq i_2 :: acc$

$Acc_F-\sqsubseteq$-UP

$i_1 \sqsubseteq i_2 \quad acc^\sqsubseteq$

$i_1 :: acc \sqsubseteq i_2 :: i_1 :: acc$

$Acc_F-\sqsubseteq$-TRANS

$acc_1 \sqsubseteq acc_2 \quad acc_2 \sqsubseteq acc_3$

$acc_1 \sqsubseteq acc_3$

Meet accumulator $Acc_M$

$Acc_M^p \triangleq \text{zero} \mid \text{two } Idx_M^p \text{ Idx}_M^p$

$1_M^p = \text{zero}$

$i \otimes_M \text{zero} \quad = \text{two } i i$

$i \otimes_M (\text{two } i' i'') = \text{two } i (i \sqcap i'')$

$s_M^p \text{zero} \quad = []$

$s_M^p (\text{two } i i') = [i, i']$

$Acc_M-\sqsubseteq$-zero

zero $\sqsubseteq$ zero

$Acc_M-\sqsubseteq$-two

two $i_1 \ i_2 \sqsubseteq \text{two } i'_1 \ i'_2 \rightsquigarrow i_1 \sqsubseteq i'_1 \wedge i_2 \sqsubseteq i'_2$

Forgetful accumulator $Acc_U$

$Acc_U^p \triangleq \text{option } Idx^p$

$1_U^p = \text{none}$

$i \otimes_U acc = \text{some } i$

$s_U^p \text{none} \quad = []$

$s_U^p (\text{some } i) = [i]$

$Acc_U-\sqsubseteq$-none

none $\sqsubseteq$ none

$Acc_U-\sqsubseteq$-some

some $i \sqsubseteq$ some $i' \rightsquigarrow i \sqsubseteq i'$

<caption>Fig. 6. Instances of index accumulators</caption>

accumulated index, irrespective of the previous state of the accumulator. The section $S_{Acc_U}$ maps none to the empty list and some to a singleton list. The precision only needs to make none and some self-precise ($Acc_U-\sqsubseteq$-none and $Acc_U-\sqsubseteq$-some).

The forgetful index accumulator serves as a space optimization of the free index accumulator, although a really imprecise one. Since intermediate casts are ignored, computations will succeed as long as the most external cast is valid, allowing a program to recover from invalid states.

## 5.3 Static and Dynamic Semantics

In the subsequent sections, we detail the semantics of PUNK for a fixed inductive family $\mathbb{I}$ with respect to a chosen listable index accumulator **Acc**. The typing and reduction rules for PUNK, presented in Figure 7, are derived from the rules for indexed inductive types in CIC with a few adjustments to account for index accumulators. We reuse the metafunctions from the static semantics of indexed inductive types (Figure 3).

Typing. Constructors (**GI**-CTOR) now hold additionally an index accumulator *acc* of type **Acc** and their indices are computed using *get* on said accumulator using the original index of the constructor
Head, Whnf□, head : Whnf□ → Head

Head ::= ... | I

Whnf□ ::= ... | I pi

head (I pi) := I

Γ ⊢ t : T

GI-TY

Γ ⊢ p : Param
Γ ⊢ i : Idx<sup>p</sup>
---
Γ ⊢ I pi : □<sub>ℓ</sub>

GI-ERR

Γ ⊢ p : Param
Γ ⊢ i : Idx<sup>p</sup>
---
Γ ⊢ err<sub>I pi</sub> : I pi

GI-UNK

Γ ⊢ p : Param
Γ ⊢ i : Idx<sup>p</sup>
---
Γ ⊢ ?<sub>I pi</sub> : I pi

GI-CTOR

Γ ⊢ p : Param
Γ ⊢ a : Arg<sub>c</sub><sup>p</sup>
---
Γ ⊢ acc : Acc<sup>p</sup>
∀ j < #indargs<sub>c</sub>, Γ ⊢ r<sub>j</sub> : Π(x<sub>j</sub> : IndArg<sub>c,j</sub><sup>p</sup> a), I p (arg_idx<sub>c,j</sub><sup>p</sup> ax<sub>j</sub>)
---
Γ ⊢ c<sup>p</sup> acc a ⃗r<sub>j</sub> : I p (get<sup>p</sup> (ctr_idx<sub>c</sub><sup>p</sup> a) acc)

GI-CATCH

Γ ⊢ p : Param
Γ ⊢ M : Π(i : Idx<sup>p</sup>), I pi → □<sub>ℓ'</sub>
Γ ⊢ i : Idx<sup>p</sup>
Γ ⊢ t : I pi
---
Γ ⊢ h<sub>err</sub> : Π(i : Idx<sup>p</sup>), M i err<sub>I pi</sub>
Γ ⊢ h<sub>unk</sub> : Π(i : Idx<sup>p</sup>), M i ?<sub>I pi</sub>
∀ k < #ctors, Γ ⊢ h<sub>c<sub>k</sub></sub> : Branch<sub>c<sub>k</sub></sub><sup>p</sup> M
---
Γ ⊢ catch<sup>p</sup> M h<sub>c<sub>k</sub></sub> h<sub>err</sub> h<sub>unk</sub> i t : M i t

t ↦→ t

GI-CATCH-CTOR: catch<sup>p</sup> M h<sub>c<sub>k</sub></sub> h<sub>err</sub> h<sub>unk</sub> i (c<sup>p</sup> acc a ⃗r<sub>j</sub>) ↦→ ⟨M<sub>n</sub> ⇐ ... M<sub>0</sub>⟩ h<sub>c</sub> a ⃗r<sub>j</sub> t<sub>j</sub>

with [i, ..., i<sub>k</sub>, ... i<sub>1</sub>] ≜ s<sup>p</sup> acc

acc<sub>c</sub> ≜ Γ<sup>p</sup> [i<sub>k</sub>, ..., i<sub>1</sub>],

M<sub>k</sub> ≜ M i<sub>k</sub> (c<sup>p</sup> acc<sub>c</sub> a ⃗r<sub>j</sub>)

M<sub>n</sub> ≜ M i (c<sup>p</sup> acc a ⃗r<sub>j</sub>)

M<sub>0</sub> ≜ M (ctr_idx<sub>c</sub><sup>p</sup> a)

t<sub>j</sub> ≜ λ(x<sub>j</sub> : IndArg<sub>c,j</sub><sup>p</sup> a), catch<sup>p</sup> M h<sub>c<sub>k</sub></sub> h<sub>err</sub> h<sub>unk</sub> (arg_idx<sub>c,j</sub><sup>p</sup> ax<sub>j</sub>) (r<sub>j</sub> x<sub>j</sub>)

GI-CATCH-ERR: catch<sup>p</sup> M h<sub>c<sub>k</sub></sub> h<sub>err</sub> h<sub>unk</sub> i err<sub>I pi</sub> ↦→ h<sub>err</sub> i

GI-CATCH-UNK: catch<sup>p</sup> M h<sub>c<sub>k</sub></sub> h<sub>err</sub> h<sub>unk</sub> i ?<sub>I pi</sub> ↦→ h<sub>unk</sub> i

GI-CTOR-CAST: ⟨I p' i' ⇐ I pi⟩ c<sup>p</sup> acc a ⃗r<sub>j</sub> ↦→ c<sup>p'</sup> (i' ⊗ p' acc') a' ⃗r<sub>j</sub>

with a' ≜ ⟨Arg<sub>c</sub><sup>p'</sup> ⇐ Arg<sub>c</sub><sup>p</sup> a⟩

acc' ≜ ⟨Acc<sup>p'</sup> ⇐ Acc<sup>p</sup>⟩ (i ⊗ p acc)

r'<sub>j</sub> ≜ ⟨Π(x'<sub>j</sub> : IndArg<sub>c,j</sub><sup>p'</sup> a'), I p' (arg_idx<sub>c,j</sub><sup>p'</sup> a' x'<sub>j</sub>)⟩ = Π(x<sub>j</sub> : IndArg<sub>c,j</sub><sup>p</sup> a), I p (arg_idx<sub>c,j</sub><sup>p</sup> ax<sub>j</sub>)⟩ r<sub>j</sub>

GI-ERR-CAST: ⟨I p' i' ⇐ I pi⟩ err<sub>I pi</sub> ↦→ err<sub>I p' i'</sub>

GI-UNK-CAST: ⟨I p' i' ⇐ I pi⟩ ?<sub>I pi</sub> ↦→ ?<sub>I p' i'</sub>

GI-DEC-UP: ⟨?□ ⇐ I pi⟩ t ↦→ ⟨?□ ⇐ I ?<sub>Param</sub> i'⟩ ⟨I ?<sub>Param</sub> i' ⇐ I pi⟩ t

GI-DEC-DOWN: ⟨I pi ⇐ ?□⟩ t ↦→ ⟨I pi ⇐ I ?<sub>Param</sub> i'⟩ ⟨I ?<sub>Param</sub> i' ⇐ ?□⟩ t

GI-HEAD-ERR: ⟨X ⇐ I pi⟩ t ↦→ err<sub>X</sub> when X ∈ Whnf□ and I ≠ head X

EVALUATION CONTEXTS

C ::= ... | ⟨C ⇐ A⟩ t | ⟨B ⇐ A⟩ C | catch<sup>p</sup> M h<sub>c<sub>k</sub></sub> h<sub>err</sub> h<sub>unk</sub> i C

GRED-CONG

t ↦→ t'
---
C[t] ↦ C[t']

canonical t

canonical err<sub>I pi</sub>

canonical ?<sub>I pi</sub>

canonical c<sup>p</sup> acc a ⃗r<sub>j</sub>

<caption>Fig. 7. Typing and reduction rules for PUNK.</caption>
as default value. As with any gradual type, the exceptional terms `err` (`GI-ERR`) and `?` (`GI-UNK`) inhabit the inductive type for any valid instance of the parameters and indices. The eliminator `catch` (`GI-CATCH`) extends `elim` from CIC with two new branches, one for each exceptional term. Finally, the typing of indexed inductive types (`GI-TY`) remains unchanged.

**Reduction.** The canonical forms for an inductive family consist of constructors as in CIC, as well as both exceptional terms `?I<sub>p<sub>i</sub></sub>` and `errI<sub>p<sub>i</sub></sub>`. The crux of the dynamic semantics is concentrated in two reduction rules that describe how index accumulators are used to accumulate the indices of casts on constructors and how they are used when eliminating a constructor.

Casting a constructor (`GI-CTOR-CAST`) to the same inductive type, with possibly different parameters and indices, is performed as follows: First, the index accumulator `acc`, the non-inductive arguments `a`, and the inductive arguments $\overrightarrow{r_j}$ are cast so they now depend on the target parameter $p'$. Then, we add the target index $i'$ to the previously cast index accumulator using $\otimes$. Since parameters are uniform over an indexed inductive definition, they need to be processed differently from indices. Treating parameters as indices would lead to a less useful elimination principle where the motive would have to abstract over parameters as well as indices. Casts propagate exceptional terms (`GI-ERR-CAST` and `GI-UNK-CAST`) adapting the indices and parameters on the fly. Casting a term of an inductive type to and from the unknown type `?\square` (`GI-DEC-UP` and `GI-DEC-DOWN`) is decomposed into two casts, going through $\mathbb{I} ? \mathbb{P}_{\text{param}}$ ($\langle \text{Idx}^2 \rangle \Leftarrow \text{Idx}^1 \rangle i$), the most general type with $\mathbb{I}$ as the head constructor at the "same" index (cast to the correct type). Although going through the most general index `?\text{Idx}^2 \text{Param}` would also work we prefer our system to be as precise as possible, while preserving graduality (Definition 3.3), and not lose precision if it is not required. Finally, casts from an indexed inductive type to a different indexed inductive type (e.g., $\langle a =_A b \Leftarrow \forall A n \rangle v$), a $\Pi$ type, or a universe always fail (`GI-HEAD-ERR`). Following GRIP, we present this reduction rule using an auxilliary function head computing the head type former of a type in weak head normal form (e.g., head ($\forall A n$) = $\forall$). This complete the description of reduction on casts, and we now focus on the reduction on `catch`.

Elimination of constructors using `catch` (`GI-CATCH-CTOR`) is more involved since we need to describe how to handle the casts accumulated in the index accumulator. At a high level, the rule propagates casts to the outside of the `catch` using the list of indices to construct the target of each cast and applies the corresponding branch as if the accumulator was empty. To facilitate the comprehension of the rule we present a detailed step-by-step description of how this reduction rule works:

(1) The branch corresponding to the constructor is applied ignoring the accumulator.

(2) The index accumulator `acc` is converted into a list of indices `s acc` from which we compute a sequence `[acc_n, ..., acc_1]` of partial accumulators using $\otimes$ starting from $\mathbb{1}$; in particular, $acc_n \triangleq \mathbb{I}^p(s acc)$.

(3) The intermediate cast types are then defined as $M_k \triangleq M(\mathit{get}^p(\mathit{ctr\_idx}_c^p a) acc_k) (c^p acc_k a \overrightarrow{r_j})$.

(4) Finally, the right hand side of the reduction rule consists of $n$ casts on the result of applying the correct branch (step 1), passing through each intermediate target $M_k$ in order, and ending with the motive $M$ applied to the eliminated term $c^p acc a \overrightarrow{r_j}$ and its index $i$.

When the index accumulator is empty, this rule is equivalent to the reduction for `elim` on constructors (`I-ELIM-CTOR` in Figure 5).

The interaction of `catch` on exceptional terms uses the corresponding premises (respectively $h_{err}$ in `GI-CATCH-ERR` and $h_{unk}$ for `GI-CATCH-UNK`). Finally, we have some congruence rules in order for terms eliminated using `catch` reduce until canonical forms.
<figure><img src="image_10.png" /><figcaption>Fig. 8. Precision for indexed inductive types.</figcaption></figure>

## 5.4 Precision

Now, we turn our focus to the definition of precision for gradual indexed inductive types (Figure 8). Precision for telescopes is defined as pairwise precision. Indexed inductive types and their constructors are monotonous. Therefore, two indexed inductive types are related by precision exactly when they have the same head and their parameters and indices are also related (I-CONG-TY). The exceptional types err□ and ?□ are the bottom and top elements respectively for self-precise indexed inductive types (err-I-CONG-TY and ?-I-CONG-TY). Indexed inductive types are never related to types with a different head constructor (NoCONF-I-UP-TY and NoCONF-I-DOWN-TY). Two constructors are related by precision exactly when they are the same constructor and their arguments are pairwise precise (I-CONC). As expected, the exceptional terms err and ? serve as the bottom and top elements respectively for self-precise terms (err-I-CONC and ?-I-CONC) and self-precise parameters and indices. Also, for each pair of different constructors $c_j$ and $c_k$ where $j \neq k$ there is a no confusion rule (NoCONF-C) stating that different constructors are never related by precision.

## 6 Metatheory of Punk

This section establishes the main metatheoretical properties of the PUNK framework: subject reduction, conservativity over CIC (§6.1) and graduality (§6.2). These properties hold for any choice of a listable index accumulator, hence for all the gradual indexed inductive types defined using the instances of §5.2. Section §6.3 then shows that these different instances of index accumulator exhibit the three possible behavior of eliminators with respect to precision.

### 6.1 Basic Metatheory of the PUNK Framework

As an extension of GRIP [Maillard et al. 2022] with comprehensive support for indexed inductive types, PUNK preserves two important properties as a gradual dependently-typed programming
language: subject reduction and conservativity with respect to CIC. Throughout the section, we focus on the fragment specific to indexed inductive types and rely on the established metatheory of GRIP when needed. We center the discussion towards the properties of constructors, sidelining exceptional terms, as focusing on these properties highlights the nuanced insights that have guided the design choices of PUNK's formalization (§5). For brevity, this section presents definitions and theorems in an empty context, focusing on a generic inductive family $\mathbb{I}: \Pi(p: \mathbf{Param})$, $\mathbf{Idx}^p \to \Box_\ell$, for any choice of a listable index accumulator **Acc**.

*Conversion for inductive families.* Conversion is defined in terms of reduction and syntactic comparison of terms up to extensionality principles—proof irrelevance for strict propositions and $\eta$-rule for functions. Two terms $t$ and $u$ are convertible, noted $t \equiv u$, if both eventually reduce to two terms that are extensionally equal, noted $t =_\eta u$.

The notion of conversion is crucial in a dependently typed setting to support computation at the level of types.

$$ \frac{\substack{\text{CONV} \\ \Gamma \vdash t : T'} \qquad \Gamma \vdash T : \Box_\ell \qquad \Gamma \vdash T' \equiv T : \Box_\ell}}{\Gamma \vdash t : T} $$

Conversion and the conversion typing rule (CONV) play an important role in the proof of subject reduction. In particular the proof depends on the injectivity of the type constructor for indexed inductive types. With the definition of conversion based on reduction, injectivity of type constructors is easy to prove because there is no reduction rules applying to them and extensional equality is straightforwardly injective on type constructors.

Note that the definition of conversion using reduction however has the drawback that it does not immediately form an equivalence relation, and in particular transitivity is not for free. This property has been formally proven by Sozeau et al. [2019] for the type theory of the Coq proof assistant. The crux of the proof lies in the proof of confluence (Church-Rosser) of reduction together with a simulation lemma saying that extensional equality commutes with reduction. In PUNK, the reduction rules have been extended to guarantee that the technique used for the proof of confluence remains valid. The proof of confluence makes use of the auxiliary notion of one-step parallel reduction, noted $t \Rightarrow u$, which allows all available reductions to be performed in parallel in the same step. One-step parallel reduction satisfies the triangle lemma saying that for any term $t$, there exists an optimally reduced term $\rho(t)$ (that performs all possible reduction in parallel) such that $t \Rightarrow \rho(t)$ and for any $t \Rightarrow u$, $u \Rightarrow \rho(t)$. Confluence is then a direct consequence of this triangle lemma and the fact that parallel reduction entails reduction.

*Subject reduction.* We first prove that typing is preserved by reduction. The main two cases concern cast reduction on a constructor and elimination via catch.

**LEMMA 6.1 (SUBJECT REDUCTION FOR CASTS ON CONSTRUCTORS).** *Consider two indices $i_1, i_2$, a listable index accumulator **acc**, and arguments $a$ and $\vec{r}_j$. If $\Gamma \vdash \langle \mathbb{I} p_2, i_2 \rightleftharpoons \mathbb{I} p_1, i_1 \rangle \mathcal{C}^{p_1} \text{acc} a \vec{r}_j : \mathbb{I} p_2, i_2$, then*

$$ \vdash \mathcal{C}^{p_2} (i_2 \otimes \text{acc}') a' (\langle T_j \Leftarrow C_j \rangle \vec{r}_j) : \mathbb{I} p_2, i_2 $$

where $\forall j. T_j \triangleq \Pi(x_j : \text{IndArg}_{c,j}^{p_2} a')$, $\mathbb{I} p (\text{arg\_idx}_{c,j}^{p_2} a' x_j)$, $a' \triangleq \langle \text{Arg}_{c}^{p_2} \Leftarrow B \rangle a$, and $\text{acc}' \triangleq \langle \text{Acc}^{p_2} \Leftarrow A \rangle (i_1 \otimes \text{acc})$, for some terms A, B, and $\forall j. C_j$.

**PROOF.** By repeated inversion on the typing derivation of $\langle \mathbb{I} p_2, i_2 \Leftarrow \mathbb{I} p_1, i_1 \rangle \mathcal{C}^{p_1} \text{acc} a \vec{r}_j$, we know that $i_1 : \mathbf{Idx}^{p_1}$ and $i_2 : \mathbf{Idx}^{p_2}$, and $\mathcal{C}^{p_1} \text{acc} a \vec{r}_j : \mathbb{I} p_1, i_1$. First, we have to show

$$ \mathbb{I} p_2 \text{get}^{p_2} (\text{ctr\_idx}_{c}^{p_2} a') (i_2 \otimes \text{acc}') \equiv \mathbb{I} p_2, i_2. $$
This equation is given by the injectivity of the type constructor $\mathbb{I}$, the definition of **get**, and the partial preservation of the action by $\mathfrak{s}$ (Equation (5)). Then, by inversion on the typing derivation of $c^{p_1} acc \overrightarrow{a r_j} : \mathbb{I} p_1 i_1$, and the rules for conversion (**CONV**) and typing of constructors (**GI-CTOR**), we have **acc'**: A, a: B, and $\forall j. r_j: C_j$. Finally, by typing of constructors (**GI-CTOR**), we have to show

$$i_2 \otimes \text{acc'} : \text{Acc}^{p_2} \qquad a' : \text{Arg}_c^{p_2} \qquad \forall j. \langle T_j \leftarrow C_j \rangle \overrightarrow{r_j} : T_j.$$

These typing judgments follow directly from the typing rule of casts (§2.1). □

**LEMMA 6.2 (SUBJECT REDUCTION FOR CATCH ON CONSTRUCTORS).** *Consider a parameter $p$; a motive $M$; branches $\overrightarrow{pC_k}$, $h_{err}$, and $h_{unk}$; an index $i$; a listable index accumulator $acc$; and arguments $a$ and $\overrightarrow{r_j}$.*

If $\vdash \text{catch}^p M \overrightarrow{h_c} h_{err} h_{unk} i (c^p \text{acc} \overrightarrow{a r_j}) : M i (c^p \text{acc} \overrightarrow{a r_j})$, then

$$\vdash \langle M i (c^p \text{acc} \overrightarrow{a r_j}) \rangle \equiv \dots \langle M (\text{ctr\_idx}_c^p a) (c^p \mathbb{1}^p \overrightarrow{a r_j}) \rangle h_c \overrightarrow{r_j} \overrightarrow{t_j} : M i (c^p \text{acc} \overrightarrow{a r_j}).$$

*PROOF.* By inversion on the typing rule of catch (**GI-CATCH**) we know,

$$p : \text{Param} \qquad h_c : \text{Branch}_c^p M \qquad M : \Pi(i' : \text{IDX}^p), \mathbb{I} p i' \to \Box \qquad c^p \text{acc} \overrightarrow{a r_j} : \mathbb{I} p i.$$

Then, we have to show that (a) the outermost target is well-typed and that (b) the method application is well-typed to the source type. (a) follows directly from the type of $M$, $i$, and $c^p \text{acc} \overrightarrow{a r_j}$; (b) by the conversion rule (**CONV**) and the typing rule for constructors (**GI-CTOR**), we have to show, between some typing premises, that $\mathbb{I} p (\text{get}^p (\text{ctr\_idx}_c^p a) \mathbb{1}^p) \equiv \mathbb{I} p (\text{ctr\_idx}_c^p a)$, which is given directly by the injectivity of the type constructor $\mathbb{I}$, the definition of **get**, and the preservation of the empty element by $\mathfrak{s}$ (Eq. (4)). The rest of the premises are given by the inversion of the hypothesis. □

**THEOREM 6.3 (SUBJECT REDUCTION FOR PUNK).** *If $\vdash T : \Box_{t'}$, $\vdash t : T$ and $t \rightsquigarrow t'$ for some $t'$, then $\vdash t' : T' \text{ for some } \vdash T' : \Box_{t'}$ such that $\vdash T \equiv T'$. *

*PROOF.* The proof proceeds by induction on $t \rightsquigarrow t'$. The cases for casts (**GI-CTOR-CAST**) and catch (**GI-CATCH-CTOR**) on constructors follow directly from Lemmas 6.1 and 6.2. Cases for casts and catch on exceptional terms follow directly from the typing rules. The rest of the cases are given by the induction hypothesis, the typing rules, and the subject reduction of GRIP. □

*Conservativity with respect to CIC.* Since PUNK extends the syntax of constructors and even uses a different eliminator than the static language presented in §4, we cannot reuse CASTCIC's *static term* definition (i.e., a term of CASTCIC that it is also a term of CIC) and need to give a specific translation (noted $\llbracket \cdot \rrbracket$) from CIC to PUNK for indexed inductive types, constructors and applications of catch:

$$\llbracket \mathbb{I} p i \rrbracket \triangleq \mathbb{I} \llbracket p \rrbracket \llbracket i \rrbracket \qquad \llbracket c^p a \overrightarrow{r} \rrbracket \triangleq c^{[p]} \mathbb{1}^{[p]} \llbracket a \rrbracket \overrightarrow{[r]} \qquad \llbracket \text{elim}^p M \overrightarrow{h_c} i t \rrbracket \triangleq \text{catch}^{[p]} \llbracket M \rrbracket (\lambda i'. \text{err}_{[M]} i' \text{ err}_{[1][p]i'}) (\lambda i'.?_{[M]} i' ?_{\mathbb{I} [p] i'}) \overrightarrow{[h_c]} \llbracket i \rrbracket \llbracket t \rrbracket$$

**THEOREM 6.4 (CONSERVATIVITY OF PUNK OVER CIC).** *For any term $t$ and type $T$ of CIC, if $\vdash_{CIC} t : T$ then $\vdash \llbracket t \rrbracket : \llbracket T \rrbracket$.*

*PROOF.* By induction on the typing derivation of $\vdash_{CIC} t : T$. The case for constructors follows from Equation (4). The case for catch is direct by the translation. □
## 6.2 Gradual Properties of PUNK

An inductive family designed within the PUNK framework adheres to all the characteristics of a gradual inductive family outlined in §3.2, specifically *graduality*, as well as *index relevance* and *shape relevance*. Similarly to §6.1, we focus on the fragment specific to indexed inductive types, particularly to the case of constructors. We state definitions and theorems in the empty context, in terms of a generic inductive family $\mathbb{I}$, and for any choice of index accumulator **Acc**.

*Graduality for Inductive Families.* We now prove graduality for inductive families, i.e., inductive families are monotone with respect to precision. More precisely, we prove that up-casting and down-casting the parameters and indices of an indexed inductive type form an embedding-projection pair with respect to precision [New and Ahmed 2018], i.e., satisfy the three following properties: (1) casts have to be monotone; (2) casting to a less precise type and back is the identity up to equiprecision (unit of the Galois connection and retraction condition); (3) casting to a more precise type and back increases precision (count of the galois connection). We state these properties for a fixed parameter *p* and only on constructors where the most important features of PUNK are apparent.

**LEMMA 6.5 (GRADUALITY FOR CONSTRUCTORS).** Let $p: \mathbf{Param}$ be a self-precise parameter, $i_1, i_2: \mathbf{Index}^p$, acc: **Acc**^p a self-precise index accumulator, and self-precise arguments a: $\mathbf{Arg}_e^p$ and $\mathbf{r}_j$, such that $\vdash \mathbf{C}^p \mathbf{acc} a \mathbf{r}_j: \mathbb{I} p i_1$. Then, the following precision relations hold

$$ 
\begin{align*}
i_1 \mathbf{Index}^p \sqsubseteq \mathbf{Index}^p & \quad i_2 \rightarrow \mathbf{C}^p \mathbf{acc} a \mathbf{r}_j \sqsupseteq \mathbb{I} p i_1 \\
i_2 \mathbf{Index}^p \sqsubseteq \mathbf{Index}^p & \quad i_1 \rightarrow \langle \mathbb{I} p i_1 \leftarrow \mathbb{I} p i_2 \leftarrow \mathbb{I} p i_1 \rangle \mathbf{C}^p \mathbf{acc} a \mathbf{r}_j \\
& \quad \mathbb{I} p i_1 \sqsubseteq \mathbb{I} p i_1 \mathbf{C}^p \mathbf{acc} a \mathbf{r}_j
\end{align*}
$$

**PROOF.** By reduction of cast on constructors (II-CCTOR-CAST), and removing the identity casts that appears (which is valid up-to equiprecision), we have

$$ \langle \mathbb{I} p i_1 \leftarrow \mathbb{I} p i_2 \leftarrow \mathbb{I} p i_1 \rangle \mathbf{C}^p \mathbf{acc} a \mathbf{r}_j \rightsquigarrow \mathbf{C}^p (i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc}) a \mathbf{r}_j $$

By the definition of precision on constructors (II-□-C), we have to show (omitting type annotation of precision for readability)

$$ i_1 \sqsubseteq i_2 \rightarrow \begin{array}{l} i_1 \otimes \mathbf{acc} \sqsubseteq i_1 \otimes i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc} \\ i_1 \otimes i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc} \sqsubseteq i_1 \otimes \mathbf{acc} \end{array} \wedge a \sqsupseteq a \wedge \bigwedge_j r_j \sqsupseteq r_j \wedge $$

$$ i_2 \sqsubseteq i_1 \rightarrow \begin{array}{l} i_1 \otimes i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc} \sqsubseteq i_1 \otimes \mathbf{acc} \\ \phantom{i_1 \otimes i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc} \sqsubseteq} \wedge a \sqsubseteq a \wedge \bigwedge_j r_j \sqsubseteq r_j. \end{array} $$

Then the first precision between accumulators $i_1 \otimes \mathbf{acc} \sqsubseteq i_1 \otimes i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc}$ follows from repeated applications of Equations (2) and (3), using that $i_1 \sqsubseteq i_2$, quasi-reflexivity of precision and self-precision of acc. The second precision between accumulators $i_1 \otimes i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc} \sqsubseteq i_1 \otimes \mathbf{acc}$ follows the same pattern but uses Equations (1) and (3) instead. The third precision between accumulators $i_1 \otimes i_1 \otimes i_2 \otimes i_2 \otimes i_1 \otimes \mathbf{acc} \sqsubseteq i_1 \otimes \mathbf{acc}$ also follows the same pattern but uses Equations (2) and (3) and $i_2 \sqsubseteq i_1$, instead. The other precisions are given by self-precision hypothesis. $\square$

Now we have everything we need to prove graduality for inductive families;

**THEOREM 6.6 (GRADUALITY FOR INDUCTIVE FAMILIES).** Consider two indices $i_1, i_2: \mathbf{Index}^p$. If $i_1 \sqsubseteq i_2$, then $\langle \mathbb{I} p i_2 \leftarrow \mathbb{I} p i_1 \rangle \leftarrow \langle \mathbb{I} p i_1 \leftarrow \mathbb{I} p i_2 \rangle$ form an embedding projection pair.

**PROOF.** It follows from the definition of precision on constructors (II-□-C), monotonicity of $\otimes$, and Lemma 6.5. $\square$

*Criteria for gradual indexed families.* As we discussed in §3.2, a correct treatment of gradual indexed inductive types must satisfy two properties: index relevance and shape relevance. These properties ensure that the index and shape of an inductive family are respected.
An indexed inductive type is index relevant when precision-related instances of an inductive imply relatedness of the indices.

**THEOREM 6.7 (INDEX RELEVANCE FOR INDUCTIVE FAMILIES).** Consider a parameter $p$, and two indices $i_1, i_2 : \mathbf{Idx}^p$. If $\mathbb{I} p i_1 \sqsubseteq_{\ell} \mathbb{I} p i_2$, then $i_1 \mathbf{Idx}^{p_1} \sqsubseteq_{\ell} \mathbf{Idx}^{p_2} i_2$.

*PROOF.* By the definition of precision for indexed inductive types. □

We establish that PUNK's gradual indexed inductive types are shape relevant, i.e., they are only related by precision to indexed inductive types of the same family and to the exceptional types.

**THEOREM 6.8 (SHAPE RELEVANCE FOR INDUCTIVE FAMILIES).** Assuming weak-head normalization of types in PUNK. Consider a parameter $p : \mathbf{Param}$, an index $i : \mathbf{Idx}^p$, and a type $T : \Box_{\ell}$.

$$ (T \sqsubseteq_{\ell} \mathbb{I} p i \rightarrow (T = \mathrm{err}\Box) \lor \exists (p' : \mathbf{Param})(i' : \mathbf{Idx}^{p'}). T = \mathbb{I} p' i') \\ \land \quad (\mathbb{I} p i \sqsubseteq_{\ell} T \rightarrow (T = ?\Box) \lor \exists (p' : \mathbf{Param})(i' : \mathbf{Idx}^{p'}). T = \mathbb{I} p' i') $$

*PROOF.* By the normalization assumption, we have that $T$ reduces to $T' \in \mathbf{Whnf}_{\Box}$. Then, the result is given by analysis on head $T'$ and the rules for type precision of inductive families in Figure 8. □

Having discussed the general properties of PUNK, we now turn our focus to properties specific to an index accumulator and indexed inductive types that uses them.

## 6.3 Characterizing Gradual Inductive Families

As we saw in §3, we can characterize gradual indexed inductive definitions by how casts commute with the catch eliminator up to precision. The asymmetry of the precision relation yield three cases of interest, each one potentially corresponding to a different class of inductive definitions. We show that each of the three classes arise from an index accumulator instance among those presented in §5.2.

The definitions and theorems in the rest of this section expect a monotone use of catch, therefore, we explicit all the assumptions here to avoid repeating them every time. Consider an inductive family $\mathbb{I} : \Pi(p : \mathbf{Param})$, $\mathbf{Idx}^p \to \Box$; a parameter $p : \mathbf{Param}$; a motive $M : \Pi(i : \mathbf{Idx}^p)$, $\mathbb{I} p i \to \Box$; two indices $i_1, i_2 : \mathbf{Idx}^p$; branches $\overrightarrow{h_{c_k}}$, $h_{err}$ and $h_{unk}$; and term $t : \mathbb{I} p i_1$. All self-precise and if $h_{err} \sqsubseteq_{\ell} h_{c_k} \sqsubseteq_{\ell} h_{unk}$ for all $k$. We do not fix the index accumulator since we will use a different one for each theorem. You can find the full theorems and more detailed proves in the appendix.

*Definition 6.9 (Equiprecise elimination).* An inductive family $\mathbb{I}$ satisfies equiprecise elimination if precision is preserved when casts are propagated outside of the eliminator:

$$ \langle Mp(\langle \mathbb{I} p i_2 \equiv \mathbb{I} p i_1 \rangle t) \equiv Mp t \rangle \text{catch}^p M \overrightarrow{h_{c_k}} h_{err} h_{unk} i_1 t \quad \Box \quad \text{catch}^p M \overrightarrow{h_{c_k}} h_{err} h_{unk} i_2 (\langle \mathbb{I} p i_2 \equiv \mathbb{I} p i_1 \rangle t) $$

An example of an inductive family that satisfies equiprecise elimination is the free inductive family $\mathbb{I}_F$ using the initial index accumulator $\mathbf{Acc}_F$ (§5.1).

**THEOREM 6.10 (FREE INDUCTIVES SATISFY EQUIPRECISE ELIMINATION).**

$$ \langle Mp(\langle \mathbb{I}_F p i_2 \equiv \mathbb{I}_F p i_1 \rangle t) \equiv Mp t \rangle \text{catch}^p_{\mathbb{I}_F} M \overrightarrow{h_{c_k}} h_{err} h_{unk} i_1 t \quad \mathbf{=\Box} \quad \text{catch}^p_{\mathbb{I}_F} M \overrightarrow{h_{c_k}} h_{err} h_{unk} i_2 (\langle \mathbb{I}_F p i_2 \equiv \mathbb{I}_F p i_1 \rangle t) $$

*PROOF.* By induction on the typing derivation of $t$. The exceptional cases follow from the hypothesis and the reduction of cast on exceptions. The case of constructors is given by reduction of cast on constructors and the fact that $\mathbb{I}$ is the identity for list. □
**Definition 6.11 (Over-precise elimination).** An inductive family $\mathbb{I}$ satisfies overprecise elimination if precision increases when casts are propagated outside of the eliminator.

$$ \langle Mp(\langle \mathbb{I} p i_2 \equiv \mathbb{I} p i_1 \rangle t) \equiv Mp t \rangle \text{catch}^p M \overrightarrow{h_{err}} h_{unk} i_1 t \quad \Box \quad \text{catch}^p M \overrightarrow{h_{err}} h_{unk} i_2 (\langle \mathbb{I} p i_2 \equiv \mathbb{I} p i_1 \rangle t) $$

An example of an inductive family that satisfies underprecise elimination is the forgetful inductive family $\mathbb{I}_U$ using the index accumulator $\mathbf{Acc}_U^p$ from §5.2.

**THEOREM 6.12 (FORGETFUL INDUCTIVES SATISFY OVERPRECISE ELIMINATION).**

$$ \langle Mp \langle \mathbb{I}_U p i_2 \equiv \mathbb{I}_U p i_1 \rangle t \equiv Mp t \rangle \text{catch}^p_{\mathbb{I}_U} M \overrightarrow{h_{err}} h_{unk} i_1 t \quad \Box \quad \text{catch}^p_{\mathbb{I}_U} M \overrightarrow{h_{err}} h_{unk} i_2 (\langle \mathbb{I}_U p i_2 \equiv \mathbb{I}_U p i_1 \rangle t). $$

**PROOF.** By induction on the typing derivation of $t$. The exceptional cases follow from the hypothesis and the reduction of cast on exceptions. The case of constructors goes by induction on the index accumulator *acc*. If (*acc* = none), then the result follows from the self-precision hypotheses. On the other hand, if (*acc* = some *i*'), by reduction of catch on constructors, we have to show

$$ \begin{align*} \langle M i_2 (c^p (\text{some } i_2) a \overrightarrow{r_j}) \rangle &\equiv M i_1 (c^p (\text{some } i_1) a \overrightarrow{r_j}) \equiv M (\text{ctr\_idx}_c^p a) (c^p (\text{none } a \overrightarrow{r_j})) t' \\ \Box \quad \langle M i_2 (c^p (\text{some } i_2) a \overrightarrow{r_j}) \rangle &\equiv M (\text{ctr\_idx}_c^p a) (c^p (\text{none } a \overrightarrow{r_j})) t' \end{align*} $$

where $t' \triangleq \text{catch}_{\mathbb{I}_U}^p M \overrightarrow{h_{err}} h_{unk} (\text{ctr\_idx}_c^p a) (c^p (\text{none } a \overrightarrow{r_j}))$. Which is given by cast decomposition, counit, and self-precision of hypotheses. $\square$

**Definition 6.13 (Under-precise elimination).** An inductive family $\mathbb{I}$ satisfies underprecise elimination if precision decreases when casts are propagated outside of the eliminator.

$$ \langle Mp(\langle \mathbb{I} p i_2 \equiv \mathbb{I} p i_1 \rangle t) \equiv Mp t \rangle \text{catch}^p M \overrightarrow{h_{err}} h_{unk} i_1 t \quad \Box \quad \text{catch}^p M \overrightarrow{h_{err}} h_{unk} i_2 (\langle \mathbb{I} p i_2 \equiv \mathbb{I} p i_1 \rangle t) $$

An example of an inductive family that satisfies underprecise elimination is the forgetful inductive family $\mathbb{I}_M$ using the index accumulator $\mathbf{Acc}_M^p$ from §5.2.

**THEOREM 6.14 (MEET INDUCTIVES SATISFY UNDERPRECISE ELIMINATION).**

$$ \text{catch}_{\mathbb{I}_M}^p M \overrightarrow{h_{err}} h_{unk} i_2 (\langle \mathbb{I}_M p i_2 \equiv \mathbb{I}_M p i_1 \rangle t). \quad \Box \quad \langle Mp \langle \mathbb{I}_M p i_2 \equiv \mathbb{I}_M p i_1 \rangle t \equiv Mp t \rangle \text{catch}_{\mathbb{I}_M}^p M \overrightarrow{h_{err}} h_{unk} i_1 t $$

**PROOF.** By induction on the typing derivation of $t \overset{\Box}{\equiv} p i$. The exceptional cases follow from the hypothesis and the reduction of cast on exceptions. The case for constructors, follows by induction on the index accumulator *acc*. For (*acc* = zero), the result is given by retraction and self-precision of *M*. If (*acc* = two $i_1 i'$), it is given by precision rule $\mathbf{Acc}_M^p$ ($\mathbf{Acc}_M^p$-two) and properties of the meet index accumulator. $\square$

# 7 Related Work

Having given a formal presentation of PUNK we can now revisit in more detail the comparison with previous approaches discussed in §2.3. Then, we briefly discuss the related work regarding effectful and gradual dependent types (§7.2 and §7.3).

## 7.1 Previous Approaches to Gradual Indexed Inductive Types

GCIC. Lennon-Bertrand et al. [2022] present an implementation of vectors for GCIC where casts are eagerly reduced and casting constructors to the unknown index is internalized as a new constructor. In particular, casting a constructor to an incompatible index immediately fails in GCIC:

$$ \langle \mathbb{V} B(Sn) \equiv \mathbb{V} A 0 \rangle \text{nil} \rightsquigarrow_{\text{GCIC}} \text{err}_{\mathbb{V} B(Sn)} $$
This behavior cannot be encoded in PUNK, because cast reduction always preserves the head constructor, regardless of the choice of index accumulator. For example, the cast reduction rule for constructors (GI-CTOR-CAST) can be instantiated to the nil constructor for V as

$$ \langle V B n \leftarrow V A m \rangle \text{nil acc} \rightsquigarrow \text{nil } (n \otimes (\langle \text{Acc}^B \rightleftharpoons \text{Acc}^A \rangle m \otimes acc)). $$

Note that the reduction only updates the index accumulator, so casting nil always reduces to nil, and cannot fail; errors only appear on elimination with catch. This difference is justified by the fact that matching on the index of the target of a cast is not possible in general (e.g., when the index is a function or a type). Indeed, the authors informally argue that this approach generalizes to other inductive families as long as their indices are forceable [Brady et al. 2004]. This in particular leaves out propositional equality, discussed next. As a general framework for the definition of indexed inductive types, PUNK's cast reduction semantics must accommodate indices of any type.

GEq. Eremondi et al. [2022] develop GEq, an extension of GCIC with a type former for propositional equality ($t_1 =_T^{GEq} t_2$) inhabited by $refl_{t_w \vdash t_1 \cong t_2}^{GEq}$, which holds a witness terms $t_w$ more precise than both $t_1$ and $t_2$. The typing rule for refl (CASTREFL) is defined using bidirectional typing, following Lennon-Bertrand et al. [2022], and the precision judgment $\Gamma | \Gamma' \vdash t \sqsubseteq \bar{t}'$, which states that $t$ is more precise than $t'$ up-to conversion, with $t$ and $t'$ well-typed in contexts $\Gamma$ and $\Gamma'$ respectively:

$$ \frac{\Gamma \vdash t_w \Rightarrow T \qquad \Gamma \vdash t_1 \Leftarrow T \qquad \Gamma \vdash t_2 \Leftarrow T \qquad \Gamma | \Gamma \vdash t_w \sqsubseteq \bar{t}_1 \qquad \Gamma | \Gamma \vdash t_w \sqsubseteq \bar{t}_2}{\Gamma \vdash refl_{t_w \vdash t_1 \cong t_2}^{GEq} \Rightarrow t_1 =_T^{GEq} t_2} $$

Instead of a general catch, propositional equality in GEq is equipped with a custom eliminator $J(M, t_1, t_2, t_{M1}, t)$ that, given an equality $t$ with type $t_1 =_T^{GEq} t_2$, transforms a term $t_{M1}$ of type $M t_1$ into one of type $M t_2$. Similarly to meet indexed inductive types in PUNK, casts in GEq accumulate the meet of the source and target indices (REDCASTEQ) and elimination propagates the casts to the outside (REDJ):

$$ \text{REDCASTEQ: } \langle t'_1 =_{T'}^{GEq} t'_2 \Leftarrow t_1 =_T^{GEq} t_2 \rangle \text{refl}_{t_w \vdash t_1 \cong t_2}^{GEq} \rightsquigarrow \text{GEq refl}_{(\langle T' \Leftarrow T \rangle t_w \sqcap t'_1 \sqcap t'_2) \vdash t'_1 \cong t'_2}^{GEq} $$

$$ \text{REDJ: } J(M, t_1, t_2, t_{M1}, \text{refl}_{t_w \vdash t_1 \cong t_2}^{GEq}) \rightsquigarrow \text{GEq} \langle M t_2 \Leftarrow M t_w \rangle \langle M t_w \Leftarrow M t_1 \rangle t_{M1} $$

We can encode the J eliminator in PUNK as $J_{PUNK}$ which satisfies the REDJ reduction rule:

$$ \lambda T \cdot J_{PUNK}(M, t_1, t_2, t_{M1}, t) \triangleq \text{catch}^{T, t_1} M (\lambda t'_2. \langle M t'_2 \Leftarrow M t_1 \rangle t_{M1}) (\lambda t'_2. \langle M t'_2 \Leftarrow M t_1 \rangle t_{M1}) t_{M1} t_2 t $$

But, in contrast to PUNK, GEq conflates exceptions with refl, the only canonical inhabitant of equality (PROPEQUNK and PROPEQERR):

$$ \text{PROPEQUNK: } ?_{t_1 =_T^{GEq} t_2} \rightsquigarrow \text{GEq refl}_{t_1 \sqcap t_2 \vdash t_1 \cong t_2}^{GEq} \qquad \text{PROPEQERR: } \text{err}_{t_1 =_T^{GEq} t_2} \rightsquigarrow \text{GEq refl}_{\text{err}_T \vdash t_1 \cong t_2}^{GEq} $$

We observe that this construction is specific to propositional equality and cannot be generalized to inductive families with multiple constructors: in order to preserve err and ? as the bottom and top elements of the precision relation, supporting this behavior in general requires every pair of constructors to be related with each other.

Furthermore, because there is no notion of empty index accumulator, the embedding of CIC into GEq translates refl into $refl_{t \vdash t \cong t_1}^{GEq}$ which introduces extra identity casts. This means that a conservativity result over CIC (as in Theorem 6.4) would require an extra conversion rule for identity casts ($\langle A \Leftarrow A \rangle a \equiv a$); it is unclear how to achieve this in a gradual setting, although Pujet and Tabareau [2024] achieve this for observational equality.
Note that, as mentioned in §2.3, it is possible to use propositional equality to define indexed inductive types via fording. In fact, one can obtain a cast reduction semantics similar to that induced by a given index accumulator by using fording with a propositional equality with that index accumulator. A deeper and formal exploration of this connection is future work.

## 7.2 Effects in Dependent Type Theory

Gradual type systems rely on effects, in particular errors, to enforce dynamic typing invariants, a challenging aspect within type theory. Indeed, the Fire Triangle of Pédrot and Tabareau [2020] exhibit a strong tension between the metatheoretic properties of CIC, starting with logical consistency, and observable effects. Dependently typed programming languages featuring effectful computations either isolate dependencies to a fragment of pure expressions [Swamy et al. 2016; Xi and Pfenning 1998] or give up on some metatheoretical properties: Dependent Haskell [Eisenberg 2016], Trellys [Kimmell et al. 2012; Stump et al. 2010] and Zombie [Casinghino et al. 2014] which allow diverging type-level expressions either admit inconsistencies or undecidable typechecking. The recent work of Pédrot and Tabareau [2017, 2018] specifically consider exceptions in type theory, building up to RETT, a type theory exploiting universe hierarchies to separate effectful, inconsistent computations from pure, consistent proofs to reason about the effectful content [Pédrot et al. 2019].

## 7.3 Gradual Dependent Types

This work pursue a line of research in combining dependent types and dynamic type checking, as first explored by [Ou et al. 2004], more specifically following the gradual typing approach [Siek and Taha 2006; Siek et al. 2015a], and extending it to a full-blown dependent type theory. Ou et al. [2004] study a programming language with separate dependently- and simply-typed fragments, using arbitrary runtime checks at the boundary. The blame calculus of Wadler and Findler [2009] considers subset types on base types, where the refinement is an arbitrary term, as in hybrid type checking [Knowles and Flanagan 2010], but lacks dependent function types. Tanter and Tabareau [2015] provide casts for subset types with decidable properties in Coq, and Dagand et al. [2018] support dependent interoperability [Osera et al. 2012] in Coq. All these approaches lack the notion of precision that is central to gradual typing. Gradual refinement types [Lehmann and Tanter 2017] are an extension of liquid types [Rondon et al. 2008] with imprecise logical formulas, based on an SMT-decidable logic about base types. Eremondi et al. [2019] study the gradualization of CC, and propose approximate normalization to ensure decidable typechecking. Gradual inductive types only appear in GCIC [Lennon-Bertrand et al. 2022], and its follow up, GRIP [Maillard et al. 2022], upon which we build PUNK.

## 8 Conclusion

PUNK provides a general framework to define gradual indexed inductive families. As illustrated in §6.3, PUNK is able to explore the space of cast reduction semantics, providing adequate descriptions for different semantics of indexed inductive types in a unified way. Its expressivity stems from the use of a simple and algebraic notion of listable indexed accumulators taking, in a gradual setting, the role that would otherwise be filled by propositional equality in approaches of indexed inductive types using Fordism in CIC. This abstraction not only allows to prove the metatheory of the framework uniformly for all possible semantics of gradual indexed inductive types, but also open the way for programmers using gradual dependent types to choose the implementation of gradual indexed inductive types that best fit their need, arbitrating between space efficiency and precision of the dynamic typing constraint tracking.
References

Rastislav Bodík and Rupak Majumdar (Eds.). 2016. *Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016)*. ACM Press, St Petersburg, FL, USA. https://doi.org/10.1145/2837614

Edwin Brady. 2013. Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation. *Journal of Functional Programming* 23, 5 (Sept. 2013), 552–593.

Edwin Brady, Conor McBride, and James McKinna. 2004. *Types for Proofs and Programs*. Lecture Notes in Computer Science, Vol. 3085. Springer-Verlag, Chapter Inductive Families Need Not Store Their Indices, 115–129.

Ali Caglayan. 2021. https://github.com/HoTT/Coq-HoTT/blob/master/theories/Types/IWType.v

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014. Combining proofs and programs in a dependently typed language. In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014)*. ACM Press, San Diego, CA, USA, 671–684. https://doi.org/10.1145/2535838.2535883

Giuseppe Castagna (Ed.). 2009. *Proceedings of the 18th European Symposium on Programming Languages and Systems (ESOP 2009)*. Lecture Notes in Computer Science, Vol. 5502. Springer-Verlag, York, UK.

Adam Chlipala. 2013. *Certified Programming with Dependent Types*. MIT Press.

Pierre-Évariste Dagand, Nicolas Tabareau, and Éric Tanter. 2018. Foundations of Dependent Interoperability. *Journal of Functional Programming* 28 (2018), 9:1–9:44.

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In *Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction (Lecture Notes in Computer Science)*, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 378–388. https://doi.org/10.1007/978-3-319-21401-6_26

Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. arXiv:1610.07978 [cs.PL]

Joseph Eremondi, Ronald Garcia, and Éric Tanter. 2022. Propositional Equality for Gradual Dependently-Typed Programming. See [ICFP 2022 2022], 165–193.

Joseph Eremondi, Éric Tanter, and Ronald Garcia. 2019. Approximate Normalization for Gradual Dependent Types. See [ICFP 2019], 88:1–88:30.

Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing, See [Bodík and Majumdar 2016], 429–442. https://doi.org/10.1145/2837614 See erratum: https://www.cs.ubc.ca/rxg/agt-erratum.pdf.

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. Definitional Proof-Irrelevance without K. *Proceedings of the ACM on Programming Languages* 3, POPL (Jan. 2019), 1–28. https://doi.org/10.1145/3290316

Michael Greenberg. 2017. Space-Efficient Manifest Contracts. arXiv:1410.2813 [cs.PL] https://arxiv.org/abs/1410.2813

ICFP 2019. *Proceedings of the 24th ACM SIGPLAN Conference on Functional Programming (ICFP 2019)*. Vol. 3. ACM Press. ICFP 2022 2022.

Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and Ki Yung Ahn. 2012. Equational reasoning about programs with general recursion and call-by-value semantics. In *Proceedings of the 6th workshop on Programming Languages Meets Program Verification (PLPV 2012)*. ACM Press, 15–26. https://doi.org/10.1145/2103776.2103780

Kenneth Knowles and Cormac Flanagan. 2010. Hybrid type checking. *ACM Transactions on Programming Languages and Systems* 32, 2 (Jan. 2010), Article n.6. https://doi.org/10.1145/1111037.1111059

Nico Lehmann and Éric Tanter. 2017. Gradual Refinement Types. In *Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017)*. ACM Press, Paris, France, 775–788.

Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter. 2022. Gradualizing the Calculus of Inductive Constructions. *ACM Transactions on Programming Languages and Systems* 44, 2 (June 2022), 7:1–7:82.

Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, and Éric Tanter. 2022. A Reasonably Gradual Type Theory. See [ICFP 2022 2022], 931–959.

Per Martin-Löf. 1971. An Intuitionistic Theory of Types. Unpublished manuscript.

Conor McBride. 1999. *Dependently Typed Functional Programs and their Proofs*. Ph. D. Dissertation. University of Edinburgh.

Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs, In *Proceedings of the 23rd ACM SIGPLAN Conference on Functional Programming (ICFP 2018)*. *Proceedings of the ACM on Programming Languages* 2, 73:1–73:30. https://doi.org/10.1145/3236768

Ulf Norell. 2007. *Towards a practical programming language based on dependent type theory*. Ph. D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden.

Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. 2012. Dependent Interoperability. In *Proceedings of the 6th workshop on Programming Languages Meets Program Verification (PLPV 2012)*. ACM Press, 3–14. https://doi.org/10.1145/2103776.2103779

Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types. In *Proceedings of the IFIP International Conference on Theoretical Computer Science*. 437–450. https://doi.org/10.1007/1-4020-8141-3_34
Pierre-Marie Pédrot and Nicolas Tabareau. 2017. An effectful way to eliminate addiction to dependence. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*. IEEE Computer Society, 1-12. https://doi.org/10.1109/LICS.2017.8005113

Pierre-Marie Pédrot and Nicolas Tabareau. 2018. Failure is Not an Option - An Exceptional Type Theory. In *Proceedings of the 27th European Symposium on Programming Languages and Systems (ESOP 2018) (Lecture Notes in Computer Science, Vol. 10801)*, Amal Ahmed (Ed.). Springer-Verlag, Thessaloniki, Greece, 245-271. https://doi.org/10.1007/978-3-319-89884-1_9

Pierre-Marie Pédrot and Nicolas Tabareau. 2020. The fire triangle: how to mix substitution, dependent elimination, and effects. *Proceedings of the ACM on Programming Languages* 4, POPL (Jan. 2020), 58:1-58:28. https://doi.org/10.1145/3371126

Pierre-Marie Pédrot, Nicolas Tabareau, Hans Fehrmann, and Éric Tanter. 2019. A Reasonably Exceptional Type Theory. See [ICFP 2019], 108:1-108:29.

Benjamin C. Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hrițcu, Vilhelm Sjoberg, and Brent Yorgey. 2015. *Software Foundations*. Electronic textbook. http://www.cis.upenn.edu/bcpierce/sf.

POPL 2010 2010. *Proceedings of the 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010)*. ACM Press, Madrid, Spain.

Loïc Puget and Nicolas Tabareau. 2024. Observational Equality Meets CIC. In *Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg*, April 6-11, 2024, *Proceedings, Part I* (Luxembourg City, Luxembourg). Springer-Verlag, Berlin, Heidelberg, 275-301. https://doi.org/10.1007/978-3-031-57262-3_12

Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In *Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008)*, Rajiv Gupta and Saman P. Amarasinghe (Eds.). ACM Press, 159-169. https://doi.org/10.1145/1375581.1375602

Jeremy Siek, Ronald Garcia, and Walid Taha. 2009. Exploring the Design Space of Higher-Order Casts. See [Castagna 2009], 17-31.

Jeremy Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In *Proceedings of the Scheme and Functional Programming Workshop*. 81-92.

Jeremy Siek and Philip Wadler. 2010. Threesomes, with and without blame. See [POPL 2010 2010], 365-376. https://doi.org/10.1145/1706299.1706342

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In *1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 32)*. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Asilomar, California, USA, 274-293. https://doi.org/10.4230/LIPIcs.SNAPL.2015.274

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. 2015b. Monotonic References for Efficient Gradual Typing. In *Proceedings of the 24th European Symposium on Programming Languages and Systems (ESOP 2015) (Lecture Notes in Computer Science, Vol. 9032)*, Jan Vitek (Ed.). Springer-Verlag, London, UK, 432-456.

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2019. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. 4, POPL, Article 8 (dec 2019), 28 pages. https://doi.org/10.1145/3371076

Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich. 2010. Termination Casts: A Flexible Approach to Termination with General Recursion. In *Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010)*. 76-93. https://doi.org/10.29007/3w36

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016. Dependent types and multi-effects in F\*, See [Bodik and Majumdar 2016], 256-270. https://doi.org/10.1145/2837614

Éric Tanter and Nicolas Tabareau. 2015. Gradual Certified Programming in Coq. In *Proceedings of the 11th ACM Dynamic Languages Symposium (DLS 2015)*. ACM Press, Pittsburgh, PA, USA, 26-40.

The Coq Development Team. 2020. The Coq proof assistant reference manual. https://coq.inria.fr/refman/ Version 8.12.

Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can't Be Blamed. See [Castagna 2009], 1-16. https://doi.org/10.1007/978-3-642-00590-9_1

Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In *Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '98)*. ACM Press, 249-257. https://doi.org/10.1145/277650.277732

Received 2024-02-28; accepted 2024-06-18