# Generic bidirectional typing for dependent type theories

Thiago Felicissimo

► To cite this version:

Thiago Felicissimo. Generic bidirectional typing for dependent type theories. ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg City, Luxembourg. 10.1007/978-3-031-57262-3_6. hal-04270368v2

HAL Id: hal-04270368

https://inria.hal.science/hal-04270368v2

Submitted on 16 Dec 2024

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
# Generic bidirectional typing for dependent type theories

Thiago Felicissimo

Université Paris-Saclay, INRIA, LMF, ENS Paris-Saclay, Gif-sur-Yvette, France
thiago.felicissimo@inria.fr

**Abstract.** Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.

**Keywords:** Type Theory · Bidirectional Typing · Logical Frameworks

## 1 Introduction

Algebraic [13,7] and logical framework [27,45,8,21] presentations of dependent type theories suffer from the verbosity of the required explicit type annotations, which destroys any hope of practical usability. In these settings, every type argument must be explicitly spelled out: an application is written as $t@_{A,x.B}u$, a dependent pair as $\langle t, u \rangle_{A,x.B}$, cons as $t ::_A l$ and the list goes on.

In order to restore usability, standard presentations of dependent type theories omit the majority of these annotations, so one writes $t u$ for application, $\langle t, u \rangle$ for a dependent pair, $t :: l$ for cons, etc. This unannotated syntax is so common that readers not familiar with algebraic presentations of type theory might not even realize that an omission is being made.

The omission of type arguments has nevertheless a cost: because knowing them is still important when typing terms, it becomes unclear how to do this algorithmically, even when decidability of conversion holds. Take for instance the typing rule for the dependent pair: in order to type $\langle t, u \rangle$ one needs to guess
the arguments A and B, as unlike for the fully-annotated version $\langle t, u \rangle_{A,x.B}$ these are not stored in the syntax.

$$ \frac{\Gamma \vdash A \text{ type} \qquad \Gamma, x : A \vdash B \text{ type} \qquad \Gamma \vdash t : A \qquad \Gamma \vdash u : B[t/x]}{\Gamma \vdash \langle t, u \rangle : \Sigma x : A.B} $$

A solution to this problem is provided by bidirectional typing [35,16,19,20,41]. In this typing discipline, the declarative typing judgment $\Gamma \vdash t : A$ is decomposed explicitly into inference $\Gamma \vdash t \Rightarrow A$, where $\Gamma$ and $t$ are inputs and A is an output, and checking $\Gamma \vdash t \Leftarrow A$, where $\Gamma$, $t$ and $A$ are all inputs. The important point is that, by using these new judgments to control the flow of type information in a typing rule, one can specify algorithmically how the rule should be used. For instance, the following rule clarifies how one should type $\langle t, u \rangle$: the types A and B are not to be guessed, but instead recovered from the type C, which should be given as input.

$$ \frac{C \rightarrow^* \Sigma x : A.B \qquad \Gamma \vdash t \Leftarrow A \qquad \Gamma \vdash u \Leftarrow B[t/x]}{\Gamma \vdash \langle t, u \rangle \Leftarrow C} $$

We therefore see that bidirectional typing is the natural companion for an unannotated syntax, as it allows to algorithmically explain how the missing information can be retrieved.

Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories [16,33,25,1,38,2]. However, the formal development of bidirectional typing has until now remained confined to specific theories, with general guidelines remaining informal. One can then naturally wonder if it would be possible to define a framework in which bidirectional typing could be studied generically, putting its general theory in solid ground. This is exactly the goal of this paper.

We contribute a theory-independent account of bidirectional typing. For this, we start by giving a general definition of type theories (or equivalently, a logical framework), which differs from previous frameworks [45,29] by allowing for the usual unannotated syntaxes most often used in practice. Each such theory then defines a declarative type system, which is shown to satisfy good properties like weakening, substitution and, for well-behaved theories, subject reduction.

Then, to formulate our bidirectional system we first address the known problem that some unannotated terms cannot be algorithmically typed [18]. We propose generic notions of *inferable* and *checkable* terms which, for non-degenerate theories, coincide respectively with neutrals and normal forms, and then formulate our bidirectional system for this subset of terms. As argued in previous works [38,1], this restriction is reasonable because users of type theory usually only write terms in normal form. We then show, in a theory-independent fashion, that the bidirectional system is sound and complete with respect to the declarative system, establishing an equivalence between the two.

This equivalence is then explored to establish, for weak normalizing theories, the decidability of inference for inferable terms, and the decidability of checking
for checkable terms. This proof gives rise to generic type inference and checking algorithms, which have been implemented in a prototype theory-independent checker, allowing them to be used in practice with multiple theories. This implementation is described in detail in an accompanying experience report [22].

*Plan of the paper* We start in Section 2 by giving our general definition of type theories. We then move to Section 3, in which we give the declarative type system and show it satisfies nice properties. Section 4 then gives the bidirectional type system and its proof of equivalence with the declarative one. In Section 5 we show various examples of theories which are instances of our framework. We finish by discussing related work in Section 6 and then we conclude with Section 7.

# 2 General type theories

In this section, we give a general definition of type theories (or equivalently, a logical framework) for which we will give declarative and bidirectional type systems in later sections. Our definition is inspired by recent proposals of general definitions of type theories [29,45] and by the logical framework literature [27,8,26,40]. Our definition however crucially departs from these works by allowing for unannotated syntaxes and by exploring the constructor/destructor symmetries of symbols and rules in type theories.

We start the section by defining the raw syntax of our theories. Then, after defining patterns and substitution, we give one of the central definitions of our work: the one of theory. We finish the section by describing the rewrite judgment used to specify the definitional equality of our type theories.

## 2.1 Raw Syntax

*Scopes and signatures* The basic ingredients of our raw expressions are variables, metavariables and symbols. These are specified by scopes and signatures, which we define by the following grammars.

$$ \text{Scope} \quad \exists \quad \gamma, \delta ::= \cdot \mid \gamma, x $$

$$ \text{MScope} \quad \exists \quad \theta, \xi ::= \cdot \mid \theta, x\{\delta\} $$

$$ \text{Sig} \quad \exists \quad \Sigma ::= \cdot \mid \Sigma, c(\theta) \mid \Sigma, d(\theta) $$

Let us go through the definition. A (*variable*) scope $\gamma$ is simply a list of variables, whereas a *metavariable* scope $\theta$ is a list of metavariables, each being accompanied by a variable scope $\delta$ explaining the arguments each *metavariable* expects. A *signature* $\Sigma$ then assigns a *metavariable* scope $\theta$ to each symbol, also explaining the arguments it expects.

We see that, from the start, we split symbols in two classes: *constructors c* and *destructors d*. This separation will be justified by the fact that each of these two classes will play a different role in our theories: destructors are the source of
computation and are bidirectionally typed in mode infer, whereas constructors are the results of computations and are bidirectionally typed in mode check.

In the following, we write $\gamma.\delta$ and $\theta.\xi$ for scope concatenation, and we write constructor names in blue and destructor names in orange.

**Example 1.** The following signature $\Sigma_{\lambda\Pi}$ defines the raw syntax of a minimalistic Martin-Löf Type Theory (MLTT) with only dependent functions.

$$ \text{Ty}, \text{Tm}(A), \Pi(A, B\{x\}), \lambda(t\{x\}), \text{@}(u) \qquad (\Sigma_{\lambda\Pi}) $$

The entry for `@` might seem a bit strange since application usually takes two arguments, `t` and `u`. As we will see, destructors automatically take an extra argument, so we do not need to specify one for `t`. The reason for including symbols `Ty` and `Tm` will also become clear later.

*Terms and spines* Given a fixed signature $\Sigma$, we then define the terms, (variable) substitutions and metavariable substitutions by the following grammars.

$$
\begin{array}{r@{\quad}l@{\quad}l@{\qquad}l}
\boxed{\text{Tm } \theta \gamma} & \exists & t, u, T, U ::= & |x & \text{if } x \in \gamma \\
& & & |x\{\vec{t} \in \text{Sub } \theta \gamma \delta\} & \text{if } x\{\delta\} \in \theta \\
& & & |c(t \in \text{MSub } \theta \gamma \xi) & \text{if } c(\xi) \in \Sigma \\
& & & |d(t \in \text{Tm } \theta \gamma; t \in \text{MSub } \theta \gamma \xi) & \text{if } d(\xi) \in \Sigma \\
\boxed{\text{Sub } \theta \gamma \delta} & \exists & \vec{t}, \vec{u}, \vec{s}, \vec{v} ::= & |\varepsilon & \text{if } \delta = \cdot \\
& & & |\vec{u} \in \text{Sub } \theta \gamma \delta', t \in \text{Tm } \theta \gamma & \text{if } \delta = \delta', x \\
\boxed{\text{MSub } \theta \gamma \xi} & \exists & t, u, s, v ::= & |\varepsilon & \text{if } \xi = \cdot \\
& & & |u \in \text{MSub } \theta \gamma \xi', \vec{x}_{\delta,t} \in \text{Tm } \theta \gamma.\delta & \text{if } \xi = \xi', x\{\delta\}
\end{array}
$$

We go through the definition step by step. First, we elect an intrinsically-scoped presentation of syntax, so the definitions of terms, substitutions and metavariable substitutions are each indexed by a scope $\gamma$ and a metavariable scope $\theta$, describing the variables and metavariables that can appear free.

A term is then either a variable $x$, a metavariable $x$ applied to a substitution $\vec{t}$, a constructor $c$ applied to a metavariable substitution $t$ or a destructor $d$ applied to a term $t$ and a metavariable substitution $t$. At the level of the syntax, the main difference between constructors and destructors is that the latter are automatically applied to a first argument, called the *principal argument*. Note also that we require each variable and metavariable to be in scope, and each metavariable or symbol to be applied to a substitution matching its scope of arguments, as specified by $\theta$ or $\Sigma$.

A (variable) substitution $\vec{t} \in \text{Sub } \theta \gamma \delta$ is then either the empty substitution when $\delta$ is empty, or a substitution $\vec{u} \in \text{Sub } \theta \gamma \delta'$ and a term $t \in \text{Tm } \theta \gamma$ when $\delta = \delta', x$. Therefore, we see that the scope $\delta$ describes the output (or the domain of definition) of the substitution $\vec{t}$. Similarly, a *metavariable substitution* $t \in \text{MSub } \theta \gamma \xi$ is either empty when $\xi$ is empty, or a metavariable substitution
u ∈ MSub θ γ ξ' and a term t ∈ Tm θ γ.δ when ξ = ξ', x{δ}. Unlike variable substitutions, variable substitutions are allowed to extend the scope of their arguments by binding the variables in δ, which we refer to by x. This is used for instance in the cases of λ and Π in the following example.

*Example 2.* The terms defined by the signature Σ<sub>Π</sub> are given by the following grammar, where we omit the scope requirements for variables and metareferences.

$$t, u, A, B ::= x \mid x\{\vec{t}\} \mid Ty \mid Tm(A) \mid \lambda(x.t) \mid \Pi(A, x.B) \mid @\langle t; u \rangle$$

In the following, given a metareference substitution t ∈ MSub θ γ ξ and x{δ} ∈ ξ, we write t<sub>x</sub> ∈ Tm θ γ.δ for the term in t at the position pointed by x. Similarly, given a substitution t̄ ∈ Sub θ γ δ and x ∈ δ, we write t<sub>x</sub> ∈ Tm θ γ for the term in t̄ at the position pointed by x.

*Contexts* Given a fixed signature Σ, we define (variable) contexts and metaref- able contexts by the following grammars.

$$\mathbf{Contexts} \quad \Gamma, \Delta ::= \cdot \mid \Gamma \in \mathbf{Contexts} \quad \gamma, x : T \in Tm \quad \gamma \cdot | \Gamma|$$

$$\mathbf{Metaref. Contexts} \quad \Theta, \Xi ::= \cdot \mid \Theta \in \mathbf{Metaref. Contexts} \quad \gamma, x \{ \Gamma \in \mathbf{Metaref. Contexts} \cdot | \Theta | (\cdot) \} : T \in Tm \quad \gamma \cdot | \Theta| | \Gamma|$$

These are specified mutually with the underlying scopes |Γ| of Γ and |Θ| of Θ, defined by the following clauses.

$|_\cdot : \mathbf{Contexts} \quad \gamma \to \mathbf{Scope}$

$|\cdot| := \cdot$

$|\Gamma, x : T| := |\Gamma|, x$

$|\_\cdot : \mathbf{Metaref. Contexts} \quad \theta \to \mathbf{MScope}$

$|\cdot| := \cdot$

$|\Theta, x\{\Delta\} : T| := |\Theta|, x\{|\Delta|\}$

A context Γ ∈ Ctx γ θ is either empty, or composed by a context Γ' ∈ Ctx γ θ and a variable x with a term T ∈ Tm θ γ.|Γ'|. The first important thing to note is that the term T does not live in scope γ, but in the extension of γ with the underlying scope of Γ', meaning that each entry in the context has access to the previously declared variables. Second, like in other frameworks [45], terms can also play the role of judgments, as illustrated by the following example.

*Example 3.* In MLTT we have two judgment forms: □ type for classifying types, and □ : A for classifying terms. In our framework, these are represented by the constructors Ty and Tm. For instance, the context A type, x : A, y : (Πz : A.A) of MLTT is represented in our framework as

$$A : Ty, x : Tm(A), y : Tm(\Pi(A, z.A))$$

which is syntactically well-formed in the signature Σ<sub>Π</sub>. We can also write some strange contexts like x : λ(z.z), y : x, which will be eliminated later by typing.

The case of a *metaref. variable context* Θ ∈ MContext θ is similar. We have either Θ empty or Θ = Θ', x{Δ} : T, where Δ has access to metaref. variables in θ and Θ, and T has moreover access to the variables in Δ.
Notation 1. We finish this subsection by establishing some notations.

- We write $e \in \text{Expr } \theta \gamma$ as an informal abbreviation for any of the following: $e \in \text{Tm } \theta \gamma$ or $e \in \text{Sub } \theta \gamma \delta$ or $e \in \text{MSub } \theta \gamma \xi$ or $e \in \text{'Ctx } \theta \gamma$.

- If the underlying signature is not clear from the context, we write $\text{Tm}_\Sigma$, $\text{Sub}_\Sigma$, $\text{MSub}_\Sigma$, $\text{'Ctx}_\Sigma$, $\text{M'Ctx}_\Sigma$ in order to make it explicit.

- We write $\text{'Ctx } \theta$ for $\text{'Ctx } \theta(\cdot)$, $\text{'Ctx}$ for $\text{'Ctx } \cdot(\cdot)$ and $\text{M'Ctx}$ for $\text{M'Ctx } \cdot(\cdot)$.

Remark 1. Because we work with a nameful syntax, we allow ourselves to implicitly weaken expressions: if $e \in \text{Expr } \theta \gamma$ and $\theta$ is a subsequence of $\theta'$ and $\gamma$ is a subsequence of $\gamma'$ then we also have $e \in \text{Expr } \theta' \gamma'$. Nevertheless, we expect that our proofs can be formally carried out using de Bruijn indices, by properly inserting weakenings whenever needed, and showing all the associated lemmata.

2.2 Substitution

Before defining the application of a substitution to a term, we first need to define the *identity substitutions*, by the following clauses. Note that, while the identity variable substitution $\text{id}_\gamma$ is just the list of variables from $\gamma$, the identity variable substitution $\text{id}_\theta$ needs to eta-expand each variable $x\{\delta\} \in \theta$ to $\vec{x}_\delta.x\{\text{id}_\delta\}$ in order for the result to be a valid variable substitution. In the following, we sometimes abuse notation and write $\text{id}_\Gamma$ for $\text{id}|_\Gamma$ and $\text{id}_\Theta$ for $\text{id}|_\Theta$.

$\text{id}_- : (\gamma \in \text{Scope}) \rightarrow \text{Sub}(\cdot) \gamma \gamma$

$\text{id}_-(\cdot) := \varepsilon$

$\text{id}_{\gamma,x} := \text{id}_\gamma, x$

$\text{id}_+ : (\theta \in \text{MScope}) \rightarrow \text{MSub} \ \theta(\cdot) \ \theta$

$\text{id}_+(\cdot) := \varepsilon$

$\text{id}_{\theta,x\{\gamma\}} := \text{id}_\theta, \vec{x}_\gamma.x\{\text{id}_\gamma\}$

We can now define in Figure 1 the application of a substitution to an expression. Given a variable substitution $\vec{v} \in \text{Sub } \theta_1 \gamma_2$ its application to an expression $e \in \text{Expr } \theta_2$ gives $e[\vec{v}] \in \text{Expr } \theta_1$, and given a variable substitution $v \in \text{MSub } \theta_1 \delta \theta_2$ its application to an expression $e \in \text{Expr } \theta_2$ gives $e[v] \in \text{Expr } \theta_1 \delta \gamma$. The main case of the definition is when we substitute $v \in \text{MSub } \theta_1 \delta \theta_2$ in the term $x\{\vec{t}\} \in \text{Tm } \theta_2 \gamma$. If $x\{\gamma_x\} \in \theta_2$, then by recursively substituting $v$ in $\vec{t} \in \text{Sub } \theta_2 \gamma \gamma_x$ we get $\vec{t}[v] \in \text{Sub } \theta_1 \delta \gamma \gamma_x$. We moreover have $v_x \in \text{Tm } \theta_1 \delta \gamma_x$, so by substituting the variables in $\gamma_x$ by $\vec{t}[v]$ and the ones in $\delta$ by $\text{id}_\delta$ we get $v_x[\text{id}_\delta, \vec{t}[v]] \in \text{Tm } \theta_1 \delta \gamma$ as the final result.

*Example 4.* If $t \in \text{Tm}(\cdot)(\gamma, x)$ and $u \in \text{Tm}(\cdot)\gamma$, then by applying $x.t, u \in \text{MSub}(\cdot)\gamma$ ($t\{x\}, u$) to @($\lambda(x.t\{x\}); u$) $\in \text{Tm}(t\{x\}, u)(\cdot)$ we get the term @($\lambda(x.t); u$) $\in \text{Tm}(\cdot)\gamma$. Note in particular that, compared to frameworks derived from contextual modal type theory [37], our variable substitutions are not required to be closed and can introduce new variables in the scope of the resulting term. For instance, while the initial term @($\lambda(x.t\{x\}); u$) lives in an empty variable scope, the resulting term @($\lambda(x.t); u$) lives in the variable scope $\gamma$.

Substitution application satisfies all the expected laws, such as $e[v][u] = e[v[u]]$, $e[\text{id}_\gamma] = e$ and $\text{id}_\theta[v] = v$ — we refer to the technical report [24] for a detailed account of these properties, and for the full definition of substitution.
<figure><img src="image_2.png" /><figcaption>Fig. 1. Application of a variable or variable substitution (excerpt)</figcaption></figure>

## 2.3 Patterns

There will be a need to isolate a special class of expressions that will be shown later to support decidable and unitary matching. This will be needed both to define the rewrite rules of our theories and to determine when omitted arguments can be recovered. For this, given a fixed signature $\Sigma$, we define the term patterns and *metavariable substitution patterns* by the following grammars.

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

As we can see, the only symbols that are allowed to appear in patterns are constructors. This will be essential later to ensure that patterns do not only support syntactic matching, but also matching modulo rewriting. Moreover, our patterns are linear, and so each *metavariable* in scope occurs exactly once. Finally, our patterns are *fully-applied*, meaning that each *metavariable* occurrence is fully applied to all variables in scope.

*Example 5.* In the signature $\Sigma_{\Pi}$ we can build the pattern

$$ \mathrm{Tm}(\Pi(A, x.B\{x\})) \in \mathrm{Tm}^P(A, B\{x\}) (\cdot) $$

We have the inclusions $\mathrm{Tm}^P \theta \gamma \subset \mathrm{Tm} \theta \gamma$ and $\mathrm{MSub}^P \theta \gamma \xi \subset \mathrm{MSub} \theta \gamma \xi$, which we use to implicitly coerce patterns into regular expressions when needed.

## 2.4 Theories

We now come to a central definition in our work, that of a *theory* $\mathcal{T}$. We define inductively how a theory is built, simultaneously with its underlying signature $|\mathcal{T}|$ — technically, our definition is by small induction-recursion. The base case covers the empty theory $\mathcal{T} = (\cdot)$, so assuming now a theory $\mathcal{T}$ is given we can extend it with two types of entries: *schematic typing rules* and *rewrite rules*. We start with the first, which come in three kinds: sort, constructor and destructor rules.
**Sort rules** In our framework, a sort $T$ is a term that can appear to the right of a colon.<fnref n="1" /> As hinted in Example 3, and following [13,45,44], sorts are used to specify the judgment forms of a theory. For instance, the two judgment forms of MLTT "□ type" and "□ : A" are defined by the following.

$$ \vdash A : Ty \qquad \frac{\vdash Tm(A) \text{ sort}}{} $$

Formally, a sort rule is of the form

$$ c(\Xi \in \mathbf{MCtx}_{|T|}) \text{ sort} $$

and the previously shown rules are just an informal notation for $Ty(\cdot)$ sort and $Tm(A : Ty)$ sort. In the following, we will make use of such informal representations in order to enhance readability of schematic rules. Note also that the premises (e.g. $\vdash A : Ty$) correspond to entries in the variable context of the rule, and henceforth we will use these two points of view interchangeably.

**Constructor rules** Like most works in bidirectional typing [35,19,1,16], our framework imposes that constructors are to be bidirectionally typed in mode check, and thus the sort of the conclusion can be used to recover arguments which are not recorded in the syntax. To capture this, premises are split into two variable contexts $\Xi_1$ and $\Xi_2$, where $\Xi_1$ is erased and $\Xi_2$ is stored in the term. The sort $T$ is then required to be a pattern containing the variables of $\Xi_1$, leading to constructor rules of the following form.

$$ c(\Xi_1 \in \mathbf{MCtx}_{|T|}; \Xi_2 \in \mathbf{MCtx}_{|T|} | \Xi_1) : U \in Tm_{|T|}^{P} | \Xi_1 | (\cdot) $$

Two examples of constructor rules are the ones for $\Pi$ and $\lambda$ — note however that the one for $\Pi$ is slightly degenerate, given that we have $\Xi_1 = \cdot$ and thus no erased premises.

$$ \frac{\vdash A : Ty \qquad x : Tm(A) \vdash B : Ty}{\vdash \Pi(A, B) : Ty} \qquad \frac{x : Tm(A) \vdash B : Ty}{x : Tm(A) \vdash t : Tm(B\{x\})} \qquad \frac{\vdash \lambda(t) : Tm(\Pi(A, x.B\{x\}))}{\vdash \lambda(t) : Tm(\Pi(A, x.B\{x\}))} $$

These are just informal notations for $\Pi(\cdot; A : Ty, B\{x : Tm(A)\} : Ty) : Ty$ and $\lambda(A : Ty, B\{x : Tm(A)\} : Ty; t\{x : Tm(A)\} : Tm(B\{x\})) : Tm(\Pi(A, x.B\{x\}))$.

** rules** As for constructor rules, in destructor rules premises are also separated into erased $\Xi_1$ and non-erased $\Xi_2$ parts. However, unlike constructors, destructors are bidirectionally typed in inference mode. In this case, the erased arguments in $\Xi_1$ are not to be recovered from the sort of the conclusion, but instead by inferring the sort of the *principal argument* which is required to be

<footnote n="1">¹ We avoid calling them "types" to prevent a name clash with the types of the theories we define. Still, we allow ourselves to say "t is typed by sort $T$" to mean $t : T$.</footnote>
a pattern containing the variables of $\Xi_1$. The destructor rules are therefore of the following form.

$$d(\Xi_1 \in \mathbf{MC}_{\mathbf{T}}; x : T \in \mathbf{Tm}_{\mathbf{T}}^P | \Xi_1 | (\cdot); \Xi_2 \in \mathbf{MC}_{\mathbf{T}} | (\Xi_1 | x, \Xi_2 | \cdot)) : U \in \mathbf{Tm}_{\mathbf{T}} | (\Xi_1 | x, \Xi_2 | \cdot) (\cdot)$$

The main example of destructor rule is the application rule

$$\vdash A : Ty \qquad x : Tm(A) \vdash B : Ty \qquad \vdash t : Tm(\Pi(A, x.B\{x\})) \qquad \vdash u : Tm(A) \\ \qquad \vdash @ (t; u) : Tm(B\{u\})$$

which is just an informal notation for

$$@ (A : Ty, B\{x : Tm(A)\} : Ty; t : Tm(\Pi(A, x.B\{x\})); u : Tm(A)) : Tm(B\{u\})$$

**Rewrite rules** Finally, the last type of rules are rewrite rules, which allow us to specify the definitional equality (also known as conversion) of the theory. As suggested by our constructor/destructor separation of symbols, the left-hand side of rewrite rules are to be headed by destructors. Moreover, to ensure the decidability of rewriting, we also ask both arguments *t* and *u* of the left hand side *d(t; u)* to be patterns. The right-hand side of the rule is then a term containing only the variables introduced by *t* and *u*. The rewrite rules are hence of the following form, where $d(\xi) \in \mathbb{T}$.

$$\theta_1; \theta_2 \Vdash d(t \in \mathbf{Tm}_{\mathbb{T}}^P \theta_1 (\cdot); u \in \mathbf{MSub}_{\mathbb{T}}^P \theta_2 (\cdot) \xi) \mapsto r \in \mathbf{Tm}_{\mathbb{T}} \theta_1 . \theta_2 (\cdot)$$

We shall also ask for a supplementary condition: in order to extend a theory $\mathbb{T}$ with a rule $\theta_1; \theta_2 \Vdash l \mapsto r$, there can be no rule $\theta'_1; \theta'_2 \Vdash l' \mapsto r'$ in $\mathbb{T}$ such that we have $l[\mathbf{v}] = l'[\mathbf{v}']$ for some $\mathbf{v}$ and $\mathbf{v}'$. As discussed in the next subsection, this will ensure that the rewrite system is confluent by construction.

The prototypical example of a rewrite rule is the computation rule for functions: the $\beta$-rule from the $\lambda$-calculus.

$$t\{x\}; u \Vdash @ (\lambda(x.t\{x\}); u) \mapsto t\{u\}$$

In the following we allow ourselves to omit the variable scopes $\theta_1, \theta_2$ as these can be easily reconstructed by inspecting the rewrite rule's left hand side.

**Underlying signature** Finally, the recursive definition of the underlying signature of a theory is given by the following clauses, where we write Thy for the set of theories. As we can see, in both constructor and destructor rules the variable $\Xi_1$ is omitted from the syntax. Moreover, rewrite rules are simply ignored when computing the underlying signature.

$$\begin{array}{l@{\quad}l}
|\_| : \text{Thy} \to \text{Sig & } |\mathbb{T}, c(\Xi_1; \Xi_2) : U| := |\mathbb{T}|, c(|\Xi_2|) \\
|\cdot| := \cdot & |\mathbb{T}, d(\Xi_1; x : T; \Xi_2) : U| := |\mathbb{T}|, d(|\Xi_2|) \\
|\mathbb{T}, c(\Xi) \text{ sort}| := |\mathbb{T}|, c(|\Xi|) & |\mathbb{T}, \theta_1; \theta_2 \Vdash d(t; u) \mapsto r| := |\mathbb{T}|
\end{array}$$
*Example 6.* By putting together all of the rules previously seen in this subsection, we get the following theory $T_{\lambda\Pi}$ defining a basic version of MLTT with only dependent functions.

Ty(·) sort, Tm(A : Ty) sort, Π(·; A : Ty, B{x : Tm(A)} : Ty) : Ty, (T_{\lambda\Pi})
λ(A : Ty, B{x : Tm(A)} : Ty; t{x : Tm(A)} : Tm(B{x})) : Tm(Π(A,x.B{x))),
@(A : Ty, B{x : Tm(A)} : Ty; t : Tm(Π(A,x.B{x})); u : Tm(A)) : Tm(B{u}),
@(λ(x.t{x}); u) ↦→ t{u}

When computing its underlying signature $|T_{\lambda\Pi}|$ we get the signature $\Sigma_{\lambda\Pi}$.

## 2.5 Rewriting

The rewrite rules of a theory $\mathcal{T}$ are used to define the *rewrite relation* $e \to e'$ for expressions $e, e' \in \mathit{Expr} \ \theta \ \gamma$, which is given by the context closure of the following rule — see the technical report [24] for the full definition.

$$ \frac{ (\theta_1; \theta_2 \models d(t; \mathbf{u}) \mapsto r) \in \mathcal{T} \quad \mathbf{v}_1 \in \mathit{MSub} \ \theta \ \gamma \ \theta_1 \quad \mathbf{v}_2 \in \mathit{MSub} \ \theta \ \gamma \ \theta_2 \\ d(t[\mathbf{v}_1]; \mathbf{u}[\mathbf{v}_2]) \to r[\mathbf{v}_1, \mathbf{v}_2] \in \mathcal{Tm} \ \theta \ \gamma } $$

The relations $\to^+$, $\to^*$ and $\equiv$ are then defined as usual, respectively as the transitive, reflexive-transitive and reflexive-symmetric-transitive closures of $\to$. The relation $\equiv$ is called the *definitional equality* (or *conversion*) of the theory.

Rewriting satisfies the key property of being stable under substitution: if $e \to^* e'$ and $\vec{v} \to^* \vec{v}'$ then $e[\vec{v}] \to^* e'[\vec{v}]$, and if $e \to^* e'$ and $\mathbf{v} \to^* \mathbf{v}'$ then $e[\mathbf{v}] \to^* e'[\mathbf{v}]$. This implies in particular that definitional equality is also stable under substitution.

Finally, recall that when defining theories we asked that no two different left-hand sides should unify. Because this is the only way two rule can overlap, this means that there are no *critical pairs* [11]. Therefore, because rules are also all *left-linear*, it follows that the rewrite system of any theory is *orthogonal*, hence confluent by [34, Theorem 6.11].

**Proposition 1 (Confluence).** If $e' * \leftarrow e \to^* e''$ then there is some $e'''$ such that $e' \to^* e''' * \leftarrow e''$. In particular, this implies that whenever $e \equiv e'$ then we have $e \to^* e'' * \leftarrow e'$ for some $e''$.

*Notation 2.* Whenever the underlying theory is not clear from the context we write $\to_T$ and $\to_T^+$ and $\to_T^*$ and $\equiv_T$ to make it explicit.

## 3 Declarative type system

In the previous section we have given a general definition of type theories. As explained in the introduction, each theory also defines a declarative type system, which can be seen as the platonic type system, and a bidirectional type system, which is the one that can be algorithmically used in practice.
In this section we introduce the declarative type system. This system is then used to define the valid theories, a class of theories which are well-behaved. We then conclude the section by showing that the declarative system satisfies nice properties, and in particular satisfies subject reduction when the theory is valid.

## 3.1 Declarative typing rules

Given a fixed theory $T$, the declarative type system is defined by the rules in Figure 2. The system is split in 6 judgments:

- $\Theta \vdash : \text{Well-formedness of variable context } \Gamma$ under context $\Theta$.

- $\Theta; \Gamma \vdash : \text{Well-formedness of variable context } \Gamma$ under declarative context $\Theta$.

- $\Theta; \Gamma \vdash T \text{ sort} : \text{Well-formedness of sort } T$ under contexts $\Theta; \Gamma$.

- $\Theta; \Gamma \vdash t : T : \text{Typing of a term } t$ by $T$ under context $\Theta; \Gamma$.

- $\Theta; \Gamma \vdash \vec{t} : \Delta : \text{Typing of a variable substitution } \vec{t}$ by $\Delta$ under context $\Theta; \Gamma$.

- $\Theta; \Gamma \vdash t : \Xi : \text{Typing of a declarative substitution } t$ by $\Xi$ under context $\Theta; \Gamma$.

The most important rules are the ones which instantiate schematic typing rules: CONS, DEST and SORT. For instance, in order to use DEST to type $d(t; u)$ a declarative substitution $t$ not stored in the syntax must be "guessed", and then we must show that $t, t, u$ is typed by $\Xi_1.(x : T).\Xi_2$. The rules for typing a declarative substitution can then be applied, which has the effect of unfolding the judgment $t, t, u : \Xi_1.(x : T).\Xi_2$ into regular term typing judgments. At the end of this unfolding process, the resulting "big-step derivation" has basically the same shape as the schematic typing rule for $d$, and it can be understood as its instantiation. Let us look at a concrete example of this.

*Example 7.* Suppose we want to show that $@ (t; u)$ is well-typed in the theory $T_{\Lambda\Pi}$. Because $@$ is a destructor symbol with schematic rule

$$ @ (A : \text{Ty}, B\{x : \text{Tm}(A)\} : \text{Ty}; t : \text{Tm}(\Pi(A, x.B\{x}\)), u : \text{Tm}(A)) : \text{Tm}(B\{u\}) $$

by guessing some $A$ and $B$ we can start the derivation with rule DEST, giving

$$ \Theta; \Gamma \vdash A, x.B, t, u : (A : \text{Ty}, B\{x : \text{Tm}(A)\} : \text{Ty}, t : \text{Tm}(\Pi(A, x.B\{x}\)), u : \text{Tm}(A)) $$

$$ \Theta; \Gamma \vdash @ (t; u) : \text{Tm}(B\{u\}) [A, x.B, t, u] $$

If we note that $\text{Tm}(B\{u\})[A, x.B, t, u] = \text{Tm}(B[id_\Gamma, u])$, and we continue by applying the rules defining the judgment $\Theta; \Gamma \vdash t : \Xi$, we get

$$ \Theta; \Gamma \vdash \Theta; \Gamma \vdash A : \text{Ty} \quad \Theta; \Gamma, x : \text{Tm}(A) \vdash B : \text{Ty} $$

$$ \Theta; \Gamma \vdash t : \text{Tm}(\Pi(A, x.B)) \quad \Theta; \Gamma \vdash u : \text{Tm}(A) $$

$$ \Theta; \Gamma \vdash @ (t; u) : \text{Tm}(B[id_\Gamma, u]) $$

which can be understood as the instantiation of the schematic rule for $@$. This also corresponds to the usual application rule of MLTT, as the first 3 premises can be shown admissible by inversion of typing and the results of Subsection 3.3.
$$ \begin{array}{ccc} \Theta \vdash & (\Theta \in \mathbf{MCtx}) & \Theta; \Gamma \vdash (\Theta \in \mathbf{MCtx}; \Gamma \in \mathbf{Ctx} |\Theta|) \end{array} $$

$$ \begin{array}{ccc} \text{EMPTYMCTX} & \text{EXTMCTX} & \text{EMPTYCTX} \\ \underline{\cdot \vdash} & \underline{\Theta; \Gamma \vdash T \ \text{sort}} & \underline{\Theta; \cdot \vdash} \\ & \Theta, x\{\Gamma\} : T \vdash & \Theta; \Gamma \vdash T \ \text{sort} \end{array} $$

$$ \begin{array}{c} \Theta; \Gamma \vdash T \ \text{sort} \quad (\Theta \in \mathbf{MCtx}; \Gamma \in \mathbf{Ctx} |\Theta|; T \in \mathbf{Tm} |\Theta| |\Gamma|) \end{array} $$

$$ \text{SORT} \\ c(\Xi) \ \text{sort} \in \mathbb{T} \frac{\Theta; \Gamma \vdash t : \Xi}{\Theta; \Gamma \vdash c(t) \ \text{sort}} $$

$$ \begin{array}{c} \Theta; \Gamma \vdash t : T \quad (\Theta \in \mathbf{MCtx}; \Gamma \in \mathbf{Ctx} |\Theta|; T \in \mathbf{Tm} |\Theta| |\Gamma|; t \in \mathbf{Tm} |\Theta| |\Gamma|) \end{array} $$

$$ c(\Xi_1; \Xi_2) : T \in \mathbb{T} \frac{\Theta; \Gamma \vdash t, u : \Xi_1 \cdot \Xi_2}{\Theta; \Gamma \vdash c(u) : T[t]} \qquad x : T \in \Gamma \frac{\Theta; \Gamma \vdash}{\Theta; \Gamma \vdash x : T} $$

$$ d(\Xi_1; x : T; \Xi_2) : U \in \mathbb{T} \frac{\Theta; \Gamma \vdash t, u : \Xi_1 \cdot (x : T) \cdot \Xi_2}{\Theta; \Gamma \vdash d(t; u) : U[t, t, u]} \qquad x\{\Delta\} : T \in \Theta \frac{\Theta; \Gamma \vdash \vec{t} : \Delta}{\Theta; \Gamma \vdash x\{\vec{t}\} : T[\vec{t}]} $$

$$ T \equiv_T U \frac{\Theta; \Gamma \vdash t : T}{\Theta; \Gamma \vdash U \ \text{sort}} $$

$$ \begin{array}{c} \Theta; \Gamma \vdash \vec{t} : \Delta \quad (\Theta \in \mathbf{MCtx}; \Gamma \in \mathbf{Ctx} |\Theta|; \Delta \in \mathbf{Ctx} |\Theta|; \vec{t} \in \mathbf{Sub} |\Theta| |\Gamma| |\Delta|) \end{array} $$

$$ \frac{\text{EMPTYSUB}}{\Theta; \Gamma \vdash} \qquad \frac{\text{EXTSUB}}{\Theta; \Gamma \vdash \varepsilon : (\cdot)} \qquad \frac{\Theta; \Gamma \vdash \vec{t} : \Delta \qquad \Theta; \Gamma \vdash t : T[\vec{t}]}{\Theta; \Gamma \vdash \vec{t}, t : (\Delta, x : T)} $$

$$ \begin{array}{c} \Theta; \Gamma \vdash t : \Xi \quad (\Theta \in \mathbf{MCtx}; \Gamma \in \mathbf{Ctx} |\Theta|; \Xi \in \mathbf{MCtx}; t \in \mathbf{MSub} |\Theta| |\Gamma| |\Xi|) \end{array} $$

$$ \frac{\text{EMPTYMSUB}}{\Theta; \Gamma \vdash} \qquad \frac{\text{EXTMSUB}}{\Theta; \Gamma \vdash t : \Xi} \qquad \frac{\Theta; \Gamma \Delta[t] \vdash t : T[t]}{\Theta; \Gamma \vdash t, \vec{x}_{\Delta,t} : (\Xi, x\{\Delta\} : T)} $$

<caption>Fig. 2. Declarative typing rules</caption>
Notation 3. We finish this subsection by establishing some notations.

1. We write $\Theta; \Gamma \vdash \mathcal{J}$ for any of the following: $\Theta; \Gamma \vdash$ or $\Theta; \Gamma \vdash T$ sort or $\Theta; \Gamma \vdash t : T$ or $\Theta; \Gamma \vdash \tilde{t} : \Delta$ or $\Theta; \Gamma \vdash t : \Xi$.

2. We write $T \triangleright \Theta; \Gamma \vdash \mathcal{J}$ when $T$ is not clear from the context.

3. We write $\Theta \vdash \mathcal{J}$ for $\Theta; \cdot \vdash \mathcal{J}$ and $\Gamma \vdash \mathcal{J}$ for $\cdot; \Gamma \vdash \mathcal{J}$.

## 3.2 Valid theories

Our definition of theories given in Subsection 2.4 is a bit too permissive, and we would like to isolate a class of theories for which we can show nicer properties. These are the valid theories, defined by the following inference rules.

$$ \begin{array}{ccc} \begin{array}{c} \mathcal{T} \text{ valid} \\ \cdot \text{ valid} \end{array} & \begin{array}{c} \mathcal{T} \triangleright \Xi_1 \vdash T \text{ sort} \\ \mathcal{T}, c(\Xi_1; \Xi_2) : T \text{ valid} \end{array} & \begin{array}{c} \mathcal{T} \triangleright \Xi_1 \cdot \Xi_2 \vdash \\ \mathcal{T}, d(\Xi_1; x : U; \Xi_2) : T \text{ valid} \end{array} \\ \begin{array}{c} \mathcal{T} \text{ valid} \\ \mathcal{T}, c(\Xi) \text{ sort valid} \end{array} & \begin{array}{c} \mathcal{T} \triangleright \Xi_1 \vdash \\ \mathcal{T} \triangleright \Xi_1 \cdot (x : U) \cdot \Xi_2 \end{array} & \begin{array}{c} \mathcal{T} \triangleright \Xi_1 \cdot (x : U) \cdot \Xi_2 \vdash T \text{ sort} \\ \mathcal{T} \triangleright \Xi_1 \cdot x : U; \Xi_2 \end{array} \end{array} $$

$$ \begin{array}{c} \mathcal{T} \text{ valid} \\ \mathcal{T} \triangleright \Xi_1.\Theta_1.\Theta_2 \vdash (\mathrm{id}_{\Xi_1}, t, \mathbf{u}) : \Xi_1.(x : U).\Xi_2 \end{array} \quad \begin{array}{c} \mathrm{for} \ \mathrm{some} \ \Theta_1, \Theta_2 \ \mathrm{with} \ |\Theta_1| = \theta_1, |\Theta_2| = \theta_2 : \\ \mathrm{V}[\mathrm{id}_{\Xi_1}, t, \mathbf{u}] \end{array} \\ \mathcal{T}, \theta_1; \theta_2 \models d(t; \mathbf{u}) \mapsto r \text{ valid} \end{array} $$

Intuitively, the definition of valid theories ensures that each time we extend a theory $T$ with a schematic typing or rewrite rule, $T$ can justify that the extension is well-behaved. For sort rules $c(\Xi)$ sort this means ensuring that the variable context $\Xi$ is well-formed in $T$, and for destructor rules $d(\Xi_1; x : U; \Xi_2) : T$ this means ensuring that $T$ is a well-formed sort in variable context $\Xi_1.(x : U).\Xi_2$ and in the theory $T$. The rule for a constructor $c(\Xi_1; \Xi_2) : T$ does not only ask $\Xi_1.\Xi_2$ to be a well-formed variable context, but also for the term $T$ to be a well-formed sort for $\Xi_1$ — recall that $T$ can only contain variables from $\Xi_1$.

The most complicated case is for a rewrite rule $\theta_1; \theta_2 \models d(t; u) \mapsto r$, in which we must find variable contexts $\Theta_1, \Theta_2$ with $|\Theta_1| = \theta_1$ and $|\Theta_2| = \theta_2$ allowing to type $\mathrm{id}_{\Xi_1}, t, u$ and $r$. This technical condition is essential to prove subject reduction of our valid theories (Theorem 1).

**Example 8.** It is tedious but uncomplicated to see that the theory $T_{\lambda\Pi}$ is valid. The most interesting part of the proof is when we add the $\beta$-rule

$$ t\{x\}; u \models @\{\lambda(x.t\{x\}); u\} \mapsto t\{u\} $$

If we write $T'$ for the part of $T_{\lambda\Pi}$ preceding this declaration, and (for space reasons) we abbreviate $(A : Ty, B\{x : Tm(A)\} : Ty)$ as $\Theta_{AB}$, we have to show

$$ T' \triangleright \Theta_{AB}.\Theta_1.\Theta_2 \vdash (A, x.B\{x\}, \lambda(x.t\{x\}), u) : \Theta_{AB}.(t : Tm(\Pi(A, x.B\{x\})), u : Tm(A)) $$

and

$$ T' \triangleright \Theta_{AB}.\Theta_1.\Theta_2 \vdash t\{u\} : Tm(B\{u\}) $$

which can both be easily shown if we chose $\Theta_1 = t\{x : Tm(A)\} : Tm(B\{x\})$ and $\Theta_2 = u : Tm(A)$, which indeed satisfy $|\Theta_1| = t\{x\}$ and $|\Theta_2| = u$.
### 3.3 Basic metaproperties

We now show some basic metaproperties satisfied by the declarative type system. The assumption that the theory is valid is not necessary for all results, and will be stated explicitly when needed. We give proof sketches for some of the properties, and refer to the technical report [24] for the proofs.

**Proposition 2 (Contexts are well-formed).** The following rules are admissible.

$$ \frac{\Theta; \Gamma \vdash \mathcal{J}}{\Theta; \Gamma \vdash} $$

$$ \frac{\Theta; \Gamma \vdash \mathcal{J}}{\Theta \vdash} $$

**Proposition 3 (Weakening).** Let us write $\Gamma \sqsubseteq \Delta$ if $\Gamma$ is a subsequence of $\Delta$, and $\Theta \sqsubseteq \Xi$ if $\Theta$ is a subsequence of $\Xi$. The following rules are admissible.

$$ \Gamma \sqsubseteq \Delta \frac{\Theta; \Gamma \vdash \mathcal{J} \qquad \Theta; \Delta \vdash}{\Theta; \Delta \vdash \mathcal{J}} $$

$$ \Theta \sqsubseteq \Xi \frac{\Theta; \Gamma \vdash \mathcal{J} \qquad \Xi \vdash}{\Xi; \Gamma \vdash \mathcal{J}} $$

In order to state the substitution property, given $\Theta; \Delta \vdash \mathcal{J}$ we define the notations $(\Theta; \Delta \vdash \mathcal{J})[\vec{v}]$ and $(\Theta; \Delta \vdash \mathcal{J})[\mathbf{v}]$ by the following table.

<table><thead><tr><th>Θ; Δ ⊢ J</th><th>(Θ; Δ ⊢ J)[v̄]</th><th>(Θ; Δ ⊢ J)[v]</th></tr><tr><td></td><td>where Θ; Γ ⊢ v̄ : Δ</td><td>where Ξ; Γ ⊢ v : Θ</td></tr></thead><tbody><tr><td>Θ; Δ ⊢</td><td>Θ; Γ ⊢</td><td>Ξ; Γ.Δ[v] ⊢</td></tr><tr><td>Θ; Δ ⊢ T sort</td><td>Θ; Γ ⊢ T[v̄] sort</td><td>Ξ; Γ.Δ[v] ⊢ T[v] sort</td></tr><tr><td>Θ; Δ ⊢ t : T</td><td>Θ; Γ ⊢ t[v̄] : T[v̄]</td><td>Ξ; Γ.Δ[v] ⊢ t[v] : T[v]</td></tr><tr><td>Θ; Δ ⊢ ť : Δ'</td><td>Θ; Γ ⊢ ť[v̄] : Δ'</td><td>Ξ; Γ.Δ[v] ⊢ id<sub>Γ</sub>, ť[v] : Γ.Δ'[v]</td></tr><tr><td>Θ; Δ ⊢ t : Ξ'</td><td>Θ; Γ ⊢ t[v̄] : Ξ'</td><td>Ξ; Γ.Δ[v] ⊢ t[v] : Ξ'</td></tr></tbody></table>

**Proposition 4 (Substitution property).** The following rules are admissible.

$$ \frac{\Theta; \Gamma \vdash \vec{v} : \Delta \qquad \Theta; \Delta \vdash \mathcal{J}}{(\Theta; \Gamma \vdash \mathcal{J})[\vec{v}]} $$

$$ \frac{\Xi; \Gamma \vdash v : \Theta \qquad \Theta; \Delta \vdash \mathcal{J}}{(\Theta; \Delta \vdash \mathcal{J})[v]} $$

*Proof.* We illustrate the main case of the second statement's proof, which is by induction on $\Theta; \Delta \vdash \mathcal{J}$. Suppose the derivation ends with the rule MVAR.

$$ x\{\Delta'\} : T \in \Theta \frac{\Theta; \Delta \vdash \vec{t} : \Delta'}{\Theta; \Delta \vdash x\{\vec{t}\} : T[\vec{t}]} $$

By i.h. we have $Ξ; Γ.Δ[v] \vdash \mathrm{id}_Γ, \vec{t}[v] : Γ.Δ'[v]$. Moreover, from $Ξ; Γ \vdash v : Θ$ we can derive $Ξ; Γ.Δ'[v] \vdash v_× : T[v]$, so by the first statement (the substitution property for variable substitutions) we get $Ξ; Γ.Δ[v] \vdash v_×[\mathrm{id}_Γ, \vec{t}[v]] : T[v][\mathrm{id}_Γ, \vec{t}[v]]$. Because $x\{\vec{t}\}[v] = v_×[\mathrm{id}_Γ, \vec{t}[v]]$ and $T[\vec{t}][v] = T[v][\mathrm{id}_Γ, \vec{t}[v]]$ we are done.
**Proposition 5 (Sorts are well-typed).** The following rule is admissible when the underlying theory is valid.

$$ \frac{\Theta; \Gamma \vdash t : T}{\Theta; \Gamma \vdash T \text{ sort}} $$

*Proof.* By case analysis on $\Theta; \Gamma \vdash t : T$, and using Proposition 4. For rules CONS and DEST we use the validity of the theory to deduce $\Xi_1 \vdash T$ sort from $c(\Xi_1; \Xi_2) : T \in T$ and $\Xi_1.(x : T).\Xi_2 \vdash U$ sort from $d(\Xi_1; x : T; \Xi_2) : U \in T$.

**Proposition 6 (Conversion in context).** The following rule is admissible.

$$ \Gamma \equiv \Delta \frac{\Theta; \Gamma \vdash \mathcal{J}}{\Theta; \Delta \vdash \mathcal{J}} $$

## 3.4 Subject reduction

A key property that all of our valid theories satisfy is subject reduction. Aside from ensuring that well-typed programs cannot go wrong, this property will be vital to establish the soundness of the bidirectional type system.

In order to show subject reduction, we first need to prove some important properties of patterns. The first of them is injectivity with respect to conversion.

**Lemma 1 (Injectivity of patterns).** If $t \in Tm^P \theta \gamma$ and $t[v] \equiv t[v']$ for some $v \in MSub \theta' \delta \theta$ and $v' \in MSub \theta' \delta \theta$ then $v \equiv v'$.

*Proof.* By induction on the pattern, generalizing the statement also to metavariable substitution patterns. The key step is in case $c(t[v]) \equiv c(t[v'])$ in which we crucially rely on Proposition 1 to get $t[v] \equiv t[v']$ and invoke the i.h. to conclude.

Given a well-typed term $t$ such that the result of substituting $v$ in $t$ is also well-typed, generally we cannot conclude that the metavariable substitution $v$ is well-typed. This reasoning is however valid when $t$ is a pattern, as shown by the following result. Differently from the previous lemma, its proof is more intricate so instead of trying to give a proof sketch we refer to the technical report [24].

**Proposition 7 (Inversion of pattern typing).** Let $v \in MSub (\cdot) |\Delta| |\Theta|$.

- If $t \in Tm^P |\Theta| (\cdot)$ and $\Theta \vdash t : T$ and $\Delta \vdash t[v] : T[v]$ then $\Delta \vdash v : \Theta$

- If $T \in Tm^P |\Theta| (\cdot)$ and $\Theta \vdash T$ sort and $\Delta \vdash T[v]$ sort then $\Delta \vdash v : \Theta$

- If $t \in MSub^P |\Theta| (\cdot) |\Xi|$ and $\Theta \vdash t : \Xi$ and $\Delta \vdash t[v] : \Xi$ then $\Delta \vdash v : \Theta$

We are now ready to show subject reduction.

**Theorem 1 (Subject reduction).** Suppose that the underlying theory is valid.

- If $\Gamma \vdash T$ sort and $T \rightarrow T'$ then $\Gamma \vdash T'$ sort

- If $\Gamma \vdash t : T$ and $t \rightarrow t'$ then $\Gamma \vdash t' : T$

- If $\Gamma \vdash t : \Xi$ and $\Xi \vdash t$ and $t \rightarrow t'$ then $\Gamma \vdash t' : \Xi$
*Proof.* By induction on the rewrite judgment. We show only the main case:

$$ \frac{\theta_1; \theta_2 \models d(t; \mathbf{u}) \mapsto r \quad \mathbf{v}_1 \in \mathrm{MSub}(\cdot) |\Gamma| \theta_1 \quad \mathbf{v}_2 \in \mathrm{MSub}(\cdot) |\Gamma| \theta_2}{d(t[\mathbf{v}_1]; \mathbf{u}[\mathbf{v}_2]) \rightarrow r[\mathbf{v}_1, \mathbf{v}_2]} $$

Let $d(\Xi_1; x : U; \Xi_2) : V \in \mathbb{T}$ be the rule for $d$ in $\mathbb{T}$. Because $\mathbb{T}$ is valid, there are $\Theta_1$ and $\Theta_2$ with $|\Theta_1| = \theta_1$ and $|\Theta_2| = \theta_2$ such that

$$ \Xi_1.\Theta_1.\Theta_2 \vdash (\mathrm{id}_{\Xi_1}, t, \mathbf{u}) : \Xi_1.(x : U).\Xi_2 \quad \text{and} \quad \Xi_1.\Theta_1.\Theta_2 \vdash r : V[\mathrm{id}_{\Xi_1}, t, \mathbf{u}] $$

By inversion on $\Gamma \vdash d(t[\mathbf{v}_1]; \mathbf{u}[\mathbf{v}_2]) : T$ we get

$$ T \equiv V[\mathbf{v}_0, t[\mathbf{v}_1], \mathbf{u}[\mathbf{v}_2]] \frac{\Gamma \vdash \mathbf{v}_0, t[\mathbf{v}_1], \mathbf{u}[\mathbf{v}_2] : \Xi_1.(x : U).\Xi_2}{\Gamma \vdash d(t[\mathbf{v}_1]; \mathbf{u}[\mathbf{v}_2]) : V[\mathbf{v}_0, t[\mathbf{v}_1], \mathbf{u}[\mathbf{v}_2]]}{\Gamma \vdash d(t[\mathbf{v}_1]; \mathbf{u}[\mathbf{v}_2]) : T} $$

Therefore, we have $\Gamma \vdash (\mathrm{id}_{\Xi_1}, t, \mathbf{u})[\mathbf{v}_0, \mathbf{v}_1, \mathbf{v}_2] : \Xi_1.(x : U).\Xi_2$, and because $\mathrm{id}_{\Xi_1}, t, \mathbf{u} \in \mathrm{MSub}^P |\Xi_1.\Theta_1.\Theta_2| (\cdot) |\Xi_1.(x : U).\Xi_2|$, then by Proposition 7 we get $\Gamma \vdash \mathbf{v}_0, \mathbf{v}_1, \mathbf{v}_2 : \Xi_1.\Theta_1.\Theta_2$. By applying Proposition 4 with $\Xi_1.\Theta_1.\Theta_2 \vdash r : V[\mathrm{id}_{\Xi_1}, t, \mathbf{u}]$ we get $\Gamma \vdash r[\mathbf{v}_0, \mathbf{v}_1, \mathbf{v}_2] : V[\mathrm{id}_{\Xi_1}, t, \mathbf{u}][\mathbf{v}_0, \mathbf{v}_1, \mathbf{v}_2]$. Finally, we have $\Gamma \vdash T$ sort by Proposition 5 applied to $\Gamma \vdash d(t[\mathbf{v}_1]; \mathbf{u}[\mathbf{v}_2]) : T$, and because $r[\mathbf{v}_0, \mathbf{v}_1, \mathbf{v}_2] = r[\mathbf{v}_1, \mathbf{v}_2]$ and $V[\mathrm{id}_{\Xi_1}, t, \mathbf{u}][\mathbf{v}_0, \mathbf{v}_1, \mathbf{v}_2] = V[\mathbf{v}_0, t[\mathbf{v}_1], \mathbf{u}[\mathbf{v}_2]] \equiv T$ then by the conversion rule we conclude $\Gamma \vdash r[\mathbf{v}_1, \mathbf{v}_2] : T$.

# 4 Bidirectional type system

In the previous section we have defined the declarative type system. We now move to the bidirectional type system. We start the section by discussing the problem of matching modulo, which is needed for recovering missing arguments. We then introduce the inferable and checkable terms, for which the bidirectional system is defined. We then give the bidirectional typing rules and prove they are sound and complete with respect to the declarative type system. Finally, we use this equivalence to deduce some important properties of the declarative system.

## 4.1 Matching modulo rewriting

Suppose we want to type $@ (t; u)$ by first inferring the sort of $t$, yielding $T$. We know that the sort of the principal argument in the rule for $@$ is the pattern $\mathrm{Tm}(\Pi(A, x.B\{x\}))$, so we could hope to recover $A$ and $B$ by matching $T$ against this pattern. However, because of the conversion rule, in dependent type theories we cannot expect $T$ to be syntactically equal to an instance of this pattern, but only convertible to it. Therefore, our goal is instead to find $A$ and $B$ satisfying $\mathrm{Tm}(\Pi(A, x.B\{x\}))[A, x.B] \equiv T$. This shows that the process of recovering missing arguments in bidirectional typing is actually an instance of *matching modulo rewriting* — a connection that seems not to have been noted before in the literature. This also explains why we were careful in Subsection 2.4 to require the
sort of a constructor rule and the sort of the principle argument of a destructor rule to be patterns, as they need to support decidable and unitary matching.

In order to explain how to solve matching modulo problems, let us first recall some concepts about rewriting theory. A (*functional*) strategy $\mathcal{S}$ [11] is defined by a subrelation $\to^{\mathcal{S}} \subseteq \to^*$ which has the same normal forms as $\to$ and is functional in the sense that $t \to^{\mathcal{S}} u_1$ and $t \to^{\mathcal{S}} u_2$ imply $u_1 = u_2$. Let $m/o$ be the maximal outermost strategy, which contracts all outermost redexes in one step, and write $t \to_{m/o}^h c(\mathbf{u})$ if $c(\mathbf{u})$ is the first term headed by a constructor to which $t$ reduces by $\to_{m/o}^*$.

We can now define in Figure 3 an inference system for matching modulo rewriting, which given a pattern $t$ and a term $u$ tries to compute a variable substitution $v$ such that $t[v] \equiv u$. Note that the use of a specific rewriting strategy is necessary to ensure the functionality of the inference system.

<figure><img src="image_4.png" /><figcaption>**Fig. 3.** Inference system for matching modulo</figcaption></figure>

Let us now establish the correctness of this inference system in three steps. We first show its soundness, which follows by an easy induction on the derivation.

**Proposition 8 (Soundness of matching).**

- If $t < u \to v$ then $u \to^* t[v]$.

- If $t < u \to v$ then $u \to^* t[v]$.

In order to show completeness we first have to answer the following question: if $t \equiv c(\mathbf{u})$, are we sure that by reducing $t$ we eventually reach a term headed by $c$? The answer would be no, had we taken for instance an innermost strategy. Thankfully, because the rewrite systems of our theories are both orthogonal and *fully-extended*, it follows by [39, Theorem 2] that the maximal-outermost strategy we are using is *head-normalizing*, and so we have the following property.

**Lemma 2.** If $u \equiv c(t)$ then $u \to_{m/o}^h c(u)$ with $t \equiv u$.
Using Lemma 2, we can now show completeness by induction on the pattern.

**Proposition 9 (Completeness of matching).**

- If $t[v] \equiv u$ for some $v \in \mathbf{MSub}(\cdot) \delta \theta$ then $t < u \rightsquigarrow v'$ for some $v' \equiv v$

- If $t[v] \equiv u$ for some $v \in \mathbf{MSub}(\cdot) \delta \theta$ then $t < u \rightsquigarrow v'$ for some $v' \equiv v$

Recall that an expression is weak normalizing if it reduces to a normal form. We can now show that the inference system is decidable when being used with weak normalizing expressions. The proof is by induction on the pattern, using the fact that m/o is normalizing [42, Theorem 10], so that reducing a weak normalizing term with m/o always terminates.

**Proposition 10 (Decidability of matching).**

- If $u$ is weak normalizing, then $\exists v. t < u \rightsquigarrow v$ is decidable for all $t$.

- If $u$ is weak normalizing, then $\exists v. t < u \rightsquigarrow v$ is decidable for all $t$.

## 4.2 Inferable and checkable terms

Before giving the bidirectional typing rules, we first have to address the problem that some terms without annotations cannot be algorithmically typed. Suppose for instance that we want to type the term $@(\lambda(x.t); u)$ by inferring the sort of the principal argument of @ to recover A and B. But because $\lambda(x.t)$ is headed by a constructor it can only be bidirectionally typed in mode check, so we are stuck. One could think that this limitation is specific to bidirectional typing, however a famous result by Dowek shows that, in a dependently-typed setting, the problem of typing unannotated terms is actually undecidable in its full generality [18].

To solve this issue, we have two options. We could proceed as in the COQ literature [33] and add extra annotations to terms so that they can always be inferred. For instance, we would then need to annotate abstraction with its domain by writing $\lambda(A, x.t)$ instead of $\lambda(x.t)$. However, not only this solution makes the syntax heavier, but by abandoning the constructor/destructor separation in which constructors are always typed in mode check, it yields typing rules which are much less symmetric and whose form seems difficult to specify in a generic way.

We instead take the choice made by most of the dependent bidirectional typing literature [2,38,1,16,3,4] and define our bidirectional system only for a subset of expressions, the *checkable and inferable terms* and the *checkable *metavariable* substitutions*. Given a fixed signature $\Sigma$, they are defined as follows.

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\boxed{\mathbf{Tm}^i \gamma} \ni t, u, v ::= & |x & \text{if } x \in \gamma \\
& | d(t \in \mathbf{Tm}^i \gamma; t \in \mathbf{MSub}^c \gamma \xi) & \text{if } d(\xi) \in \Sigma \\
\boxed{\mathbf{Tm}^c \gamma} \ni t, u, v ::= & |c(t \in \mathbf{MSub}^c \gamma \xi) & \text{if } c(\xi) \in \Sigma \\
& |\underline{t} \in \mathbf{Tm}^i \gamma & \\
\boxed{\mathbf{MSub}^c \gamma \xi} \ni t, u, v ::= & |\varepsilon & \text{if } \varepsilon = \cdot \\
& |\mathbf{t}' \in \mathbf{MSub}^c \gamma \xi', \vec{x}_{\delta,t} \in \mathbf{Tm}^c \gamma.\delta & \text{if } \xi = \xi', x\{\delta\}
\end{array}
$$
Let us go through the definition. An inferable term is either a variable or a destructor whose principal argument is inferable, and whose other arguments are given by a checkable metavariable substitution. Imposing the principal argument to be inferable is the key restriction to rule out terms like @($\lambda(x.t);u$). A checkable term is then either a constructor applied to a checkable metavariable substitution, or an underlined inferable term. Finally, a checkable metavariable substitution is just a metavariable substitution containing only checkable terms.

*Example 9.* The inferrable and checkable terms for the signature $\Sigma_{\lambda\Pi}$ are given respectively by the following grammars, where we omit the scope information.

$$ 
\begin{align*}
t^i, u^i &::= x \mid @ (t^i; u^c) \\
t^c, u^c, A^c, B^c &::= \textcolor{blue}{Ty} \mid \textcolor{blue}{Tm}(A^c) \mid \textcolor{blue}{\Pi}(A^c, x.B^c) \mid \lambda(x.t^c) \mid \underline{t^i}
\end{align*}
$$

One could wonder if restricting the terms that can be algorithmically typed is a significant limitation. For most usual theories (like $T_{\lambda\Pi}$ and those in Section 5) the checkable terms coincide with the normal forms, and the inferable terms coincide with the neutrals. As argued in other works [38,1], users of type theory almost only write terms in normal form, and in the few cases writing a redex is more convenient, in actual implementations the principal argument can always be lifted to a top-level definition. Therefore, this restriction, also present in most of the dependent bidirectional typing literature [2,38,1,16,3,4], does not pose a serious limitation in practice.

Note also that inferable and checkable terms have no metavariables. Even if metavariables are needed in the declarative system to be able to say which theories are valid, when writing terms in a fixed theory metavariables are generally not needed, and hence they are omitted from usual presentations of type theories. It is therefore reasonable to leave them out of the bidirectional syntax, as they will be of no use for users.

Given $t \in Tm^c$ $\gamma$ or $t \in Tm^i$ $\gamma$ we write $\Gamma t \Gamma \in Tm$ ($\cdot$) $\gamma$ for its underlying term, and for $t \in MSub^c$ $\gamma \xi$ we also write $\Gamma t \Gamma \in MSub$ ($\cdot$) $\gamma \xi$ for its underlying metavariable substitution.

## 4.3 Bidirectional typing rules

Given a theory $T$, we can now define its bidirectional type system by the rules in Figure 4. The system is split in 4 judgments:

- $\Gamma \vdash T \equiv \textcolor{blue}{sort}$ : Checking that a checkable term $T$ is a well-formed sort

- $\Gamma \vdash t \equiv T$ : Checking that a checkable term $t$ has sort $T$

- $\Gamma \vdash t \Rightarrow T$ : Inferring a sort $T$ for an inferable term $t$

- $\Gamma | v : \Xi \vdash t \equiv \Theta$ : Checking that a checkable metavariable substitution $t$ can be typed by $\Theta$ "to the right" of $v : \Xi$

As in the declarative system, the most important rules are the one that instantiate the schematic typing rules: CONST, DEST and SORT. However, differently from the declarative system, no more guessing is needed when building
$$ \Gamma \vdash t \Leftrightarrow T \quad (\Gamma \in \mathrm{Ctx}; T \in \mathrm{Tm}(\cdot) |\Gamma|; t \in \mathrm{Tm}^c |\Gamma|) $$

$$ c(\Xi_1; \Xi_2) : T \in \mathbb{T} \quad \frac{T < U \rightsquigarrow \mathbf{v} \quad \Gamma | \mathbf{v} : \Xi_1 \vdash \mathbf{u} \Leftarrow \Xi_2}{\Gamma \vdash c(\mathbf{u}) \Leftarrow U} $$

$$ T \equiv_T U \frac{\Gamma \vdash t \Rightarrow T}{\Gamma \vdash t \Leftarrow U} $$

$$ \Gamma \vdash t \Rightarrow T \quad (\Gamma \in \mathrm{Ctx}; T \in \mathrm{Tm}(\cdot) |\Gamma|; t \in \mathrm{Tm}^i |\Gamma|) $$

$$ d(\Xi_1; x : T; \Xi_2) : U \in \mathbb{T} \quad \frac{\Gamma | (\mathbf{v}, \lceil t \rceil) : (\Xi_1, x : T) \vdash \mathbf{u} \Leftarrow \Xi_2}{\Gamma \vdash d(t; \mathbf{u}) \Rightarrow U[\mathbf{v}, \lceil t \rceil, \lceil \mathbf{u} \rceil]} $$

$$ x : T \in \Gamma \quad \frac{\mathrm{VAR}}{\Gamma \vdash x \Rightarrow T} $$

$$ \Gamma \vdash T \Leftrightarrow \mathrm{sort} \quad (\Gamma \in \mathrm{Ctx}; T \in \mathrm{Tm}^c |\Gamma|) $$

$$ c(\Xi) \text{ sort} \in \mathbb{T} \quad \frac{\Gamma | \varepsilon : (\cdot) \vdash t \Leftarrow \Xi}{\Gamma \vdash c(t) \Leftarrow \text{sort}} $$

$$ \Gamma | \mathbf{v} : \Theta \vdash t \Leftarrow \Xi \quad \left( \begin{array}{l} \Gamma \in \mathrm{Ctx}; \Theta \in \mathrm{MSub}(\cdot) |\Gamma| |\Theta|; \\ \Xi \in \mathrm{MCTX} |\Theta|; \mathbf{t} \in \mathrm{MSub}^c |\Gamma| |\Xi| \end{array} \right) $$

$$ \frac{\mathrm{EMPTYMSUB}}{\Gamma | \mathbf{v} : \Theta \vdash \varepsilon \Leftarrow (\cdot)} $$

$$ \frac{\mathrm{EXTMSUB}}{\Gamma | \mathbf{v} : \Theta \vdash t \Leftarrow \Xi \quad \Gamma \Delta[\mathbf{v}, \lceil t \rceil] \vdash t \Leftarrow T[\mathbf{v}, \lceil t \rceil]} \quad \Gamma | \mathbf{v} : \Theta \vdash t, \vec{x}_{\Delta,t} \Leftarrow (\Xi, x\{\Delta\} : T) $$

<caption>**Fig. 4.** Bidirectional typing rules</caption>

a type derivation. For instance, when using rule DEST with $d(t; \mathbf{u})$ the omitted arguments are no longer guessed, but instead recovered by inferring the sort of the principal argument $t$ and then matching it against the associated pattern.

*Example 10.* Suppose we want to infer a sort for $@ (t; u)$ in the theory $T_{\Delta\Pi}$. To use rule DEST, we start by inferring a sort $V$ for $t$, and then we try to match it against the pattern $\mathrm{Tm}(\Pi(A, x.B\{x\}))$. If matching succeeds, we recover the arguments $A$ and $B$, which together with $t$ are then used in

$$ \Gamma | (A, x.B, x. \lceil t \rceil) : (A : \mathrm{Ty}, B\{x : \mathrm{Tm}(A)\} : \mathrm{Ty}, t : \dots) \vdash (u) \Leftarrow (u : \mathrm{Tm}(A)) $$

where we omit the sort of $t$ for lack of space. By applying the rules that define the judgment $\Gamma | \mathbf{v} : \Theta \vdash t \Leftarrow \Xi$, we see that this amounts to showing just $\Gamma \vdash u \Leftarrow \mathrm{Tm}(A)$, and so the final shape of this "big-step derivation" is the following, which corresponds to the usual bidirectional rule for application.

$$ \frac{\Gamma \vdash t \Rightarrow V \qquad \mathrm{Tm}(\Pi(A, x.B\{x\})) < V \rightsquigarrow A, x.B \qquad \Gamma \vdash u \Leftarrow \mathrm{Tm}(A)}{\Gamma \vdash @ (t; u) \Rightarrow \mathrm{Tm}(B[\mathrm{id}_{\Gamma}, \lceil u \rceil])} $$
## 4.4 Equivalence with declarative typing

We now establish the equivalence between the declarative and bidirectional type systems. This is done in two steps, the first one being soundness:

**Theorem 2 (Soundness).** Suppose that the underlying theory $\mathcal{T}$ is valid.

1. If $\Gamma \vdash$ and $\Gamma \vdash t \Rightarrow T$ then $\Gamma \vdash \Gamma^t : T$

2. If $\Gamma \vdash T$ sort and $\Gamma \vdash t \Leftarrow T$ then $\Gamma \vdash \Gamma^t : T$

3. If $\Gamma \vdash$ and $\Gamma \vdash T \Leftarrow$ sort then $\Gamma \vdash \Gamma^T$ sort

4. If $\Gamma \vdash v : \Xi_1$ and $\Xi_1 \vdash v : \Xi_2$ and $\Gamma \vdash v : \Xi_1 \vdash t \Leftarrow \Xi_2$ then $\Gamma \vdash v, \Gamma^t : \Xi_1 \Xi_2$.

*Proof.* By induction on the derivation. We illustrate one of the interesting cases.

$$c(\Xi_1; \Xi_2) : T \in \mathcal{T} \frac{T < U \rightsquigarrow v \quad \Gamma \mid v : \Xi_1 \vdash u \Leftarrow \Xi_2}{\Gamma \vdash c(u) \Leftarrow U}$$

By Proposition 8 we have $U \to^* T[v]$, so because we have $\Gamma \vdash U$ sort then by Theorem 1 we get $\Gamma \vdash T[v]$ sort. We have $T \in \Gamma^m \mid \Xi_1| (\cdot)$, and validity of the theory also gives $\Xi_1 \vdash T$ sort, therefore by Proposition 7 we get $\Gamma \vdash v : \Xi_1$. By validity of the theory we also have $\Xi_1 \Xi_2 \vdash$, therefore by applying the i.h. to the second premise we get $\Gamma \vdash v, \Gamma^u : \Xi_1 \Xi_2$. We can then derive $\Gamma \vdash c(\Gamma^u) : T[v]$, and because $T[v] \equiv U$ and $\Gamma \vdash U$ sort, by conversion we conclude $\Gamma \vdash c(\Gamma^u) : U$.

Completeness then asserts that checkable/inferable terms typable in the declarative system can also be typed in the bidirectional system.

**Theorem 3 (Completeness).** Suppose that the underlying theory $\mathcal{T}$ is valid.

1. If $t$ is inferable and $\Gamma \vdash \Gamma^t : T$ then $\Gamma \vdash t \Rightarrow T'$ with $T \equiv T'$

2. If $t$ is checkable and $\Gamma \vdash \Gamma^t : T$ then we have $\Gamma \vdash t \Leftarrow T$

3. If $t$ is checkable and $\Gamma \vdash \Gamma^T$ sort then $\Gamma \vdash T \Leftarrow$ sort

4. If $t$ is checkable and $\Gamma \vdash v, \Gamma^t : \Theta \Xi$ then we have $\Gamma \vdash v : \Theta \vdash t \Leftarrow \Xi$

*Proof.* The proof requires us to strengthen the statement, so the two occurrences of the context $\Gamma$ in points 1-4, of the sort $T$ in point 2 and of the substitution $v$ in point 4 are not required to be syntactically equal, but only convertible (see the technical report [24] for the exact statement). The proof is then by induction on the checkable/inferable term or checkable substitution.

We illustrate the case $t = d(u; t)$, in which we have to show that for all $\Gamma' \equiv \Gamma$ we have some $T' \equiv T$ such that $\Gamma' \vdash t \Rightarrow T'$. By inversion on $\Gamma \vdash \Gamma^t : T$ we have

$$d(\Xi_1; x : U; \Xi_2) : V \in \mathcal{T} \frac{\Gamma \vdash v, \Gamma^u, \Gamma^t : \Xi_1 \cdot (x : U) \Xi_2}{T \equiv V[v, \Gamma^u, \Gamma^t] \frac{\Gamma \vdash d(\Gamma^u; \Gamma^t) : V[v, \Gamma^u, \Gamma^t]}{\Gamma \vdash d(\Gamma^u; \Gamma^t) : T}}$$

Let $\Gamma' \equiv \Gamma$. From $\Gamma \vdash v, \Gamma^u, \Gamma^t : \Xi_1 \cdot (x : U) \Xi_2$ we get $\Gamma \vdash \Gamma^u : U[v]$, so because $u$ is inferrable, by the i.h. we obtain that for some $U' \equiv U[v]$ we have $\Gamma' \vdash u \Rightarrow U'$. By Proposition 9 we then get $U < U' \rightsquigarrow v'$ with $v \equiv v'$. Then, because $t$ is checkable and $\Gamma \equiv \Gamma'$ and $v, \Gamma^u \equiv v', \Gamma^u$, by the i.h. we derive $\Gamma' \mid (v', \Gamma^u) : (\Xi_1, x : U) \vdash t \Leftarrow \Xi_2$. Putting all this together, we conclude $\Gamma' \vdash d(u; t) \Rightarrow V[v', \Gamma^u, \Gamma^t]$, where we have $V[v', \Gamma^u, \Gamma^t] \equiv T$ as required.
## 4.5 Consequences of the equivalence

We now explore the established equivalence in order to show two important properties: decidability of typing and uniqueness of sorts.

We say that a theory $\mathcal{T}$ is weak normalizing if for all expressions $e$ with $\Gamma \vdash e$ sort or $\Gamma \vdash e : T$ or $\Gamma \vdash e : \Xi$ we have that $e$ is weak normalizing.

**Theorem 4 (Decidability of typing).** Suppose that the underlying theory $\mathcal{T}$ is valid and weak normalizing.

1. If $t$ is inferable and $\Gamma \vdash$ then the statement $\exists T. (\Gamma \vdash \Gamma^t : T)$ is decidable.

2. If $t$ is checkable and $\Gamma \vdash T$ sort then the statement $\Gamma \vdash \Gamma^t : T$ is decidable.

3. If $T$ is checkable and $\Gamma \vdash$ then the statement $\Gamma \vdash \Gamma^T$ sort is decidable.

4. If $t$ is checkable and $\Theta.\Xi \vdash$ and $\Gamma \vdash v : \Theta$ then the statement $\Gamma \vdash v, \Gamma^t : \Theta.\Xi$ is decidable.

*Proof.* We first show the corresponding statement for the bidirectional system, using Proposition 10, Theorem 2 and the decidability of conversion for well-typed terms (which follows from weak normalization). By Theorems 2 and 3 we can then conclude. We refer to the technical report [24] for the proof.

We now move to uniqueness of sorts. First note that, because our terms are non-annotated, uniqueness of sorts does not hold in general: for instance, $\lambda(x.x)$ can be typed by $\mathbf{Tm}(\Pi(A,x.A))$ in context $\Gamma$ for any $A$ with $\Gamma \vdash A : \mathbf{Ty}$. Nevertheless, we can still show uniqueness of sorts for inferable terms:

**Theorem 5 (Uniqueness of sorts).** Suppose that the underlying theory $\mathcal{T}$ is valid. If $t$ is inferable and $\Gamma \vdash \Gamma^t : T$ and $\Gamma \vdash \Gamma^t : U$ then $T \equiv U$.

*Proof.* By Theorem 3 we get $\Gamma \vdash t \Rightarrow T'$ with $T \equiv T'$ from $\Gamma \vdash \Gamma^t : T$ and $\Gamma \vdash t \Rightarrow U'$ with $U \equiv U'$ from $\Gamma \vdash \Gamma^t : U$. We can show type inference to be functional, so we get $T' = U'$ and thus $T \equiv U$.

# 5 More examples

In the previous sections we have illustrated our framework with the theory $\mathcal{T}_{\Lambda\Pi}$, defining a basic Martin-Löf Type Theory with dependent products. We now show other examples of valid theories to showcase the generality of our framework. Throughout this section, we use the informal notation for schematic typing rules discussed in Subsection 2.4, for readability purposes. We refer to the files of the implementation [23] for more details.

*Lists* We can define lists by extending $\mathcal{T}_{\Lambda\Pi}$ with the following.

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \vdash A : \mathbf{Ty} & \vdash x : \mathbf{Tm}(A) & \\ \vdash \mathbf{List}(A) : \mathbf{Ty} & \vdash l : \mathbf{Tm}(\mathbf{List}(A)) & \\ \vdash A : \mathbf{Ty} & \vdash \mathbf{cons}(x, l) : \mathbf{Tm}(\mathbf{List}(A)) & \end{array} $$

$$ \begin{array}{l} \vdash A : \mathbf{Ty} \qquad \vdash l : \mathbf{Tm}(\mathbf{List}(A)) \qquad x : \mathbf{Tm}(\mathbf{List}(A)) \vdash \mathbf{P} : \mathbf{Ty} \qquad \vdash \mathbf{pnil} : \mathbf{Tm}(\mathbf{P}\{\mathbf{nil}\}) \\ x : \mathbf{Tm}(A), y : \mathbf{Tm}(\mathbf{List}(A)), z : \mathbf{Tm}(\mathbf{P}\{y\}) \vdash \mathbf{pcons} : \mathbf{Tm}(\mathbf{P}\{\mathbf{cons}(x, y)\}) \\ \multicolumn{4}{c}{\vdash \mathbf{ListRec}(l; \mathbf{P}, \mathbf{pnil}, \mathbf{pcons}) : \mathbf{Tm}(\mathbf{P}\{l\})} \end{array} $$
$$
\begin{align*}
\texttt{ListRec}(\texttt{nil}; x.P\{x\}, \texttt{pnil}, xyz.pcons\{x, y, z\}) &\mapsto \texttt{pnil} \\
\texttt{ListRec}(\texttt{cons}(x, l); x.P\{x\}, \texttt{pnil}, xyz.pcons\{x, y, z\}) &\mapsto \\
&\qquad pcons\{x, l, \texttt{ListRec}(l; x.P\{x\}, \texttt{pnil}, xyz.pcons\{x, y, z\})\}
\end{align*}
$$

Like one would wish, the constructors `nil` and `cons` indeed do not store the type annotation `A`, which is recovered from the sort. This annotation is also elided in the destructor `ListRec`, where it is recovered from the principal argument.

In general, we can extend the theory with any (non-indexed) inductive type.
For instance, see the file `mltt.bitt` where we add dependent sums and W types.

*Universes* We can define *Tarski-style* universes by extending $T_{\lambda\Pi}$ with a type $U$
and a decoding function mapping each inhabitant $a$ of $U$ into a type $El(a; \varepsilon)$.

$$
\begin{array}{c}
\vdash U : Ty \\
\hline
\end{array}
\qquad
\begin{array}{c}
\vdash a : Tm(U) \\
\hline
\end{array}
$$

We then add a code for each type of the theory, with an associated rewriting
rule stating that the code is decoded by El into the appropriate type.

$$
\begin{array}{c}
\vdash u : Tm(U) \\
\hline
\end{array}
\qquad
\begin{array}{c}
\vdash a : Tm(U) & x : Tm(El(a; \epsilon)) \vdash b : Tm(U) \\
\vdash \pi(a, b) : Tm(U) & \\
\hline
\end{array}
$$

This specifies a type in type universe, which is known to be inconsistent [15].
This can however be easily fixed by stratifying universes into a hierarchy. By
doing this, we can then define a Tarski-style variant of (functional) *Pure Type
Systems* [9]. Alternatively, instead of using Tarski-style we can also define (weak)
*Coquand-style universes* [17,30,32,6] which require replacing the sorts *Ty* and
*Tm* by indexed families *Ty*ᵢ and *Tm*ᵢ — see the file *mltt-coquand.bitt* for a
definition also featuring (weak) cumulativity and universe polymorphism.

*Higher-order logic* We have seen how to extend $T_{\lambda\Pi}$ with various type formers,
however we can also define logics. To define higher-order logic (HOL) we first de-
clare a type of propositions and a sort rule to represent the judgment "P is true".

$$
\begin{array}{c}
\vdash \text{Prop} : \text{Ty} \\
\hline
\end{array}
\qquad
\begin{array}{c}
\vdash \text{P} : \text{Tm}(\text{Prop}) \\
\hline
\end{array}
$$

We can then add connectors or quantifiers such as the universal quantifier $\forall$ —
see the file `hol.bitt` for more details.

$$
\begin{array}{c}
\vdash A : Ty \\
\hline
x : Tm(A) \vdash P : Tm(Prop) \\
\vdash \forall (A, P) : Tm(Prop) \\
\hline
\end{array}
\qquad
\begin{array}{c}
\vdash A : Ty & x : Tm(A) \vdash P : Tm(Prop) \\
\hline
x : Tm(A) \vdash p : Prf(P) \\
\hline
\end{array}
$$
$$
\begin{array}{c}
\vdash A : Ty & x : Tm(A) \vdash P : Tm(Prop) \\
\vdash r : Prf(\forall (A, x.P\{x\})) & \vdash t : Tm(A) \\
\hline
\end{array}
$$
$$
\forall \text{el}(\forall \text{in}(x.p\{x\}); t) \mapsto p\{t\}
$$
# 6 Related work

Our general definition of dependent type theories draws much inspiration from other frameworks for type theory, such as GATs/QIITs [13,7,31], SOGATs [45], FTTs [29], and logical frameworks such as Dedukti [8,12] and Harper's Equational LF [27]. However, we differ from these works by supporting non-annotated syntaxes and enforcing a constructor/destructor separation of symbols and rules, both of which seem to be important ingredients for bidirectional typing.

Another point of divergence from these frameworks is that most of them allow the use of arbitrary equations when defining the definitional equality of theories. However, it then becomes hard to give an implementation, as it would require deciding arbitrary equational theories. We instead take the approach of Dedukti of supporting only rewrite rules, which allows to decide the definitional equality of theories in a uniform manner, and makes it possible to implement our framework. A different approach is taken in Andromeda, an implementation of FTTs, where they also allow for extensionality rules [10]. They however provide no proof of completeness for their equality-checking algorithm.

Our proposal also draws inspiration from the works of McBride, a main advocate of dependent bidirectional typing. His ongoing work on a framework for bidirectional typing [35,36] shares many similarities with ours, for instance by adopting a constructor/destructor separation of rules. However, an important difference with our framework is that he takes the bidirectional type system as the definition of the theory. Therefore, there is no discussion on how to show soundness and completeness with respect to a declarative system, as the bidirectional one is the only type system defined in his setting. This approach differs from most of the literature on dependent bidirectional typing [19,2,33,1,3,4], in which one first defines the type theory by a "platonic" declarative type system and then shows it equivalent to a bidirectional system which can be implemented. Finally, this choice also makes the metatheoretic study of theories quite different: for instance, in order for the bidirectional system to satisfy subject reduction he is obliged to introduce type ascriptions in the syntax.

Another work from which ours drew inspiration is the one of Reed [43], where he proposes a variant of the Edinburgh Logical Framework in which arguments can be omitted. Crucially, these arguments are not elaborated through global unification, but instead locally recovered by annotating each declaration with modes to guide a bidirectional algorithm. However, his framework does not allow for extending the definitional equality, meaning that one cannot define dependent type theories directly, but instead has to encode its derivations trees (as in [28]). This also means that his system does not need to deal with some complications that arise in our more general setting, such as matching modulo.

Finally, concurrently to our work, Chen and Ko [14] have proposed a framework for simply-typed bidirectional typing. They also define declarative and bidirectional systems and establish a correspondence between them. Compared to our work, their restriction to simple types removes many of the complexities that appear in dependent type theories. For instance, while their types are first-order terms with no notion of computation or typing, our sorts are higher-order terms.
terms considered modulo a set of rewrite rules and subject to typing judgments, making the process of recovering missing arguments much more intricate. They however formalize all their proofs in Agda.

# 7 Conclusion and future work

In this work we have given a generic account of bidirectional typing for a general class of dependent type theories. Our main results, Theorems 2 and 3, establish an equivalence between declarative and bidirectional type systems for a general class of theories. The underlying algorithm of Theorem 4, establishing the decidability of typing for weak normalizing theories, has been implemented in a prototype further described in an accompanying experience report [22]. Compared to other theory-independent typecheckers, such as Dedukti, its support for unannotated syntaxes should allow for better performances, which can make it a good candidate for cross-checking real proof libraries.

Regarding future work, the most important omission that we would like to address is that of inductive families. Indeed, these do not fit our definitions because their constructor's sorts either are non-linear patterns (as in the constructor for equality) or contain VARIABLES for arguments that are computationally relevant and thus cannot be omitted (as in the cons constructor for vectors).

Moreover, even if our system builds heavily on the constructor/destructor distinction in type theory, some few constructions do not respect this separation. For instance, to define Russell universes we need the rewrite rule $Tm(U) \leftrightarrow Ty$ [44], which is not valid as $Tm$ is not a destructor. Whether there is a way of accommodating these constructions without fully abandoning the constructor/destructor separation is something we would like to investigate in future work.

A long term goal is also to extend our framework to account for type-directed equality rules, which are needed for handling $\eta$-laws and definitional proof irrelevance. Even if it is well known how to design complete equality checking algorithms for specific theories with type-directed equalities [5], doing so in a general setting like ours seems to be an important challenge. We could take inspiration from the customizable equality-checking algorithm implemented in Andromeda [10]. However, as mentioned in the previous section, their algorithm is not proven complete, so further research in this direction seems to be needed.

*Acknowledgements* The author thanks Gilles Dowek, Vincent Moreau, Théo Winterhalter for helpful remarks on a preliminary version of this paper, Meven Lennon-Bertrand, Jesper Cockx, András Kovács for informative discussions about bidirectional typing, and Frédéric Blanqui for valuable remarks about this work.

*Data-Availability Statement* The implementation associated with this work is available online [23] and is described in an accompanying experience report [22].
References

1. Abel, A., Altenkirch, T.: A partial type checking algorithm for type: Type. Electronic Notes in Theoretical Computer Science 229(5), 3–17 (2011)

2. Abel, A., Coquand, T.: Untyped algorithmic equality for martin-löf's logical framework with surjective pairs. In: Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings 7. pp. 23–38. Springer (2005)

3. Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Logical Methods in Computer Science 7 (2011)

4. Abel, A., Vezzosi, A., Winterhalter, T.: Normalization by evaluation for sized dependent types. Proceedings of the ACM on Programming Languages 1(ICFP), 1–30 (2017)

5. Abel, A., Öhman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. Proceedings of the ACM on Programming Languages 2(POPL), 1–29 (Jan 2018). https://doi.org/10.1145/3158111, https://dl.acm.org/doi/10.1145/3158111

6. Altenkirch, T., Boulier, S., Kaposi, A., Tabareau, N.: Setoid type theory—a syntactic translation. In: Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings 13. pp. 155–196. Springer (2019)

7. Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 18–29. POPL ’16, Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/2837614.2837638, https://doi.org/10.1145/2837614.2837638

8. Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Dedukti: a logical framework based on the $\lambda\pi$-calculus modulo theory (2016), unpublished

9. Barendregt, H.P., Dekkers, W., Statman, R.: Lambda calculus with types. Cambridge University Press (2013)

10. Bauer, A., Komel, A.P.: An extensible equality checking algorithm for dependent type theories. Log. Methods Comput. Sci. 18(1) (2022). https://doi.org/10.46298/lmcs-18(1:17)2022, https://doi.org/10.46298/lmcs-18(1:17)2022

11. Bezem, M., Klop, J., de Vrijer, R., Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2003), https://books.google.fr/books?id=7QQ5u-4tRUkC

12. Blanqui, F., Dowek, G., Grienenberger, É., Hondet, G., Thiré, F.: Some axioms for mathematics. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference). LIPIcs, vol. 195, pp. 20:1–20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.FSCD.2021.20, https://doi.org/10.4230/LIPIcs.FSCD.2021.20

13. Cartmell, J.: Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic 32, 209–243 (1986). https://doi.org/10.1016/0168-0072(86)90053-9, https://www.sciencedirect.com/science/article/pii/0168007286900539

14. Chen, L.T., Ko, H.S.: A formal treatment of bidirectional typing (2024)

15. Coquand, T.: An analysis of Girard's paradox. Tech. Rep. RR-0531, INRIA (May 1986), https://inria.hal.science/inria-00076023
16. Coquand, T.: An algorithm for type-checking dependent types. Science of Computer Programming **26**(1-3), 167–177 (1996)

17. Coquand, T.: Canonicity and normalisation for dependent type theory. arXiv preprint arXiv:1810.09367 (2018)

18. Dowek, G.: The undecidability of typability in the lambda-pi-calculus. In: International Conference on Typed Lambda Calculi and Applications. pp. 139–145. Springer (1993)

19. Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Computing Surveys (CSUR) **54**(5), 1–38 (2021)

20. Dunfield, J., Pfenning, F.: Tridirectional typechecking. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 281–292. POPL ’04, Association for Computing Machinery, New York, NY, USA (2004). https://doi.org/10.1145/964001.964025, https://doi.org/10.1145/964001.964025

21. Felicissimo, T.: Adequate and Computational Encodings in the Logical Framework Dedukti. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 25:1–25:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2022). https://doi.org/10.4230/LIPIcs.FSCD.2022.25, https://drops.dagstuhl.de/opus/volltexte/2022/16306

22. Felicissimo, T.: Artifact report: Generic bidirectional typing for dependent type theories (2024)

23. Felicissimo, T.: BiTTs (Jan 2024). https://doi.org/10.5281/zenodo.10500598, https://doi.org/10.5281/zenodo.10500598

24. Felicissimo, T.: Generic bidirectional typing for dependent type theories (Technical Report) (2024), https://inria.hal.science/hal-04270368/file/tech.pdf

25. Gratzer, D., Sterling, J., Birkedal, L.: Implementing a modal dependent type theory. Proceedings of the ACM on Programming Languages **3**(ICFP), 1–29 (2019)

26. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM **40**(1), 143–184 (1993)

27. Harper, R.: An equational logical framework for type theories. arXiv preprint arXiv:2106.01484 (2021)

28. Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. Journal of functional programming **17**(4-5), 613–673 (2007)

29. Haselwarter, P.G., Bauer, A.: Finitary type theories with and without contexts. arXiv preprint arXiv:2112.00539 (2021)

30. Kaposi, A., Huber, S., Sattler, C.: Gluing for type theory. In: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)

31. Kaposi, A., Kovács, A., Altenkirch, T.: Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. **3**(POPL) (jan 2019). https://doi.org/10.1145/3290315, https://doi.org/10.1145/3290315

32. Kovács, A.: Staged compilation with two-level type theory. Proceedings of the ACM on Programming Languages **6**(ICFP), 540–569 (2022)

33. Lennon-Bertrand, M.: Complete Bidirectional Typing for the Calculus of Inductive Constructions. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 24:1–24:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021). https://doi.org/10.4230/LIPIcs.ITP.2021.24, https://drops.dagstuhl.de/opus/volltexte/2021/13919
34. Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical computer science 192(1), 3–29 (1998)

35. McBride, C.: Basics of bidirectionalism. https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/ (2018)

36. McBride, C.: Types who say ni. https://github.com/pigworker/TypesWhoSayNi/ (2022)

37. Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic (TOCL) 9(3), 1–49 (2008)

38. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden (September 2007)

39. van Oostrom, V.: Normalisation in weakly orthogonal rewriting. In: International Conference on Rewriting Techniques and Applications. pp. 60–74. Springer (1999)

40. Pfenning, F.: Logical frameworks. Handbook of automated reasoning 2, 1063–1147 (2001)

41. Pierce, B.C., Turner, D.N.: Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS) 22(1), 1–44 (2000)

42. van Raamsdonk, F.: Outermost-fair rewriting. In: International Conference on Typed Lambda Calculi and Applications. pp. 284–299. Springer (1997)

43. Reed, J.: Redundancy elimination for lf. Electronic Notes in Theoretical Computer Science 199, 89–106 (2008)

44. Sterling, J.: Algebraic type theory and universe hierarchies. arXiv preprint arXiv:1902.08848 (2019)

45. Uemura, T.: Abstract and concrete type theories. Ph.D. thesis, University of Amsterdam (2021)