Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation

MLTT is a dependent type theory presented by five mutually defined judgements, characterizing well-formed context $⊢\mathrm{\Gamma }$, types $\mathrm{\Gamma }⊢A$ and terms $\mathrm{\Gamma }⊢t:A$, and asserting that two terms (resp. types) are convertible or definitionally equal $\mathrm{\Gamma }⊢A\equiv A^{\prime }$ (resp. $\mathrm{\Gamma }⊢t\equiv t^{\prime }:A$). During type-checking we need to compare (dependent) types, which can contain terms. Thus, equations between the latter can appear when comparing the former, meaning we have to decide conversion between arbitrary terms.

MLTT is a language with binders, represented with names in the text for readability. In the implementation, the front language has names, but internally we use de Bruijn indices for terms and de Bruijn levels for semantic values, as is standard for NbE [1].

We use a single universe $𝒰$ as the type of all types, with $𝒰:𝒰$. This is known to break termination of the system [14], making the type theory undecidable and inconsistent. Yet, as this is orthogonal to our focus, we go with the simple albeit inconsistent approach in our prototype. Apart from this, our MLTT is standard, featuring dependent function ($\mathrm{\Pi }$) and pair ($\mathrm{\Sigma }$) types with their $\eta$-laws, natural numbers with large elimination, and a unit type.

The first extension of ${\text{CC}}^{\text{obs}}$ compared to MLTT are proof-irrelevant propositions, given by a universe $\mathrm{\Omega }$ with the following conversion rule:

We use the symbol $𝔰$ for an arbitrary sort, $𝒰$ or $\mathrm{\Omega }$. Propositions include the false and true propositions $\perp$ and $\top$, and existential quantification $\exists (x{:}_{𝔰}A).B$. A $\mathrm{\Pi }$ type with a propositional codomain is again a proposition, representing universal quantification if the domain is relevant, or (dependent) implication if it is not.

Observational equality is a family of types, representing identifications between two inhabitants of the same type.

Equality is proven by reflexivity $\mathrm{𝐫𝐞𝐟𝐥}(t):t{\sim }_{A}t$, and can be used in two different ways: transport $\mathrm{𝐭𝐫𝐚𝐧𝐬𝐩}(t,xp.C,u,t^{\prime },e)$ lets us use the proof $e:t{\sim }_A{t}^{\prime }$ to turn the proof $u:C[t/x,\mathrm{𝐫𝐞𝐟𝐥}t/p]:\mathrm{\Omega }$ into a proof of $C[t^{\prime }/x,e/p]$;²²2Thanks to proof irrelevance, our version of transport where the motive $C$ depends on the proof of equality is inter-derivable with one without, so we include the stronger primitive for ease of use, while Pujet has the weaker primitive to simplify meta-theory. with cast $\mathrm{𝐜𝐚𝐬𝐭}(A,B,e,t)$, we can use a proof $e:A{\sim }_{U}B$ to construct an inhabitant of $B$ one of $A$. The difference is that the latter applies to relevant types, while the former proves a proposition. Thus, only $\mathrm{𝐜𝐚𝐬𝐭}$ needs to be endowed with computational content, as all propositions are convertible.

Beyond $\mathrm{𝐫𝐞𝐟𝐥}$, we add constants for symmetry ($\mathrm{𝐬𝐲𝐦}$) and transitivity ($\mathrm{𝐭𝐫𝐚𝐧𝐬}$). These are provable using $\mathrm{𝐭𝐫𝐚𝐧𝐬𝐩}$ and $\mathrm{𝐫𝐞𝐟𝐥}$, but some of our computation rules need them, so it is easier and cleaner to add them as primitives. This is a benefit of strict propositions: since there is no computation in the irrelevant layer, we are free to add propositional constants without needing to endow them with computational content.

Contrarily to MLTT, where equality is a type constructor and cast computes on reflexivity, in ${\text{CC}}^{\text{obs}}$ both the equality type and cast compute on the types. Yet, we still retain the following conversion, a generalisation of $\beta$ reduction of $\mathrm{𝐜𝐚𝐬𝐭}$ in MLTT – its special case when $e$ is ${\mathrm{𝐫𝐞𝐟𝐥}}_A$. This should be seen as an extensionality rule, similar to $\eta$-rules.

Observational equality gives us a synthetic language to talk about setoids [17, 4], types equipped with an equivalence relation. We can exploit this to integrate quotient types $A/R$: observational equality at such a quotient type simply boils down to the equivalence relation $R$. Quotients come with a projection map $\pi :A\to A/R$, and their elimination captures the idea that a function out of a quotient must respect the relation, i.e. map related inputs to equal outputs.

Since our system does not distinguish between local and global context, our inductive types are first-class [11, 8]: we can bind them to variables, and generally treat them as any other value. They take the following form:

The variable $F$ is bound by $\mu$. $A$ represents the type of indices. We have a finite list of constructors, each with a name $C_i$, an argument of type $B_i$, and an index $a_i$, which might depend on the argument. The $F$ at the end of each constructor is mere syntax indicating the type being constructed; it is not a free variable. In what follows, we use the following shortcut: $\mu F\triangleq \mu F:A\to 𝒰.[\overrightarrow{C_i:(x_i:B_i)\to F{a}_i}]$, i.e. $\mu F$ stands for a generic inductive.

We restrict inductive types to have exactly one index, and constructors to have exactly one argument. This loses no expressivity since we can pack arguments or indices together with $\mathrm{\Sigma }$ types, and simplifies the implementation. For further simplification, we also do not implement a positivity checker, so the typing rule allows non-strictly positive inductive types. As for universes, this is mainly orthogonal to our main concerns.

Since inductive types are first class, parameters can be handled by $\lambda$-abstraction, as illustrated by the standard example of vectors:

Values of inductive types are created by the constructors. We use fording [22, p. 65]: we allow all constructors to build a value of type $(\mu F)a$ for any index $a$ if they provide a proof that $a_i{\sim }_{A}a$, where $a_i$ is the index computed from the argument of the constructor. In the MLTT presentation of inductive types, this constraint is instead enforced definitionally.

Elimination of inductive types is single-level, total pattern matching:

This rule might appear strange, as the motive $C$ does not abstract over the index. Suppose $Vec$ as above, and we match on $v:\mathrm{𝑉𝑒𝑐}0$, so $x:\mathrm{𝑉𝑒𝑐}0⊢C:𝔰$. In the $\mathrm{𝐶𝑜𝑛𝑠}$ branch, we substitute $\mathrm{𝐶𝑜𝑛𝑠}$ into $C$. However, the index of $\mathrm{𝐶𝑜𝑛𝑠}$ is $Sn$, this looks ill-typed! But thanks to fording we can have $\mathrm{𝐶𝑜𝑛𝑠}(x,e):\mathrm{𝑉𝑒𝑐}0$, given a proof of $Sm\sim 0$, which we do have in this branch. Moreover, since $Sm\sim 0\equiv \perp$, we can use this to witness that this branch is in fact unreachable. The $\beta$ rule is straightforward, but for handling of the forded equality.

Observational equality between inductive types does not equate inductive types structurally: types with propositionally equal but definitionally different index and constructor types are not deemed equal.

The goal is twofold. First, this simplifies the implementation, as it means we avoid having to compare telescopes of parameters with numerous casts. Second, a purely structural equality of inductive types would equate all “boolean” inductive types (those with two argumentless constructors), a severe case of boolean blindness [16].

When the two definitions are not convertible, observational equality is simply stuck,³³3 As noted by Pujet [26, 5.2.2], there is a lot of room in how much definitional equalities are imposed on observational equality, the sole constraint – coming from canonicity – being that casts between convertible closed types must compute. i.e. it does not reduce further. This covers the case of definitely different inductive types (where we could be more eager and reduce to $\perp$), but also of parameterized inductive types. Indeed, for two different variables $A$ and $A^{\prime }$, $VecAn{\sim }_{𝒰}Vec{A}^{\prime }n$ is stuck, and will compute further only if $A$ and $A^{\prime }$ are substituted by convertible types. This equality therefore does not imply $A{\sim }_{𝒰}{A}^{\prime }$. We thus do not implement a conversion rule like the following:

Deriving these definitional equalities roughly amounts to deriving a general $map$ operation for inductive types, a non-trivial enterprise which we did not attempt. Since the design of our prototype, Pujet and Tabareau [29] have explored the question further, and proposed a solution, which we did not try to reproduce.

Equality of general inductives behaves like that of natural numbers: when comparing equal constructors, the proposition steps to equality of the contents, and when they are different, it steps to $\perp$. These respectively reflect injectivity and no-confusion of constructors.

For casts on constructors, as explained above we do not need to – and indeed cannot – propagate them deep in the structure. Instead, we merely need to handle indices, which amounts to composing equality proofs. Note the use of the $\mathrm{𝐭𝐫𝐚𝐧𝐬}$ primitive.

Pattern matching as eliminator for inductive types does not let us handle their recursive structure. That is, we have no notion of induction, as we can look only one level at a time. To correct this, we introduce $\mathrm{𝐟𝐢𝐱}$ in a style extending Mendler recursion [23] to dependent induction.

To express it, we first need an operation $\mathrm{𝐥𝐢𝐟𝐭}$ which applies a functor $F$ to a type $X$.

This operation is defined by the following equation:

In essence, $\mathrm{𝐥𝐢𝐟𝐭}[\mu F]B$ is an inductive type which is mute in the variable $F$, that is, non-recursive. It represents adding a single “layer” of $F$-structure over the family $B$.

Using this primitive, we can express the type of Mendler-style induction. As above, we abbreviate the inductive type to $\mu F$. The type $C$ is the one we want to inhabit by induction.

To type the body of the fixed point, Mendler induction operates by introducing a generic type family, $G$ and an inhabitant $x$ of $\mathrm{𝐥𝐢𝐟𝐭}[\mu F]Gp$, and demands that we construct an inhabitant of $C$ at $x$, while having access to “recursive calls” only on inhabitants of $G$ via the function $f$. Intuitively, we can pattern-match on $x$, recovering values of $G$ corresponding to “subterms”, that can be used for recursive calls. Since $G$ is abstract, this is the only way to call $f$, and so the fixed point we obtain is structurally decreasing.

The $\mathrm{𝐟𝐢𝐱}$ operation computes when applied to a constructor, as per the following rule. The argument must be a constructor in order to prevent infinite unfolding.

Mendler induction ensures $\mathrm{𝐟𝐢𝐱}$ is well-founded by restricting recursive appeals to the induction hypothesis. However, in this process, we lose information: we only have access to recursive calls, but not to the current value of the inductive type. In categorical parlance, fixed-points and pattern matching implement catamorphisms: generalised folds over tree-like structures.

What we want instead are paramorphisms, which provide primitive recursion by giving access to the current value. We thus introduce an extra function $\iota :\mathrm{\Pi }(p:A).Gp\to (\mu F)p$ to view the opaque $G$ as the inductive type it represents. Once the knot of the fixed point is tied and the variable $G$ is substituted for the inductive type, this becomes the identity.

To type the fixed point’s body we need to lift $\iota :\mathrm{\Pi }(p:A).Gp\to (\mu F)p$ into ${\iota }^{\prime }:\mathrm{\Pi }(p:A).\mathrm{𝐥𝐢𝐟𝐭}[\mu F]Gp\to (\mu F)p$. Hence, we need again the action of the functor $\mu F$ on values, i.e. the associated $map$. As explained above, we do not provide infrastructure to derive this operation. We instead allow an inductive definition to come with a user-provided functor action.⁴⁴4We do not check this indeed is the functor action, since generating the equalities a correct $map$ operation satisfies is basically the same as deriving that operation itself. Note that in the premise we use an inductive type without a functor.

To be able to use this definition, we introduce the term $\mathrm{𝐟𝐦𝐚𝐩}$ for projecting the functorial action from an inductive type and $\mathrm{𝐢𝐧}$, witnessing the isomorphism between $\mu F$ and $\mathrm{𝐥𝐢𝐟𝐭}[\mu F](\mu F)$, which is the identity function on constructors: $\mathrm{𝐢𝐧}(C_i(t,e))\equiv C_i(t,e)$.

With this infrastructure, we extend the typing rule for fixed-points.

The variable $\iota$ is now accessible in both the motive $C$ and the body $t$ of the fixed-point, facilitating primitive recursion. At the top level, $\iota$ is substituted by the identity function. By functoriality, this means ${\iota }^{\prime }$ is $\mathrm{𝐢𝐧}\circ \mathrm{id}$, which also behaves as the identity.

In summary, if the user provides a $map$ operation, we leverage that to upgrade our Mendler-style catamorphisms to paramorphisms. Of course, in a full-fledged implementation we would derive that operation automatically, and simply give access to the paramorphism.

We present ${\text{CC}}^{\text{obs}}$ in Russell style [21, 25], so we have a common grammar for both terms and types, given in Figure 2. This is roughly the one given in Pujet [26], with some additions: let bindings and type annotations, which are important with bidirectional typing, and, as explained in Section 2.1, constants for symmetry and transitivity.

We use a unit type $\mathrm{𝟙}$, with the term-directed $\eta$-conversions $t\equiv \mathrm{!}$ and $\mathrm{!}\equiv t$. These break transitivity of a term-directed algorithmic conversion: in the context $x,y:\mathrm{𝟙}$, we have $x\equiv \mathrm{!}\equiv y$ but $x\not\equiv y$. This is a trade-off: since we impose inductive types to have exactly one index and constructors exactly one argument, this unit type is handy to pad these positions with definitionally irrelevant content. In a more mature implementation, this would not be necessary, and we could drop our ill-behaved $\mathrm{𝟙}$, or adopt the more complex – and satisfactory – solution proposed by Kovács [20].

Box types $\mathrm{\square }A$ turn a type into a proposition – what is alternatively called squashing, truncation, or inhabited – see Pujet [26] for details.

Application $t{@}^{𝔰}u$ is tagged with the sort $𝔰$ of the argument $u$, and $\lambda$-terms and pairs with their domain sort. This is necessary for evaluation, but is always inferred during type-checking; users need not give these annotations in the source syntax.

This grammar inductively defines the type $\mathrm{𝖯𝗋𝖾𝖳𝗆}$ of pre-terms: syntactically well-formed, but untyped. We define another type $\mathrm{𝖳𝗆}$ of well-typed terms. Every well-typed term has a (unique) sort – $𝒰$ or $\mathrm{\Omega }$ –, the type of its type. We let ${\mathrm{𝖳𝗆}}^{𝒰}$ and ${\mathrm{𝖳𝗆}}^{\mathrm{\Omega }}$ be the set of terms with sort $𝒰$ and $\mathrm{\Omega }$ respectively. In the code we have separate types for $\mathrm{𝖯𝗋𝖾𝖳𝗆}$ and $\mathrm{𝖳𝗆}$, the former using named variables and the latter de Bruijn indices. We cannot enforce in Haskell that $\mathrm{𝖳𝗆}$ contains only well-typed terms, but maintain this as an invariant.

In what follows, we do not always cover all cases, focusing on the most interesting or illustrative ones. The code can be consulted for the complete picture.

Normals and neutrals are defined mutually as predicates on ${\mathrm{𝖳𝗆}}^{𝒰}$. In contrast to Pujet [27], they are deep, so subterms are also required to be normal.

We only need to characterize normal forms in ${\mathrm{𝖳𝗆}}^{𝒰}$, i.e. relevant terms. Indeed, since proof-irrelevant terms have no notion of evaluation, they all are “normal forms”. This means that normal forms are only unique up to $\eta$-equality and proof irrelevance. Luckily, thanks to typing constraints, irrelevant subterms of a relevant normal form can only appear as arguments to $\mathrm{𝐚𝐛𝐨𝐫𝐭}$, to $\mathrm{𝐜𝐚𝐬𝐭}$, or an application tagged with $\mathrm{\Omega }$, which lets us decide which subterms (not) to compare purely syntactically, without typing information.

Normal forms, as standard, correspond to constructors – observational equality and cast are viewed as destructors, and so are not normal forms. Neutral forms are somewhat more involved. The observational equality type can be blocked in three places – the type, or either of the terms – although there are no neutral forms when the equality is at a $\mathrm{\Pi }$ or $\mathrm{\Sigma }$ type, as such equalities always reduce. Similarly, casts can also block in three positions: either of the types, or the term being cast. Again, casts between universes, $\mathrm{\Pi }$ or $\mathrm{\Sigma }$ types always reduce, and so cannot be blocked by the argument. To avoid quadratic blow-up in the presentation, some cases overlap, for example $n{\sim }_{\mathbb{N}}v$ and $v{\sim }_{\mathbb{N}}n$ both cover $x{\sim }_{\mathbb{N}}y$.

Pujet [26, 5.2.2] discusses the definitional equalities observational equality should satisfy, for instance whether $\mathrm{\Pi }(x:A).B{\sim }_{𝒰}\mathrm{\Sigma }(x:A^{\prime }).B^{\prime }$ should evaluate to $\perp$ or be stuck. He remarks we can replace the reduction of $\mathrm{\Sigma }(x:A).B{\sim }_{𝒰}\mathrm{\Sigma }(x:A^{\prime }).B^{\prime }$ by two constants corresponding to the two projections out of the would-be reduct:

We chose to make conversion compute as much as possible as a minimal form of automation, although it is not entirely clear whether this makes using the proof assistant really easier.

First, we construct the various domains data-structures in Figure 3. The domains ${𝖣}^{𝒰}$ and ${𝖣}^{\mathrm{𝗇𝖾}}$ represent respectively normal and neutral forms. The domain ${𝖣}^{\mathrm{\Omega }}$ represents propositional values and is explained in Section 3.3. $𝖣$ is the union of ${𝖣}^{𝒰}$ and ${𝖣}^{\mathrm{\Omega }}$, and we often omit the injections $𝖵$ and $𝖯$.

These are defined mutually with closures ${\mathrm{𝖢𝗅𝗈𝗌}}_k^{𝔰}$ indexed by their return sort $𝔰$ and their arity $k$, as not all of them await a single argument. This is a landmark of defunctionalised NbE, which replaces semantic functions by such closures, making the various domains first-order strictly positive datatypes. Abel [1] needs a single kind of closure, consisting of an environment and a term, representing a meta-level function of type $\mathrm{𝖳𝗆}⇾\mathrm{𝖳𝗆}$. Here, we need to defunctionalise various evaluation functions, and thus have multiple forms.

Neutral terms for observational equality and casting are simplified: we do not keep track of which of the three arguments to $\mathrm{𝖤𝗊}$ and $\mathrm{𝖢𝖺𝗌𝗍}$ is blocking. This is a trade-off between a precise semantic domain and a simpler interpretation function. As the goal here is to implement the system, not prove its correctness, we choose the simpler representation.

Environments contain values from both sorts. An environment interprets a context, where each variable has a sort. It is a program invariant that the domain sort in each position in the environment matches the typing context.

Inputs to relevant interpretation are well-typed terms of sort $𝒰$; that is, the set ${\mathrm{𝖳𝗆}}^{𝒰}$. Therefore, we construct the function

The interpretation is given in Figure 4. The underlined functions and ${\cdot }_{𝔰}$ are semantic counterpart to eliminators, and are defined mutually with evaluation, see below.

We also need a function for applying a closure to $k$ values of either sort:

Applying to argument of the correct sort is a code invariant but not statically type-checked.⁵⁵5This could be enforced with closures indexed a type-level list of sorts. We use the shorthand notation $𝒞[d_1,\mathrm{\dots },d_k]$ for ${\mathrm{𝖺𝗉𝗉}}^{𝒰}𝒞d_1\mathrm{\dots }{d}_k$.

As closures are used to defunctionalise specific operations, we define those alongside the corresponding case for $\mathrm{𝖺𝗉𝗉}$. To begin with, we have the primary cases of a continuation, $(\underset{¯}{\lambda }t)\rho$, corresponding to substitution, and $\mathrm{𝖫𝗂𝖿𝗍}$, for a constant closure ignoring its argument.

Semantic application $\mathrm{\_}{\cdot }_{𝔰}\mathrm{\_}:{𝖣}^{𝒰}⇾{𝖣}^{𝔰}⇾{𝖣}^{𝒰}$ directly uses generic closure application.

To complete the semantic interpretation, we need to define $\underset{¯}{\mathrm{𝖾𝗊}}$ and $\underset{¯}{\mathrm{𝖼𝖺𝗌𝗍}}$, the semantic counterpart to the observational equality type and to cast, which implement their reduction behaviour. The former is given in Figure 5.

Semantic equality straightforwardly implements the computational behaviour of observational equality. Note the use of the two defunctionalising closures $\mathrm{𝖤𝗊𝖯𝗂}$ and ${\mathrm{𝖤𝗊𝖯𝗂}}^{\prime }$: $\mathrm{𝖤𝗊𝖯𝗂}$ forwards the equality proof into a second closure ${\mathrm{𝖤𝗊𝖯𝗂}}^{\prime }$ which performs the computation. This is necessary because we have two positions requiring arity-one closures, so they cannot be combined. When the $\mathrm{\Pi }$ types have an irrelevant domain, we need a propositional witness of type $A$, so we use $\mathrm{𝖯𝖢𝖺𝗌𝗍}$ and the freeze function $\varphi :𝖣\hookrightarrow {𝖣}^{\mathrm{\Omega }}$ for embedding relevant values into the irrelevant domain, both of which will be introduced in Section 3.3.

The final component to complete evaluation is the semantic $\underset{¯}{\mathrm{𝖼𝖺𝗌𝗍}}$ function, given in Figure 6, again straightforwardly implementing reduction rules for casts. Note the proof manipulation implemented by propositional application $\mathrm{𝖯𝖠𝗉𝗉}$ and projections $\mathrm{𝖯𝖥𝗌𝗍}$ and $\mathrm{𝖯𝖲𝗇𝖽}$, and again the embedding $\varphi :𝖣\hookrightarrow {𝖣}^{\mathrm{\Omega }}$.

The mutually recursive functions ${𝗊}_{𝗇}^{\mathrm{𝖭𝖿}}:{𝖣}^{𝒰}⇾\mathrm{𝖭𝖿}$ and ${𝗊}_{𝗇}^{\mathrm{𝖭𝖾}}:{𝖣}^{\mathrm{𝗇𝖾}}⇾\mathrm{𝖭𝖾}$ let us quote domain values back into normal and neutral forms, at de Bruijn level $𝗇$. We rely on a helper function ${\mathrm{𝗏𝗌}}_{𝗇}^{𝒰}:{\mathrm{𝖢𝗅𝗈𝗌}}_k⇾{𝖣}^{𝒰}$ to fully apply a closure to fresh variables.

Quoting is given in Figure 7, and follows the expected pattern. The cases for equality and casting do not ensure statically that they produce neutral forms. However, it is a program invariant that one position will be a blocking neutral, so the term is a neutral form in $\mathrm{𝖭𝖾}$.

The simplest strategy to handle proof-irrelevance is to rather brutally erase irrelevant terms at evaluation, as suggested in Abel et al. [2]. This amounts to having a single semantic proposition, i.e. defining ${𝖣}^{\mathrm{\Omega }}::=\mathrm{𝖶𝗂𝗍𝗇𝖾𝗌𝗌}$. This vastly simplifies the implementation, by removing intricate proof manipulations.

Although this approach is correct in terms of deciding the equational theory, it has a major drawback: normal forms cannot be quoted back to terms. Indeed, since proofs are erased, there is no information left to quote! This has nasty consequences. First, we must deal with this missing information when printing terms back to users, for instance in error messages. Quoting is also using during unification, to provide term solutions for unification variables – see Sec. 4.3.

As a mitigation, Abel et al. propose to extend the language by a constant $𝖮$ which proves every provable proposition. In practice, this would amount to indicate in quoted terms where proofs exist, but without giving a precise witness. However, one must be careful to exclude $𝖮$ from the source language, as it makes type-checking wildly undecidable by making it depend on inhabitation. Decidability could be recovered by instead having $𝖮$ prove all propositions, at the cost of making the type theory inconsistent, also far from ideal. Thus, in this approach we have to maintain a careful and clumsy distinction between “user-issued” terms and “kernel-generated” ones, with annoying consequences in the interaction with users: for instance, it means they would not be able to copy code from messages. We thus chose to reject this solution and look for another one.

A natural alternative is to retain syntactic witnesses for proof terms during evaluation: since we never need to evaluate propositions, there seems to be no point in translating them to a domain such as ${𝖣}^{𝒰}$, which is designed for efficient evaluation. This amounts to setting ${𝖣}^{\mathrm{\Omega }}::=\mathrm{𝖯𝗋𝗈𝗉}t\rho$ – a proof witness $t$ and an environment $\rho$ interpreting its free variables. Indeed, while they do not reduce, propositions still admit substitutions of their variables, which happens when evaluating relevant terms, and must be accounted for. This is the point of the stored environment, used to interpret free variables during quoting.

More challenging, though, is the proof manipulation which occurs in casting reduction rules. This requires inserting a proof-relevant value into the proof witness and shifting propositions to be well-typed in a different context. In this approach, evaluation and quoting become mutually defined, and great care must be taken to transform witnesses correctly. This entanglement of evaluation and quoting is both unsatisfying and error-prone.

We therefore introduce a third design: using a semantic domain similar to ${𝖣}^{𝒰}$. The idea is that values in this domain never reduce, they only admit substitution, which is handled by closures, but they use de Bruijn levels, making it unnecessary to shift or quote terms during evaluation. As relevant data might appear as subterms of propositions, ${𝖣}^{\mathsf{\Omega }}$ also embeds relevant terms. However, these do not reduce: they are “frozen”.

The domain of semantic propositions has a structure similar to terms, except for the use of closures for bound variables, and de Bruijn levels. Even let bindings and type annotations are represented, unevaluated. Calligraphic letters represent closures, which are the same as in Section 3.2, but have values from ${𝖣}^{\mathrm{\Omega }}$ in place of ${𝖣}^{𝒰}$.

Next, we introduce freezing, the mapping $\varphi :{𝖣}^{𝒰}⇾{𝖣}^{\mathrm{\Omega }}$ of semantic relevant values into semantic propositions, so that they may be used in proof terms. It is defined mutually with ${\mathrm{\Phi }}_k:{\mathrm{𝖢𝗅𝗈𝗌}}_k^{𝒰}⇾{\mathrm{𝖢𝗅𝗈𝗌}}_k^{\mathrm{\Omega }}$ which embeds closures. Representative cases are given as follows:

Freezing has to traverse the whole term, which is rather inefficient, especially if we repeatedly freeze the same term. In retrospect, it might be possible to replace it by a mere constructor which freely embeds ${𝖣}^{𝒰}$ into ${𝖣}^{\mathrm{\Omega }}$.

Semantic interpretation for propositions, ${[[\mathrm{\_}]]}^{\mathrm{\Omega }}\mathrm{\_}:\mathrm{𝖳𝗆}⇾\mathrm{𝖤𝗇𝗏}⇾{𝖣}^{\mathrm{\Omega }}$, is particularly easy as there are no reductions. We give only a few cases, others are entirely similar.

Projections from the environment are like in relevant interpretation, although when the entry is relevant, we freeze it with $\varphi :{𝖣}^{𝒰}⇾{𝖣}^{\mathrm{\Omega }}$. This handles substitution – syntactic variables $x_i$ are substituted by values from the environment. $\lambda$-expressions introduce a closure which can be entered, but this never happens due to application, only during quoting. Interpretation of application always produces a $\mathrm{𝖯𝖠𝗉𝗉}$, even when the interpretation of $t$ is $\mathrm{𝖯𝖫𝖺𝗆}$.

We also define a function ${\mathrm{𝖺𝗉𝗉}}^{\mathrm{\Omega }}:{\mathrm{𝖢𝗅𝗈𝗌}}_k^{\mathrm{\Omega }}⇾𝖣⇾\mathrm{\cdots }⇾𝖣⇾{𝖣}^{\mathrm{\Omega }}$ for applying closures. This works similarly to ${\mathrm{𝖺𝗉𝗉}}^{𝒰}$, only no reduction occurs: compared to Figure 5, we replace each semantic operator by a constructor. For example,

Finally, we also have quoting for semantic propositions ${𝗊}_{𝗇}^{\mathsf{\Omega }}$, which computes in the same way as quoting for ${𝖣}^{𝒰}$, fully applying closures to fresh variables.

As usual, the first step is to extend the domains, driven by the structure of the normal and neutral forms. Like before, we omit values for inductive types without functor definitions (in the implementation, we have optional value for the functor definition).

The semantic value of inductive types, $\mathrm{𝖬𝗎}$, contains the index type, followed by a list of pairs representing constructor types and indices. We have an optional value representing the presence or absence of an index. Fixed-points have a similar structure. The neutral form $\mathrm{𝖥𝗂𝗑𝖠𝗉𝗉}$ represents a fixed-point blocked by a neutral argument. Defunctionalizing closures and semantic propositions are entirely unsurprising, and we omit them here.

First, we give the semantics of the newly added terms.

The implementations of $\underset{¯}{\mathrm{𝗆𝖺𝗍𝖼𝗁}}$, $\underset{¯}{\mathrm{𝗅𝗂𝖿𝗍}}$, $\underset{¯}{\mathrm{𝖿𝗆𝖺𝗉}}$ and $\underset{¯}{\mathrm{𝗂𝗇}}$ all branch on their argument being either a constructor, in which case the relevant branch is taken, or a neutral, which leads to a neutral. They are found in the code.

Reduction of fixed points is handled by application, and we thus extend $\mathrm{\_}{\cdot }_{𝔰}\mathrm{\_}$ as follows:

When a semantic inductive type or fixed-point have not been applied to their index – indicated by their final component being $\mathrm{𝖭𝗈𝗍𝗁𝗂𝗇𝗀}$ –, we move this index into the value. When a fixed-point with an index is applied to a constructor, we invoke the closure $ℱ$, i.e. the body of the fixed point. Note how we pass the semantic identity function $\underset{¯}{\mathrm{id}}\triangleq {[[\lambda px.x]]}^{𝒰}$ for the view.

Pattern unification relies on metavariables, written $\mathrm{?}m$ and recorded in a metavariable context $\mathrm{\Sigma }$, which contains metavariables already solved through unification, and yet unsolved ones, as follows.

Note that we have metavariables $\mathrm{?}s$ for sorts, too. But what should $t$ be? That is, should metavariables stand for terms or for semantic values? To answer this, we must understand what operations we want to perform on them.

Metavariables are introduced during typing. As explained in Section 3.5, typing really is an elaboration procedure, taking in a preterm and constructing a term. In the presence of metavariables, it becomes stateful, as the metavariable context can be updated. The interesting rule is that which handles a hole in the surface syntax, creating two new metavariables representing the term and its type, and adding both to the metavariable context.

As any other term, we need to be able to evaluate metavariables into the semantic domains. If a metavariable is unsolved, it behaves like a variable and blocks the term, creating a new form of neutrals. We extend the semantic domain accordingly:

If a metavariable is defined, though, evaluation should reflect it. We achieve this as follows: