1 Introduction↩︎

Present-day proof assistants based on dependent type theory (e.g.Rocq, Lean, Agda, and Idris) are all based on elaboration: rather than merely “checking” that user-written code is well-formed, elaboration is a process that transforms user-written code to a more explicit core syntax or fails with an error. The difference between surface syntax and its core representation is that the latter must contain all the information needed to precisely describe and distinguish a well-defined mathematical object, whereas surface syntax often omits annotations and coercions that would be burdensome for a programmer to write. The design of surface and core syntax are dialectically linked, conditioned both by ergonomic and mathematical concerns:

1. Ergonomics: it is desirable for a programmer to avoid typing in bureaucratic annotations, arguments, and coercions when these can be reliably and predictably inserted by a machine.

2. Mathematics: whatever information is made implicit in the surface syntax must be unambiguously and effectively reconstructible: this depends on mathematical metatheorems about the core language, e.g. normalisation, decidability, strengthening, etc.

Experts know well what kinds of decisions in core language design might impede the implementability of a reliable surface language, and (conversely) what constraints on core languages may be required in order to enable various desirable surface language features. This folklore has not, however, prevented the promulgation of high-profile surface languages such as Lean’s in which (for example) the relation of definitional equality fails to be transitive;¹ for a user, such a failure might result in needing more than one proof step to verify \(x=y\) even when \(x\) and \(y\) are related by a sequence of definitional equations. Scenarios like this challenge the objectivity of proof assistants, which rests on a carefully negotiated division of labour between operator and machine.

Although questionable designs like this may be avoidable with a bit of care, we believe that the bigger problem is an air of “black magic” between core language metatheory and the design of suitable surface languages. We aim to address this gap by introducing a flexible mathematical framework in which a surface language is described modularly in terms of elaboration combinators in a monadic domain specific language (DSL), similar to the idea of parser combinators [2], [3]. Then, simple-minded calculational reasoning in the metalanguage may be used to reason about the behaviour of surface language code under elaboration.

Our DSL’s metalanguage is extensional Martin-Löf type theory [4],² whose dependent types are used to ensure that elaboration combinators are correct by construction in the following sense:

1. Elaboration always terminates and can only produce well-typed terms.

2. Elaboration cannot distinguish definitionally equal core language terms, and therefore respects the full \(\beta/\eta\)-congruence of the core language.

3. Elaboration is stable under core language substitution; elaboration problems can therefore be solved in any order without changing the end result.

Our viewpoint on the desirable properties of elaboration is similar to that of Kovács, who has recently argued for stable elaboration as a design principle [5]. We admit that no existing production system satisfies all of these desiderata, but our experience building and using interactive proof assistants over many years inspires our conviction that these are both desirable and achievable—with a bit of mathematics and a bit of engineering. This paper aims to provide the mathematics.

1.1 Background↩︎

1.1.1 Algebraic core languages and metatheory↩︎

In its history, the syntax of type theory has been treated in a variety of ways that span from the very concrete (inference rules over terms generated by a grammar) to the very abstract (anything satisfying the universal property of the initial model). We prefer to ground the discussion in the structural rôle of syntax in the applications of type theory—which are mainly in the area of proof assistants and programming languages. To be useful in these areas, an approach to syntax must be compatible with the statement and verification of key metatheoretic lemmas including the injectivity of type constructors and decidability of judgemental equality, both of which follow from normalisation.

For many years, metatheoretic results of these kinds were primarily established with respect to extremely concrete descriptions of syntax—at great cost. In the past decade, however, the category theoretic glueing method, long well-understood for simple types [6], [7], has finally been adapted to the far more difficult case of normalisation for dependent types, first by [8] and later refined by [9], [10] and [11]. With these streamlined methods in hand, the metatheory of dependent types can be established directly on any representation of the initial model of the type theory viewed as a second-order generalised algebraic theory [12] or SOGAT.

1.1.1.1 Second-order generalised algebraic theories

A second-order generalised algebraic theory is described by a signature that interleaves sorts, operations, and equations in a restricted version of extensional type theory. Dependent function sorts for operator arguments are available only when the domain sort is designated as representable. For example, in the signature for Martin-Löf type theory we have two generating sorts \[\Tp:\SortIdent{Sort}\text{,} \qquad \Tm\colon \Tp\to\SortIdent{Sort}_{\mathit{repr}} \text{.}\] The sort of types \(\Tp:\SortIdent{Sort}\) is not representable because bound variables cannot range over types, whereas the dependent sort of terms \(\alpha:\Tp\vdash \Tm\prn{\alpha}:\SortIdent{Sort}_{\mathit{repr}}\) is representable because bound variables may range over terms of a given type. The contexts of a type theory arise only indirectly in a SOGAT: they are given by telescopes of representable sorts. Every SOGAT gives rise to a (2,1)-category of models, which in the case of Martin-Löf type theory restricts to the usual notion of CwF [13] or natural model [14]. The bi-initial model of a given SOGAT plays the rôle of syntax, and it is with respect to this thing that the normalisation results of [9], [11], and others apply. These kinds of results should not be thought of as side-stepping traditional syntax; as [12] has shown, traditional syntax gives one representation of the bi-initial model of any SOGAT, and therefore the abstract normalisation result applies directly to traditional syntax even though it (thankfully) does not refer to it. We suggest that it is an advantage to have a metatheory that is robust to any change in representation of syntax.

1.1.1.2 The bi-initial model and its metatheory

A model of a SOGAT consists of a category of contexts \(\CX{\mathcal{M}}\) together with an algebra for the signature of sorts and operations and equations in the presheaf category \(\Psh{\CX{\mathcal{M}}}\) such that each family of representable sorts is taken to a representable family [12], [14]. The role of presheaves here can be understood as follows in the case of our running example: the sort \(\Tp:\SortIdent{Sort}\) should be interpreted by a family of sets \(\prn[\big]{\Tp_{\mathcal{M}}\prn{\Gamma}}_{\prn{\Gamma\in\CX{\mathcal{M}}}}\) of types in context, equipped with a substitution action \(\Tp_{\mathcal{M}}\prn{\Gamma}\to\Tp_{\mathcal{M}}\prn{\Delta}\) for any context morphism \(\gamma\colon\Delta\to\Gamma\). Once suitable associativity and unit laws for the substitution action are imposed, we have exactly the notion of a presheaf.

In a model of Martin-Löf type theory, the interpretation of a type constructor amounts to a natural transformation of presheaves. Written in the extensional type theoretic vernacular of \(\Psh{\CX{\mathcal{M}}}\) viewed as a locally cartesian closed category, for example, we have an arrow \[\TpPi_{\mathcal{M}}\colon \prn{\alpha:\Tp_{\mathcal{M}}}\times\prn{\Tm_{\mathcal{M}}\prn{\alpha}\to\Tp_{\mathcal{M}}}\to \Tp_{\mathcal{M}}\] and the normalisation result implies that when \(\mathcal{M}\coloneq\InitML\) is the bi-initial model of Martin-Löf type theory, the natural transformation \(\TpPi_{\InitML}\) depicted above is a monomorphism. This is the semantic version of the injectivity of type constructors.

1.1.2 Bidirectional surface languages↩︎

The “official” syntax for Martin-Löf type theory contains many apparently redundant type annotations. For example, the application of a \(\lambda\)-abstraction of type \(\TpPi\prn{\alpha,x\mathpunct{.}\beta\prn{x}}\) would involve multiple references to \(\alpha\) and \(\beta\): \[\TmApp\prn{\alpha,x\mathpunct{.}\beta\prn{x},\TmLam\prn{\alpha,x\mathpunct{.}\beta\prn{x}, x\mathpunct{.}\Var{body}\prn{x}},\Var{arg}} \]

When the injectivity of type constructors (§ 1.1.1) holds, an alternative syntax with fewer annotations can be justified as presenting the bi-initial model, allowing us to write \[\TmApp\prn{\TmLam\prn{x\mathpunct{.}\Var{body}\prn{x}},\Var{arg}} \text{.} \]

Leveraging metatheory to remove all annotations seems splendid at first, but unfortunately it renders the typing problem undecidable and therefore prevents a reasonable implementation. Consequently, the design of surface languages is conditioned by the need for annotation schemes that are less verbose than the default but not so sparse as to impede the system’s practical implementation. This search has led to the idea of bidirectional type checking [15], [16], which is based on the observation that if only neutral and normal forms are allowed, then the totally unannotated system does have decidable type checking by means of a bidirectional information flow protocol [17]:

1. Types flow out of contexts through neutrals: we may synthesise the type of a neutral \(\Gamma\vdash E\).

2. Types flow in from the goal into normals: we may check whether a normal form \(\Gamma\vdash M:\alpha\) is well-typed.

Of course, we probably do want to be able to write \(\beta\)-redexes in a suitable surface language. The bidirectional way to achieve this is to force these redexes to come with an appropriate type annotation, e.g.by extending the synthesisable terms by a constructor \(\prn{\alpha\ni M}\) embedding an annotated normal. This leads to a middle ground in which some but not all annotations are present: \[\TmApp\prn[\big]{ \TpPi\prn{\alpha,x\mathpunct{.}\beta\prn{x}} \ni \TmLam\prn{x\mathpunct{.}\Var{body}\prn{x}}, \Var{arg} } \]

Following [18], we prefer to think of bidirectionality as a property of a distinct surface language with separate sorts for checkable and synthesisable terms. Then, a bidirectional elaborator translates the surface terms to core language terms, inserting all the omitted annotations.

1.2 Key ideas and contributions↩︎

1.2.1 Bidirectional elaboration in a partiality monad↩︎

In many prior works [17], [19], [20], bidirectional type checking and elaboration have been viewed as an instance of well-moded logic programming. This perspective is good for producing attractive displays of inference rules, but it leaves underspecified many important matters that we consider of the essence, including the proper scoping of hypothetical judgements as well as the suspension and resumption of temporarily unsolved elaboration problems. For this reason, we pursue a functional interpretation of bidirectional elaboration in a partiality monad, where input and output modes are mapped to actual inputs and outputs of monadic functions. This is similar to the proposal of [21] (see § 1.3 for discussion), but unlike op.cit.we will not use the Maybe monad.

1.2.1.1 A generic model of the core language

The metalanguage for our monadic interpretation of bidirectional elaboration will be extensional type theory in which we additionally assume a sequence of constants and equations corresponding to the structure of a model of the target type theory, including constants \(\Tp:\SET\) and \(\Tm\colon \Tp\to\SET\). Such constants can be found in the extensional type theoretic vernacular of \(\Psh{\CX{\InitML}}\), which is where we shall ultimately interpret our metalanguage.

1.2.1.2 Semantic domains for surface language sorts

Relative to a monad \(\PMC\) determining a notion of computation [22] appropriate for elaboration, we define three semantic domains \(\TypScript\), \(\SynScript\), and \(\ChkScript\) corresponding to surface types, synthesis-mode, and checking-mode surface terms respectively: \[\TypScript \coloneq \PMC\prn{\Tp} \qquad \SynScript\coloneq\PMC\prn[\big]{ \prn{\alpha:\Tp}\times \Tm\prn{\alpha} } \qquad \ChkScript\coloneq \prn{\alpha:\Tp}\to \PMC\prn{\Tm\prn{\alpha}}\]

In other words,

1. a surface language type denotes a computation of a core language type;

2. a surface language synthesis-mode term denotes a computation of a core language term equipped with its type;

3. a surface language checking-mode term denotes a dependent mapping from core language types \(\alpha\) to computations of core language terms of type \(\alpha\).

Then, the constructors of the surface language will be implemented as combinators.

1.2.1.3 A partiality monad for elaboration

What monad \(\PMC\) shall we use? Experience both on the theoretical and the practical side suggests that a partiality monad is appropriate, and we are keen to clarify that the role of partiality is to introduce conditions for successful elaborations rather than to introduce any form of recursion. In particular, we define \[\PMC\prn{X} \coloneq \prn{\varphi:\PROP}\times \prn{\varphi\to X}\] where \(\PROP\) is a universe of proof-irrelevant propositions.³ An element of \(\PMC\prn{X}\) is a partial element of \(X\) whose support is given by the first component. With this in hand, we can begin to introduce some of the surface language constructors as combinators.

Below we show one further example to illustrate the way that our approach leverages the metatheory of the core language.

1.2.2 Category-theoretic interpretation of scope↩︎

Hypotheses are classified by an auxiliary sort \(\HypScript\coloneq \prn{\alpha:\Tp}\times\Tm\prn{\alpha}\). In other words, a hypothesis denotes a typed core term and not a computation thereof, in keeping with the call-by-value interpretation of elaboration scripts. Binders in the surface language are represented using the metalanguage’s function space; for example, the elaboration combinator for the surface language dependent function type is specified as follows:

To implement \(\ElabPi~A~B\) we would ideally bind \(A\) and then bind \(B\) to apply \(\TpPi\) to the results. But that doesn’t quite make sense: we have \(B\colon\prn{\alpha:\Tp}\times\Tm\prn{\alpha}\to\PMC\prn{\Tp}\), which is not the kind of thing that we can bind. Here we come to one of our main contributions: an interpretation of scope as higher-arity lax monoidal structure. In particular, for any \(K:\SET\) and family of types \(X\colon K\to \SET\) we can define a “scoping” combinator that takes \(f\colon \prn{k:K}\to\PMC\prn{X\prn{k}}\) to the evident partial element that is defined when all the \(f\prn{k}\) are defined: \[\boldsymbol{\vartheta}_{K,X}\colon \prn[\big]{\prn{k:K}\to \PMC\prn{X\prn{k}}} \to \PMC\prn[\big]{ \prn{k:K}\to X\prn{k} }\]

The above turns out to generalise the lax cartesian monoidal structure [23] of the monad \(\PMC\), as when we specialise \(K\coloneq\mathbf{2}\) we obtain (up to isomorphism) precisely the double strength \(\PMC\prn{X\prn{0}}\times\PMC\prn{X\prn{1}}\to \PMC\prn{X\prn{0}\times X\prn{1}}\). Writing “\(\Scope~k:K~\In~f\prn{k}\)” for \(\boldsymbol{\vartheta}_{K,X}\prn{f}\), we can now implement the elaboration combinator for the surface language dependent function type constructor:

1.2.3 Equational reasoning about elaboration↩︎

Instead of treating the surface language as a mere notation for the core language, we are giving a direct and compositional denotational semantics into a monad that governs the (fallible) computation of core language terms. The use of denotational semantics means that surface language terms themselves have a useful equational theory. The simplest use of equational reasoning is to unfold surface language terms (construed as elaboration scripts, i.e. instances of elaboration combinators) to the core language terms they compute by expanding definitions and using the monad laws. These calculations, as we show in our case study (§ 4.6) are elementary and easy to carry out.

1.2.3.1 Multilinearity of elaboration

A more sophisticated use of equational reasoning is to prove theorems about individual elaboration combinators. For example, each elaboration combinator is built from \(\TypScript\), \(\SynScript\), and \(\ChkScript\); as these are all algebras for the partiality monad, we can ask whether the elaboration combinators are multilinear in these arguments; the answer, we have shown in § 5.1, is yes (for the binder-forming combinators, so long as we grant a mild strengthening property that our intended semantics satisfies). Multilinearity in the context of elaboration combinators intuitively means that the well-formedness conditions of a complete surface language term come from those of its subterms; it implies multistrictness, i.e.the preservation of undefined elements in all arguments. Multilinearity is one possible sanity condition that might be used to distinguish reasonable elaboration combinators from unreasonable ones (like \(\mathtt{first} : \ChkScript\to\ChkScript\to\ChkScript\), which returns its first argument and discards its second; this is not multilinear and would not be likely to appear in a competently designed surface language).

1.2.4 Inequational reasoning and subject reduction↩︎

Each monadic type \(\PMC\prn{X}\) carries a standard partial ordering: we have \(\prn{\varphi,u}\preccurlyeq_{\PMC} \prn{\psi,v}\) when \(\varphi\to \psi\) holds and, assuming \(\varphi=\psi=\top\) we have \(u=v\). This can be thought of as an “information ordering” on partial elements, inspired by domain theory. Taking the partial ordering seriously, we get new ways to reason about surface code by means of its denotation in the partiality monad. For example, [17] has suggested a rewriting system for surface terms including “subject reductions” for surface \(\beta\)-redexes like the following: \[\TmApp\prn[\big]{ \TpPi\prn{\alpha,x\mathpunct{.}\beta\prn{x}} \ni \TmLam\prn{x\mathpunct{.}\Var{body}\prn{x}}, \Var{arg} } \longmapsto \Var{body}\prn{ \alpha\ni\Var{arg} } }\]

Mc Bride’s reduction is reflected in our denotational model of bidirectional surface syntax as a (strict) inequation in the poset \(\SynScript \equiv \PMC\prn{\prn{\alpha:\Tp}\times\Tm\prn{\alpha}}\), as we discuss in § 5.2: \[\TmApp\prn[\big]{ \TpPi\prn{\alpha,x\mathpunct{.}\beta\prn{x}} \ni \TmLam\prn{x\mathpunct{.}\Var{body}\prn{x}}, \Var{arg} } \preccurlyeq_{ \SynScript } \prn[\big]{ \beta\prn{\alpha\ni\Var{arg}} \ni \Var{body}\prn{ \alpha\ni\Var{arg} } } }\]

The reason for the directionality of the inequation is that the left-hand side places constraints on \(\beta\) and \(\Var{body}\) that are not placed on the right: on the right, these only need be well-typed when instantiated with \(\prn{\alpha\ni\Var{arg}}\). We suggest that the subject reduction laws for surface calculi should be viewed not as reflecting a rewriting semantics for the core theory but instead as a guide for the safe optimisation and refactoring of surface expressions: an inequality \(u\preccurlyeq v\) means that the proof becomes more complete when \(u\) is replaced by \(v\), without changing the core term it produces.

1.2.5 Presheaf semantics for stable elaboration with suspension↩︎

One of the major desiderata for stable elaboration elucidated by [5] is that “if we reorder elaboration actions and metavariable solutions, the eventual output must not change, up to conversion”. From a formal point of view, our partiality monad satisfies this criterion because it is a commutative monad: elaboration actions that place constraints on metavariables can be reordered at will without changing the results.

This is at first slightly confusing. For example, if an elaboration action requires that \(?\mathrm{\small meta}=_{\Tp}\mathbb{N}\) in order to succeed, wouldn’t this mean that it would fail if it was executed before solving \(?\mathrm{\small meta} \coloneq \mathbb{N}\), but succeed if executed afterwards? The key idea of our approach is, to the contrary, that the denotation of an elaboration action contains the condition under which it may go ahead, but this condition does not need to be boolean. Therefore, under either ordering, the result is a partial element with support \(?\mathrm{\small meta}=_{\Tp}\mathbb{N}\), which may become true in various scopes. So rather than asserting a condition (and failing otherwise), we can think of an action like ‘\(\Await~?\mathrm{\small meta}=_{\Tp}\mathbb{N}\)’ as simply suspending the elaboration problem until such time as the metavariable is solved.

The intuitions above are ultimately vindicated by the interpretation of our metalanguage into presheaves on the category of contexts of the target language. In the presheaf model, a proposition denotes a sieve [24]: rather than a boolean truth value, it is a predicate that isolates the substitutions under which it becomes true. Then the force of ‘\(\Await~\varphi\)’ is to further narrow this sieve to the contexts where \(\varphi\) holds; a partial element therefore awaits a substitution that will bring it into its support.

Although there is much more to investigate and we admittedly have little to say in this paper about metavariables, we believe that our presheaf semantics provides a workable starting point for understanding the suspension and resumption of elaboration.

1.3 Discussion of related work↩︎

We take inspiration liberally from prior works, especially those of [21] and [12], as well as many conversations with Conor Mc Bride:

1. From Atkey’s Algebraic Approach to Type Checking and Elaboration [21] we take the idea that surface syntax (for simple type systems) might denote monadic combinators in a functional programming language. At the end of his talk, Atkey asked “Does this work for more complex type systems?” Our results suggest that the answer is ‘yes’, assuming one upgrades the setup appropriately. In addition to our successful treatment of full dependent types, our work differs from Atkey in a few ways: (1) context is implicitly governed by our novel \(\Scope\) combinator, (2) our account of elaboration is correct by construction, (3) we account for the suspension of elaboration problems by using a partiality monad on presheaves instead of the maybe monad.

2. From Uemura’s general initiality proof for SOGATs [12], we take the idea of interpreting surface syntax using a partiality monad on presheaves. Whereas Uemura treats the interpretation of fully explicit raw syntax, we have shown how to interpret bidirectional raw syntax by leveraging the metatheory of the core language; we further carefully arrange for our elaboration function to be effectively computable, employing ideas from synthetic topology.

3. The asynchronicity suggested by our \(\Await\)-notation is inspired by Conor Mc Bride’s (paraphrased) assertion that a reliable elaborator has more in common with an operating system than a straightline type checker. Our use of presheaves is also consonant with Mc Bride’s suggestion that a correct solution to the “Good Bye, Lenin!” problem (by which they refer to resuming suspended elaboration problems under an updated information environment) must involve a Kripke-style interpretation of the function space.

1.3.0.1 Semantic vs.syntactic frameworks

To discuss the remaining related work, we find it helpful to think of elaboration as a more sophisticated form of parsing. Proposals for general accounts of parsing tend to fall into two categories:

1. Semantic frameworks. Parser combinator libraries like Parsec [25] provide an API for compositionally producing and reasoning about parsers, using ideas from functional programming.

2. Syntactic frameworks. Parser generators like Yacc [26], Menhir [27], etc. transform suitably constrained grammars into working parsers, using ideas from formal language theory.

Similarly, we have proposed an API for compositionally producing and reasoning about elaborators without introducing any kind of formal grammar (i.e.presentation by inference rules). On the syntactic side, both [17] and [28] have proposed syntactic frameworks that might be characterised as “typechecker generators”: you give the framework a set of rules written in a suitably constrained format, and it gives you a typechecker.

We are very interested in both sides of this space, and we think that there is potential for combining them. For example, one weakness of the cited syntactic approaches has been the failure to account for \(\eta\)-rules, which are table stakes for dependently typed systems in the present day. Our semantic approach effortlessly handles \(\eta\)-rules, and we wonder if it might one day serve as an alternative “backend” to the cited syntactic frameworks.

2 Elementary structure of Martin-Löf type theory, internally↩︎

The goal of this paper is to describe a semantic version of the elaboration function which takes values in actual constituents of the initial model of Martin-Löf type theory—which are, by definition, intrinsically typed and identified up to judgemental equality. Such a treatment would be sound by construction without requiring any further proof. In this section, we describe the axiomatic form in which we shall treat the target model of the type theory.

Models of Martin-Löf type theory are typically described in terms of Dybjer’s categories with families [13], or equivalent structures like Awodey’s natural models [14]. In either case, one starts with a category of contexts and then the elementary structure (judgements, type connectives, etc.) of the type theory is expressed in terms of presheaves and natural transformations over the category of contexts. In recent years, several authors [11], [29], [30] have noted that the elementary structure can be studied independently of its instantiation over a category of contexts as, indeed, it can be expressed in any locally cartesian closed category. This point of view, in fact, can be traced back to Martin-Löf’s logical framework presentation [31], [32] from the late 1980s.

At this stage, we do not yet have need of contexts and will therefore stick to the elementary axiomatisation of type theory’s judgements and type connectives in the logical framework style. What follows may be read in the internal language of any locally cartesian closed category (e.g.presheaves on the category of contexts of the initial model of Martin-Löf type theory). We first describe the bare judgemental structure of Martin-Löf type theory: types and terms.

Of course, a judgemental structure is nothing more than a container in the sense of [33], which determines a polynomial extension functor \(\Fam\colon\SET\to\SET\): \[\Fam\prn{X} \coloneq \prn{\alpha:\Tp}\times \prn{ \Tm\prn{\alpha}\to X }\]

Next, we describe individual connectives over a judgemental structure.

We also include an “answer type” in order to have a base case.⁴

3 A partiality monad for synthetic elaboration↩︎

We intend to interpret correct-by-construction elaboration algorithms in the partiality monad of a topos equipped with a dominance [34]. We recall some basic definitions.

3.1 Dominance and partiality (relative) monad; the \(\Do\)-notation↩︎

A partial element of a type \(X\) consists of a support \(\varphi:\PROP\) under which it is defined, followed by a function \(\varphi\to X\). Because we ultimately intend our elaborators to be executable, we don’t want to allow all propositions to be used as supports; on the other hand, it would be too strong to require the support to be decidable (a Boolean), as we would not be able to interpret something like the conversion rule that is defined just when two given types are equal.⁵ At this point, we will just axiomatise whatever closure conditions we need relative to a class of propositions, which we later on will instantiate in an appropriate way. For such a class to give rise to a partiality monad, we need it to satisfy Rosolini’s dominance property [34].

Now let \(\OProp\) be an arbitrary fixed dominance.

When it is clear from context, we will simply say “partial” instead of “open partial”.

[34] observes that the partial element classifier associated to a dominance forms a monad, but we will be interested in a more refined relative 2-monad structure [35], [36] on \(\PMC\) that incorporates the standard partial ordering of partial elements. Working two-dimensionally in this way will let us treat the extension operator as itself monotone, and it is the structural reason (§ 3.5) that every map between algebras of \(\PMC\) is automatically a lax multimorphism.

Consequently, we may view the partial element classifiers as giving a functor \(\PMC\colon \SET\to\POSET\).

Beyond the usual relative monad laws, the two-dimensional structure asks that the extension operator be locally monotone: if \(f\preccurlyeq g\) pointwise then \(f^\dagger\preccurlyeq g^\dagger\), which is routine.

We will at times follow the notation of functional programming languages like Haskell.

3.2 Open-subsingleton subsets and partial elements; the \(\Await\)-notation↩︎

3.3 Compact types and universal quantification; the \(\Scope\)-notation↩︎

Any finite number of partial elements can be combined to form a single partial element; this is related to the commutative strength of the partiality monad, which corresponds to the statement that \(\PMC\) is a lax monoidal (relative pseudo-)monad. Either way, we have a family of maps \[\boldsymbol{\vartheta}_{\Card{n},X}\colon \prn[\big]{\textstyle\prod_{k<\Card{n}} \PMC\prn{X_k}} \to \PMC\prn[\big]{ \textstyle\prod_{k<\Card{n}} X_i }\] for every finite cardinal \(\Card{n}\) and family of types \(\prn{X_k}_{\prn{k<\Card{n}}}\) subject to appropriate compatibility conditions. A cornerstone of our approach is to notice that the restriction to finite cardinals \(\Card{n}\) is in fact not essential: any arity \(K\) can be used so long as \(\OProp\) is closed under universal quantifications over \(K\); in other words, \(K\) must be compact in the sense of synthetic topology [37]:

3.4 Lax monoidal structure at compact arity; the \(\Scope\)-notation↩︎

The partial element classifier monad is commutative and has a unique strength, correspondingly uniquely [23] to a lax (cartesian) monoidal structure consisting of an appropriately coherent datum \(\vartheta_{\mathbf{2}}\colon \PMC\prn{X}\times\PMC\prn{Y}\to \PMC\prn{X\times Y}\). One of our main insights is that this lax monoidal structure exists not only at finite arities but, in fact, at all compact arities.

Clearly every finite type is compact, as the universal quantifier may be reduced to iterated conjunction, which we have from \(\OProp\) being a dominance. In this case, the lax monoidal structure obtained from Construction [con:lax-monoidal-compact] coincides with the standard one. We shall, however, eventually use Construction [con:lax-monoidal-compact] to interpret hypothetical judgements and binders in the denotational semantics of elaboration by assuming certain non-finite objects arising from syntax to be compact.

In what follows, let \(K\) be compact and let \(J\colon K\to\SET\) be a family of compact types; we will write \(\widetilde{J}\coloneq \prn{k:K}\times J_k\), which is also compact by Lemma 1. We check several important coherence laws for the lax monoidal structure below:

Lemma 2 says that \(\boldsymbol{\vartheta}\) is (at finite arity) the symmetric lax monoidal structure of the commutative monad \(\PMC\). The lax-idempotency of \(\PMC\)—visible in the standard order on partial elements—is the structural reason for this commutativity [38], [39].

We will at times have use for the following lemma.

3.5 Algebras; multilinear and multistrict functions↩︎

Since \(\PMC\) is a relative 2-monad along \(\DiscIncl\colon\SET\to\POSET\), it would not make sense for an algebra to be presented by a structure map \(\PMC\prn{A}\to A\): the carrier \(A\) is a poset.⁶ We use instead the extension-form presentation of [35], carried over to the two-dimensional setting as defined in [40]; concretely, the extension operator of an algebra is required to be monotone both as a map out of \(\PMC\prn{X}\) and in its argument, the latter being the algebraic analogue of the local monotonicity of \(\prn{-}^\dagger\) recorded in Construction [con:L-relative-monad].

3.5.1 Multilinear and lax multilinear functions↩︎

There is a standard notion of homomorphism between algebras in extension form: the linear map.

Because we do not wish to require that tensor products exist (as we shall discuss in Remark [rem:nonrepresentable]), we will have need of a more general notion of homomorphism in many variables, defined below.

Multilinear maps of finite arity, then, equip the algebras with the structure of a multicategory \(\underline{\mathcal{L}}\).

The multilinearity equation of Definition 16 asks for an equality. In the two-dimensional setting we can also consider a notion of lax multilinearity that replaces equality by inequality, but this turns out to be satisfied automatically by every monotone map, so we do not consider it further.

3.5.2 Multistrict functions and undefinedness↩︎

When the dominance is strict in the sense that \(\OProp\ni\bot\), we can relate multilinearity to a more intuitive property: strictness. First we note that any algebra supports an undefined element:

We do not expect the converse to Lemma 8 to hold.

4 Elaborators à la Carte, over a dominance↩︎

We now describe a semantic notion of elaborator in the partiality relative 2-monad (§3) over an arbitrary dominance \(\OProp\). Rather than fixing in advance a source language and target language, we will develop the two modularly in lockstep.

We specify the semantic domains for elaboration over a judgemental structure: \[\TypScript \coloneq \PMC\prn{\Tp} \qquad \ChkScript \coloneq \prn{\alpha:\Tp}\to\PMC\prn{\Tm\prn{\alpha}} \qquad \SynScript \coloneq \PMC\prn[\big]{\widetilde{\Tm}} \qquad \HypScript \coloneq \widetilde{\Tm}\]

4.1 Structural combinators↩︎

Everything that follows takes place over an elaborable judgemental structure.

4.1.0.1 Variables and substitution

Hypotheses are included into synthesisable expressions using the monad unit:

Conversely, a synthesisable expression \(E:\SynScript\) can be “substituted” for a hypothesis in a binder \(k\colon \HypScript\to A\) valued in an algebra \(A\) using the algebra’s extension operation: \(x\gets E; k\prn{x}\).

4.1.0.2 Conversion and annotation

The conversion rule of Martin-Löf type theory corresponds to the following combinator:

4.2 Elaborating dependent function types↩︎

The following definitions take place over an elaborable dependent function type structure. First the formation rule:

Next, we implement the introduction rule. In the case of dependent functions, it is possible to envision two different directionalities for \(\lambda\)-abstractions: checking mode without annotations, and synthesis-mode with a type annotation on the bound variable. We implement both below:

Function applications are implemented in synthesis mode as follows:

4.3 Elaborating dependent pair types↩︎

We can now define appropriate elaborators over an elaborable dependent pair type structure.

4.4 Elaborating intensional identity types↩︎

The usual formation rule for identity types takes a type together with two elements of that type. Alternatively, we can leave the type out if the left-hand side is in synthesis mode. Either rule is easily implemented in our system.

We now come to a simple example of equational reasoning on the surface language:

Assuming the identity type structure is elaborable, then the \(\TmRefl\) constructor is trivial to implement in checking and synthesis mode variants.

Martin-Löf’s identification eliminator requires an induction motive and a base case.

4.5 Elaborating the answer type↩︎

Assuming an answer type structure over an elaborable judgemental structure, we will not need any further elaborability conditions.

4.6 Case study: elaborating a complex type↩︎

We can now illustrate a bidirectional elaboration script and its evaluation to a term. We will consider in particular the type of the symmetry function that inverts an identification using Martin-Löf’s identification eliminator. We will show by simple equational reasoning how to execute the elaboration of the following script:

4.7 Scoped elaboration in context↩︎

Much as [17] has advocated, the context of elaboration is not an explicit parameter to the elaboration process but rather emerges implicitly through the use of the \(\Scope\) combinator. Nonetheless, an actual elaboration script (as written by a user in a proof assistant) will take place in the scope of a number of free hypotheses \(x_1,\ldots,x_n:\HypScript\), and this script will be executed relative to an actual well-formed type context \(x_1:A_1,\ldots,x_n:A_n\) of the same length. We show in this section that explicitly scoped elaboration scripts like this can be made sense of directly in our framework, in the presence of an elaborable judgemental structure.

4.7.1 Telescopes as formal type contexts↩︎

We define a length-indexed inductive type of telescopes to represent formal type contexts.

Then we define for each telescope the type of environments as an iterated dependent pair type.

We will write \(\widetilde{\Env}_n\) for \(\prn{\Psi:\Tele_n}\times \Env_n\prn{\Psi}\) and \(\widetilde{\Env}\) for \(\prn{n:\mathbb{N}}\times \widetilde{\Env}_n\).

5 Denotational reasoning about surface syntax↩︎

We are now in a position to begin reasoning about elaboration scripts using the semantics that we have given. Although we cannot exhaust the topic in a single paper, we present two possible areas of denotational exploitation: multilinearity as a sanity condition for good elaboration combinators, and an inequational version of subject reduction for untyped elaboration scripts.

5.1 Multilinearity of elaboration combinators↩︎

In § 3.5, we introduced the notion of algebra and multilinear map for the relative 2-monad \(\PMC\colon \SET\to\POSET\). We recall that the main semantic domains for elaboration are actually algebras:

1. \(\TypScript = \PMC\prn{\Tp}\) and \(\SynScript = \PMC\prn[\big]{\widetilde{\Tm}}\) are both free algebras.

2. \(\ChkScript = \prod_{\alpha:\Tp}\PMC\prn{\Tm\prn{\alpha}}\) is a product of free algebras.

3. The domains for binders, like \(\HypScript\to \TypScript\) and \(\HypScript\to\ChkScript\) are powers \(\HypScript\pitchfork\TypScript = \prod_{\_:\HypScript}\TypScript\) and \(\HypScript\pitchfork\ChkScript = \prod_{\_:\HypScript}\ChkScript\) of algebras respectively.

Hence we may consider whether a given combinator built from the above is multilinear.

Multilinearity in turn implies multistrictness, which we believe is an important sanity condition for elaboration rules.

In other words, if any “subterm” of an elaboration script built from these combinators is undefined, the entire script is undefined. This is an important sanity condition for surface languages: in those terms, it captures the idea that a well-typed term will necessarily have no ill-typed subterms.

5.2 Shadows of subject reduction↩︎

An important property of certain declarative presentations of type theory is subject reduction with respect to an (untyped) rewriting system: if \(\Gamma\vdash M:A\) holds and \(M\mapsto M'\), then \(\Gamma\vdash M':A\) must hold. Of course, “full spectrum” dependent type theory is not typically presented by an untyped rewriting system, as rewriting methods have thus far never scaled to a satisfactory handling of the \(\eta\)-laws for dependent pair types. For that reason, discussion of “subject reduction” in the context of modern type theoretic systems has always had the air of science fiction about it; nonetheless, we believe that our denotational semantics of surface syntax as bidirectional elaboration combinators may provide some insight on the question.

For example, one might conjecture that a surface-level “\(\beta\)-redex” would be equal to its contractum, as suggested by [17]: \[\ElabApp~\prn{ \ElabThe~\prn{ \ElabPi~A~B }~\prn{ \ElabLam~M } }~{N} \stackrel{?}{=} x\gets \ElabThe~{A}~{N}; \ElabThe~B\prn{x}~M\prn{x}\] However, if we unravel the definitions of both sides, we will see that they are not equal without additional assumptions. In particular, the left and right hand sides unravel as follows:

As can be seen by inspection, the difference between the two lies solely in their definedness as partial elements. The left-hand side is defined only when \(B\) denotes a well-typed family of types and when \(M\) denotes a well-typed section of this family of types, whereas the right-hand side requires only that specific substitution instances of \(B\) and \(M\) be well-typed. The former is stronger than the latter, which suggests that subject reductions like this may correspond to inequational reasoning in the partiality monad. Indeed:

Because all the elaboration combinators are monotone, the “subject reduction” inequations of Theorem 2 extend to an inequational congruence for elaboration scripts, making inequational reasoning compositional.

6 Correct by construction elaboration via initiality↩︎

In § 4 we have shown how to specify and construct elaboration scripts in the partiality monad of a dominance satisfying certain properties. In this section, we will describe a specific topos and dominance in which the constructions of § 4 may be executed so as to lead to a correct by construction elaboration algorithm. The extraction of this algorithm is carried out abstractly, using the initiality property of a second-order generalised algebraic theory of untyped elaboration scripts.

6.1 Implicit computational content via a base topos↩︎

We are careful to develop everything constructively (in the sense of validity in an elementary topos with a natural numbers object), so that the extracted elaboration function can be understood to have an algorithmic content. This is a kind of implicit effectiveness, which a classical mathematician might prefer to make explicit by carrying out the constructions below in a realisability topos [41]. We remain agnostic on this point, and simply work relative to an arbitrary base topos \(\BaseTopos\) that shall play the role of the ambient category of sets.

6.2 Natural models of second-order generalised algebraic theories↩︎

A natural model [14] of Martin-Löf type theory with an answer type is given by a category of contexts \(\mathbb{C}\) equipped with a terminal object \(\mathbf{1}_{\mathbb{C}}\) together with the following structure in the category of presheaves \(\Psh{\mathbb{C}}\):⁸

1. a judgemental structure \((\Tp,\Tm)\) such that \(\Tm:\Psh{\mathbb{C}}/\Tp\) is representable in the sense that each of its fibres over a representable is representable;

2. dependent function type, dependent pair type, identity type, and answer type structure.

In other words, a natural model is given by an elementary model (§ 2) in a chosen category of presheaves, with the additional condition that the base category be closed under contextual operations (empty context and context extension). The natural models arrange themselves into a (2,1)-category with a bi-initial object, which [12] shows can be built from raw syntax.⁹

The notion of natural model described above is a special case of a more general notion that applies to second-order generalised algebraic theories [12], of which Martin-Löf type theory is a specific example. We will use SOGATs twice: first to view Martin-Löf type theory algebraically, and second to circumscribe a theory of untyped elaboration scripts from whose initiality property we shall extract an elaboration algorithm.

6.3 A topos and dominance for effective elaboration↩︎

Our goal is to find a topos over \(\BaseTopos\) equipped with a dominance \(\OProp\) and an elementary model of Martin-Löf type theory that is elaborable with respect to \(\OProp\) in the sense of § 4.

6.3.1 Presheaves on contexts and substitutions↩︎

Now let \(\InitML\) be the bi-initial natural model of Martin-Löf type theory with an answer type, so that we have the structure of an elementary model (§ 2) in \(\Psh{\CX{\InitML}}\). As \(\CX{\InitML}\) is the category of contexts and substitutions of our type theory, a presheaf on \(\CX{\InitML}\) is a context-indexed family of sets equipped with a substitution action.

Our first goal is to construct a dominance in \(\Psh{\CX{\InitML}}\) that makes the given elementary model of type theory elaborable in the sense of § 4. If we chose the maximal dominance \(\PROP\), then the ensuing interpretation of elaboration scripts would shed no light on the effective computability of elaboration. Instead, we shall follow [11] by employing a subuniverse of levelwise decidable propositions, which may be defined for any presheaf topos as we do in § 6.3.2; we must also account for strengthening, which we incorporate in § 6.3.3.

6.3.2 The dominance of levelwise decidable propositions↩︎

The subobject classifier for presheaves is defined in terms of sieves [24]: a proposition in context \(\Gamma\) is given by a sieve on \(\Gamma\), i.e.a set of arrows into \(\Gamma\) that is closed under precomposition (i.e.substitution). The idea of [11] is to replace sieves with levelwise decidable sieves, i.e.sets of arrows closed under precomposition for which the membership problem is decidable in the base topos \(\BaseTopos\). Hofmann and Streicher’s universe lifting construction [44] provides a more structural characterisation, as suggested by [45]:

1. The subobject classifier of \(\Psh{\CX{\InitML}}\) is the Hofmann–Streicher lifting of the subobject classifier \(\mathbf{1}\hookrightarrow\PROP_{\BaseTopos}\) from the base topos.

2. The levelwise decidable subobject classifier of \(\Psh{\CX{\InitML}}\) is the Hofmann–Streicher lifting of the decidable subobject classifier \(\mathbf{1}\hookrightarrow\mathbf{2}\) from the base topos.

We shall write \(\PROP_{\mathit{ldec}}\subseteq\PROP\) for the dominance of levelwise decidable propositions in \(\Psh{\CX{\InitML}}\).

6.3.3 A Lawvere–Tierney modality for strengthening↩︎

Our full results on multilinearity (Theorem 1) require the following strengthening property for all open propositions.

Not every levelwise decidable proposition will be strengthenable; we will therefore intersect the levelwise decidable and strengthenable propositions. First, we comment that the strengthenable propositions form an oracle modality in the sense of [46], namely the smallest Lawvere–Tierney modality whose modal propositions are all strengthenable. As a result, the strengthenable propositions automatically form a dominance for which all types are compact.

6.3.4 Open propositions and elaborability in the presheaf model↩︎

We define \(\OProp \coloneq \PROP_{\mathit{ldec}}\cap \PROP_{\mathit{str}}\) to be the dominance consisting of strengthenable levelwise decidable propositions.

6.4 A theory of elaboration scripts↩︎

We now abstract the elaboration combinators from § 4 into a second-order generalised algebraic theory (SOGAT) with four basic sorts \(\HypScript\), \(\SynScript\), \(\ChkScript\), and \(\TypScript\). Because variables range only over hypotheses, we declare \(\HypScript\) to be representable and all other sorts non-representable; then we introduce operations corresponding to the basic elaboration combinators that we have defined. The entire signature is presented in Figure 18. This theory is provisional in the sense that we might reasonably add more generators and equations in the future. Our goal is not to fix for all time a definition of what an “elaboration script” is, but rather to delineate a reasonable signature that can be used in practice and extended in response to practical discoveries later on.

None

6.5 The presheaf model of elaboration scripts↩︎

Write \(\InitElab\) for the bi-initial natural model of elaboration scripts. We now define a presheaf model \(\mathcal{E}\) of elaboration scripts, defining the category of contexts \(\CX{\mathcal{E}}\) to be the presheaf category \(\Psh{\CX{\InitML}}\) where \(\InitML\) is the bi-initial model of Martin-Löf type theory with an answer type from § 6.3.1. Then the sorts are given by their interpretation in \(\Psh{\CX{\InitML}}\) from § 4 under the Yoneda embedding \(\Psh{\CX{\InitML}} = \CX{\mathcal{E}}\hookrightarrow\Psh{\CX{\mathcal{E}}}\). The generating operations are likewise interpreted by those from § 4 under the Yoneda embedding.

The universal property of the bi-initial natural model \(\InitElab\) of elaboration scripts determines a universal interpretation homomorphism \(\mathcal{E}\bbrk{-} \colon \InitElab\to\mathcal{E}\) which is unique up to isomorphism with the property of taking syntactic elaboration scripts to the corresponding constructs in the presheaf model \(\mathcal{E}\). More prosaically, the interpretation function translates elaboration scripts \[\begin{align} x_1 : \HypScript,\ldots,x_n:\HypScript &\vdash A\prn{x_1,\ldots,x_n}:\TypScript,\; E\prn{x_1,\ldots,x_n}:\SynScript,\; M\prn{x_1,\ldots,x_n}:\ChkScript \end{align}\] to suitable natural transformations \[\widetilde{\Tm}^n \xrightarrow{\mathcal{E}\bbrk{A}} \PMC\prn{\Tp} \qquad \widetilde{\Tm}^n \xrightarrow{\mathcal{E}\bbrk{E}} \PMC\prn[\big]{\widetilde{\Tm}} \qquad \widetilde{\Tm}^n \xrightarrow{\mathcal{E}\bbrk{M}} \prn{\alpha:\Tp}\to \PMC\prn[\big]{\Tm\prn{\alpha}}\] in the presheaf topos \(\Psh{\CX{\InitML}}\) satisfying the defining clauses of § 4.

6.6 Executing elaboration scripts by initiality↩︎

We will now transform the interpretation functions obtained from initiality (§ 6.5) into actual external elaboration procedures that can be executed in the base topos \(\BaseTopos\). To that end, we first compute more explicitly what form a section of a partial element classifier takes at the level of sets.

Similar to Procedure [proc:elaborating-type], we may give analogous procedures for elaborating synthesis-mode and checking-mode terms.

7 Conclusions and future work↩︎

Bidirectional elaboration is usually thought of as a moded logic programming problem; our contribution is a relatively simple functional semantics for the executable specification of correct-by-construction elaborators. We admit that some level of sophistication is required on the categorical side in order to substantiate the interpretation, but in return we obtain a language in which the behaviour of elaborators can be investigated using naïve equational and inequational reasoning as we have demonstrated in our case study (§ 4.6) and in our preliminary investigations of subject reduction as an inequational law (§ 5.2) and the multilinearity of elaboration combinators (§ 5.1).

Getting here, we have left many stones unturned. Here are a few of them:

1. Many type system features are left unexplored; a cumulative universe hierarchy, perhaps in the “fuss-free” style suggested by [47], would be the immediate next step.

2. Real proof assistants allow the user to leave holes in the middle of unfinished proofs; these holes correspond to metavariables that are automatically abstracted over all local variables. Incorporating holes seems to require an additional layer of polynomial monad [48].

3. Our presheaf semantics accounts for stable and dynamic elaboration automatically, in which elaboration problems may be suspended and solved in any order. We do not yet, however, account for any of the features that would necessitate dynamic elaboration, including implicit arguments and type classes. These are both areas for future work.

4. Our axioms are simple enough to postulate in a stock proof assistant like Agda or Rocq;¹⁰ although we have not yet carried this out, we believe that a key intellectual contribution of our work is the possibility of giving monadic formalisations of elaboration functions to serve as modular equational specifications for lower-level implementations, without coupling to the inessential details of important supporting algorithms (such as normalisation).

5. Our tentative discussion of multilinearity (§ 5.1) suggests a deeper connection between the design of elaboration calculi and the general study of evaluation order and polarity in programming languages. A more thorough investigation in light of both call-by-push-value [49] and the enriched effect calculus [50] is expected to bear fruit.

Finally, we stress that although we have studied a particular version of Martin-Löf type theory in this paper, our method is applicable to any suitable (i.e.second-order generalised algebraic) theory and can be tailored to the metatheorems that actually hold of that theory.

8 The partiality relative 2-monad↩︎

Intuitively, whenever the bundled evaluation is defined, so is the pointwise one, and the two agree; equivalently, the bundled side has the smaller support. It transpires in the case of the partiality monad that the lax comparison holds with no hypothesis on the codomain.

9 Proof of Theorem 1, multilinearity of elaboration combinators↩︎

For a nullary combinator \(\mathbf{1}\to A\), the multilinearity condition reduces to the unit law of the target algebra. Hence \(\underline{\ElabVar}\), \(\underline{\ElabRefl}\), \(\underline{\ElabAns}\), \(\underline{\ElabYes}\), and \(\underline{\ElabNo}\) are multilinear.

Now suppose that the judgemental structure satisfies strengthening.

The case for \(\underline{\ElabSg}\) is identical.

10 Elaboration procedures for terms↩︎

References↩︎

---

1. Lean’s language reference [1] comments that its definitional equality is “reflexive and symmetric, but not transitive”.↩︎

2. Everything in this paper can be re-done (with a bit of work) in intensional type theory. Doing so would detract from our informal exposition, but it will be necessary for the computerised implementation of our framework in future work.↩︎

3. In the actual development, we shall replace \(\PROP\) with a more restrictive subuniverse in order to automatically obtain the effective computability of elaboration.↩︎

4. When formulating a type theory about which one will prove metatheoretic results, it is important to have a base type: otherwise, the initial model of the type theory will actually contain no types! The unit type could be used, but if the unit type is the only base type, it trivialises the normalisation theorem. For this reason, we include a base type with two constructors; we could include an eliminator, but this is not needed to illustrate our methods.↩︎

5. Indeed, although it is externally the case that type equality is decidable, this will not be internally decidable. Later on, we shall choose a notion of proposition that refers to external decidability.↩︎

6. Of course, the partial element classifier also naturally gives a monad on \(\POSET\), but we will not use this structure.↩︎

7. Naturality of the extension operator is automatic: for \(h\colon X'\to X\), taking \(g\coloneq\eta_X\circ h\) in the associativity law and using the unit law yields \(\prn{f\circ h}^\dagger=f^\dagger\circ\PMC\prn{h}\). We therefore need not impose it separately.↩︎

8. Awodey requires \(\mathbb{C}\) to be small; we follow [12] in relaxing this requirement so that standard models, like the sets model, may be constructed. The category of presheaves on a large category may not be cartesian closed, but nonetheless the function spaces needed for defining natural models will be present.↩︎

9. Here we will use only the existence of the bi-initial model and will not depend on any specific details of its construction! Indeed, there can be many different constructions of the bi-initial model, each of which provides a different kind of insight.↩︎

10. Or Lean, if only its core tactics were not so tightly coupled to the axioms of classical logic which (naturally) contradict almost any synthetic approach to anything.↩︎