# Mœbius: Metaprogramming using Contextual Types

The stage where System F can pattern match on itself – Long version

Junyoung Jang  School of Computer ScienceMcGill UniversityCanada
<EMAIL_ADDRESS>,  Samuel Gélineau  SimspaceCanada ,  Stefan
Monnier  Computer ScienceUniversité de MontréalCanada<EMAIL_ADDRESS>and  Brigitte Pientka  School of Computer ScienceMcGill UniversityCanada
<EMAIL_ADDRESS>
###### Abstract.

We describe the foundation of the metaprogramming language, Mœbius, which
supports the generation of polymorphic code and, more importantly the analysis
of polymorphic code via pattern matching.

Mœbius has two main ingredients: 1) we exploit contextual modal types to
describe open code together with the context in which it is meaningful. In
Mœbius, open code can depend on type and term variables (level $0$) whose
values are supplied at a later stage, as well as code variables (level $1$)
that stand for code templates supplied at a later stage. This leads to a
multi-level modal lambda-calculus that supports System-F style polymorphism
and forms the basis for polymorphic code generation. 2) we extend the multi-
level modal lambda-calculus to support pattern matching on code. As pattern
matching on polymorphic code may refine polymorphic type variables, we extend
our type-theoretic foundation to generate and track typing constraints that
arise. We also give an operational semantics and prove type preservation.

Our multi-level modal foundation for Mœbius provides the appropriate
abstractions for both generating and pattern matching on open code without
committing to a concrete representation of variable binding and contexts.
Hence, our work is a step towards building a general type-theoretic foundation
for multi-staged metaprogramming that, on the one hand, enforces strong type
guarantees and, on the other hand, makes it easy to generate and manipulate
code. This will allow us to exploit the full potential of metaprogramming
without sacrificing the reliability of and trust in the code we are producing
and running.

Metaprogramming, Contextual Types, Polymorphism, Pattern Matching

††copyright: rightsretained††ccs: Theory of computation Modal and temporal
logics††ccs: Theory of computation Programming logic

##  1\. Introduction

Metaprogramming is the art of writing programs that produce or manipulate
other programs. This opens the possibility to eliminate boilerplate code and
exploit domain-specific knowledge to build high-performance programs.
Unfortunately, designing a language extension to support type-safe, multi-
staged metaprogramming remains very challenging.

One widely used approach to metaprogramming going back to Lisp/Scheme is using
_quasiquotation_ which allows programmers to generate and compose code
fragments. This provides a simple and flexible mechanism for generating and
subsequently splicing in a code fragment. However, it has been challenging to
provide type safety guarantees about the generated code, and although many
statically typed programming languages such as Haskell [Sheard and Jones
2022], and even dependently-typed languages such as Coq [Anand et al. 2018] or
Agda [van der Walt and Swierstra. 2012] support a form of quasiquotation, they
generate untyped code. Fundamentally, we lack a type-theoretic foundation for
quasiquotation that provides rich static type guarantees about the generated
code and allows programmers to analyze and manipulate it.

This is not to say that no advances have been made in the area of typed
metaprogramming. Two decades ago, MetaML[Taha and Sheard 2000; Taha and
Nielsen 2003] pioneered the type-safe code generation from a practical
perspective. At the same time, Davies and Pfenning [2001] observed that the
_necessity (box) modality_ allows us to distinguish the generated code from
the programs that are generating it providing a logical foundation for
metaprogramming. For example, code fragments like box(2 + 2) have boxed types
such as $\lceil$nat$\rceil$, while programs such as 6 * 3, which will evaluate
to $18$ and have type nat. Nanevski et al. [2008] extend this idea to describe
open code with respect to a context in which it is meaningful using contextual
types. For example, the code fragment box(x. x + 2) has the contextual box
type $\lceil$x:nat $\vdash$ nat$\rceil$. To use a piece of code such as box(x.
x + 2), we bind x.x+2 to the contextual variable U of type (x:nat $\vdash$
nat) using a let-box expression. At the site where we use U to eventually
splice in (x.x+2), we associate U with a delayed substitution giving a value
to x. As soon as we know what U stands for, we can apply the substitution. For
example, let box (x.U) = box(x.x+2) in box(U with 3) will bind U to the code
(x.x+2) during runtime, and produce box(3 + 2) as a result where x in the code
x+2 has been replaced by 3. We hence treat contextual variables as closures
consisting of a variable and a delayed substitution (written using the keyword
with, in this example). This allows us not only to instantiate open code
fragments, but also ensures that variables in code fragments are properly
renamed when we splice them in. Using closures and contextual types is in
contrast to using functions and function types where we could write a program
let box U = box(fn x $\rightarrow\ $ x + 2) in box(U 3). Here, evaluation
would produce the code box ((fn x $\rightarrow\ $ x + 2) 3) containing an
administrative redex, which is particularly undesirable in Mœbius, where the
program can inspect the code. Arguably, contextual types lead to more compact
generated code which is more in line with the programmer’s intention.

This line of work cleanly separates local variables (such as x) and global
variables (i.e. variables such as U, accessible at every stage) into two
zones. This provides an alternative to the Kripke-style view where a stack of
contexts models the different stages of computation. While the latter is
appealing, since box (quote) and unbox (unquote) match common metaprogramming
practice, reasoning about context stacks and variable dependencies is
difficult. The let box formulation of the modal necessity leads to an arguably
much simpler formulation of the static and operational semantics, which we see
as an advantage.

In this paper, we introduce a core metaprogramming language, Mœbius, which
allows us to generate and, importantly, analyze polymorphically-typed open
code fragments using pattern matching. Our starting point is the lambda-
calculus presented by Nanevski et al. [2008] where they distinguish between
local and global variables. This formulation makes evaluation order explicit
using let box-expressions. This allows us to more clearly understand the
behavior of multi-staged metaprograms that work with open code. We extend
their work in three main directions:

1) Generating polymorphic code. First, we generalize their language to support
System F style polymorphism and polymorphic code generation. In particular,
$\lceil$’a:*, x:’a, f: ’a $\rightarrow\ $ ’a $\vdash$ ’a$\rceil$ describes a
polymorphic code fragment such as box(’a, x, f. f (f x)). A context in our
setting keeps track of both term and type variables, hence treating both
assumptions uniformly. This allows us to support code generation for
polymorphic data structures such as polymorphic lists.

2) Generating code that depends on other code and type templates. Second, we
generalize contextual types to characterize code that depends itself on other
code fragments and support a composition of code fragments which avoids
creating administrative redexes due to boxing. This is achieved by
generalizing the two-zone formulation by Davies and Pfenning [2001] and
Nanevski et al. [2008], which distinguishes between two levels, to an n-ary
zone formulation and leads us to a multi-level contextual modal lambda-
calculus. The two-zone formulation by Davies, Pfenning, et. al. is then a
special case of our multi-level calculus. For example, $\lceil$c:(x:nat
$\vdash$ nat), x:nat $\vdash$ nat$\rceil$ can describe a piece of code like
box(c, x. x + c with x) that eventually computes a natural number, but depends
on the variable x:nat and on another piece of open code c:(x:nat $\vdash$
nat). Note that c simply stands for a piece of open code and any reference to
it will have to provide an x with which to close it – this is in contrast to
an assumption of type $\lceil$x:nat $\vdash$ nat$\rceil$ which stands for the
boxed version of a piece of code. This allows us to elegantly and concisely
combine code fragments:

⬇

1let box (y. R) = box (y. y + 2) in

2let box (c,x. U) = box (c,x. 3 * x + (c with (2 * x))) in

3 box (y. U with ((y. R with y), y))

which results in the code box(y. 3 * y + (2 * y + 2)). We say that
$\lceil$c:(x:nat $\vdash$ nat), x:nat $\vdash$ nat$\rceil$ is a level 2
contextual type, as it depends on x:nat (level 0) and c:(x:nat $\vdash$ nat)
(level 1) assumptions. This view is in contrast to the two-level modal lambda-
calculus described in Davies and Pfenning [2001] or Nanevski et al. [2008],
where we would need to characterize code depending on other code using the
type $\lceil$c:$\lceil$x:nat $\vdash$ nat$\rceil$, x:nat $\vdash$ nat$\rceil$.
However, this would not allow us to splice in (y. y + 2) for c in the code
bound to U; instead, we would need to splice in box(y. y + 2) for c and
retrieve the code (y. y + 2) using a let-box-expression. The code bound to U
in line 2 would need to be written as: box (c,x. let box (y. R’) = c in 3 * x
+ (R’ with (2 * x))). This would then generate the code box(y. let box (y. R’)
= box(y. y + 2) in 3 * y + (R’ with (2 * y))) which contains an administrative
redex. Our work avoids the generation of any administrative redexes and hence
generates code as intended and envisioned by the programmer.

We further extend this idea of code templates uniformly to type templates,
i.e. we are able to describe the skeleton and shape not only of code but also
of types themselves. As a consequence, Mœbius sits between System F and System
Fω where we support term and type-level computation.

3) Pattern matching on code. Third, we extend the multi-level contextual modal
lambda-calculus with support for pattern matching on code. This follows ideas
in Beluga [Pientka 2008; Pientka and Dunfield 2008] where pattern matching on
higher-order abstract syntax (HOAS) trees is supported. However, in Beluga, we
separate the language in which we write programs from the language that
describes syntax. In Mœbius, such a distinction does not exist and meta-
programs can pattern match on code that represents another (meta-)program in
the same language. We view the syntax of code through the lenses of higher-
order abstract syntax treating variables abstractly and characterize pattern
variables using multi-level contextual types. In fact, multi-level contextual
types are the key to characterizing pattern variables in code – especially
code that may itself contain box-expressions and let box expressions!

Pattern matching on polymorphic code may refine type variables, as is typical
in indexed or dependently typed systems. For example, when we pattern match on
a piece of code of type $\lceil$x:’a $\vdash$ ’a$\rceil$, then one of the
branches may have the pattern box(x. 0), which has type $\lceil$x:int $\vdash$
int$\rceil$. Hence, we need to use the constraint ’a = int to type check the
body of the branch. We, therefore, extend our multi-level contextual modal
lambda calculus to generate and track type constraints, and type-check a given
expression modulo constraints. Despite the delicate issues that arise in
supporting System F style polymorphism and pattern matching on code, our
operational semantics and the accompanying type preservation proof is
surprisingly compact and clean.

We view our work as a step towards building a general type-theoretic
foundation for multi-staged metaprogramming, which enforces strong type
guarantees and makes it easy to generate and manipulate code. This will allow
us to exploit the full potential of metaprogramming without sacrificing the
reliability of and trust in the code we are producing and running.

##  2\. Motivation

To illustrate the design and capabilities of Mœbius, we discuss several
examples below.

###  2.1. Example: Generating Open Polymorphic Code

First, we implement the function nth which generates the code to look up the
i-th element in a polymorphic list v where v is supplied at a later (next)
stage.

⬇

nth : int $\rightarrow\ $ $\lceil$’a:*, v:’a list $\vdash$ ’a$\rceil$

nth n = if n <= 0 then

box(’a,v. hd v )

else

let box (’a,v. X) = nth (n - 1) in box(’a,v. X with ’a, tl v) )

The result of the computation has the contextual type $\lceil$’a:*, v:’a list
$\vdash$ ’a$\rceil$. This type describes open code at level $1$ that has type
’a and depends on variables from level $0$, namely ’a:*, v:’a list. In
general, a contextual type $\lceil$$\Psi$ $\vdash^{n}$ T$\rceil$ characterizes
a code template at level $n$ of type T. This code template may depend on
locally bound variables in $\Psi$ which contains variables at levels strictly
lower than $n$. The code template may also refer to outer variables that are
greater or equal to $n$ and whose values are computed during run-time. This
principle is what underlies the design of the multi-level modal lambda-
calculus and is worth highlighting:

_Mantra: a code template $\lceil\Psi\vdash^{n}T\rceil$ at level $n$, can
depend on locally bound variables $\Psi$ from levels less than $n$ and outer
variables that have levels greater or equal to $n$._

In the above example, the result that we return in the recursive case is
box(’a,v. X with ’a, tl v). The code inside the box, depends on the locally
bound variables ’a and v (all of which have level $0$) and uses the outer
variable X (which has level $1$). During runtime, X will be bound to the
result of the recursive call nth (n-1). Given an n, the program nth will
recursively build up the code

box(’b, v. hd
(${\underset{n}{\underbrace{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\footnotesize{\@listingGroup{ltx_lst_identifier}{tl}}{\@listingGroup{ltx_lst_space}{
}}(..{\@listingGroup{ltx_lst_space}{
}}({\@listingGroup{ltx_lst_identifier}{tl}}}}}}}}$ v))))

Ultimately producing a code template that depends only on variables at level
$0$.

Subsequently, we write $\vdash^{n}$ in a contextual type, if we want to make
explicit the level at which a term is well-typed, but we will mostly omit the
levels when they can be easily inferred.

###  2.2. Example: Combining Code Templates

Next, we generate code that depends on two other code templates, c and d, both
of which have the contextual type (x:int $\vdash$1 int). The type of these
templates is at level $1$, as they depend on the variable x:int, which is at
level $0$. Hence, the overall generated code template lives at level $2$.

In this simple example, we combine the two templates c and d in different ways
depending on whether the input to the function combine is true or false. From
a computational view, if the input evaluates to true, then we generate code
that, during runtime, will first evaluate the template d and subsequently pass
its result to the template c. If the input evaluates to false, then we do the
opposite, i.e., we will first evaluate the template c and then pass its result
to d.

⬇

combine : bool $\rightarrow\ $ $\lceil$c:(x:int $\vdash$1 int) , d:(x:int
$\vdash$1 int), x:int $\vdash$2 int$\rceil$

combine p = if p then

box(c,d,x. (fun y $\rightarrow\ $ c with y) (d with x))

else

box(c,d,x. (fun y $\rightarrow\ $ d with y) (c with x))

One might wonder whether we could have generated the code box(c,d,x. c with (d
with x)) instead of box(c,d,x. (fun y $\rightarrow\ $ c with y) (d with x)).
To understand the difference in the runtime behaviour, we use the following
instantiation: (x. x+2*x) for c, (x. x*3) for d, and 3 for x.

When we use the code box(c,d,x. (fun y $\rightarrow\ $ c with y) (d with x))
with (x. x+2*x), (x. x*3), 3, then we run the code (fun y $\rightarrow\ $ y +
2*y) (3*3), which will first evaluate 3*3 to 9 and then compute 9 + 2*9, which
returns $27$. When we use box(c,d,x. c with (d with x)) with the same
instantiation, we will evaluate the code 3*3 + 2*(3*3), i.e. we will evaluate
the code 3*3, which we obtain by instantiating d with x twice! Effectively, we
are using a call-by-name evaluation strategy, as the execution of 3*3 gets
delayed. This example hence illustrates yet another difference between
closures and function applications.

Last, this example also highlights the difference between levels and stages.
The result for combine is a contextual type at level $2$, since it depends on
other code templates. However, we are generating the code in one stage.

The difference between levels and stages can also be understood from a logical
perspective: stages characterize _when code is generated_ ; as such they
describe a property of a boxed type in a positive position. Levels express a
property of the assumptions (i.e. negative occurrences) that are used in a
boxed type, namely that _how code is used_. In particular, levels allow us to
express directly and accurately the fact that code may depend not only on
closed values, but also on open code. This allows us to describe code that may
itself depend on other code.

###  2.3. Example: Type Templates

We support System-F style polymorphism in Mœbius. As a consequence, we may not
only want to describe open code, but also types that are open (i.e. type
templates). For example, consider the contextual type

⬇

$\lceil$’a:(’c:* $\vdash$ *), f: $\forall$’b. ’b $\rightarrow\ $ (’a with ’b)
$\rightarrow\ $ int $\vdash$ int$\rceil$

This describes a piece of code that relies on the polymorphic function f,
which computes an int. Here ’a describes a type template – it stands for some
type that has one free type variable. We again associate ’a with a
substitution which, in this example, renames the variable ’c in the type
template to be ’b. As a consequence, f in fact stands for a family of
functions! If we instantiate ’a with the type template ’c.’c, then f has type
$\forall$ ’b. ’b $\rightarrow\ $ ’b $\rightarrow\ $ int. If we instantiate it
with ’c. ’c $\rightarrow\ $ c’, then f stands for a function of type $\forall$
b’. b’ $\rightarrow\ $ (b’ $\rightarrow\ $ b’) $\rightarrow\ $ int. In System
Fω, we would have declared this type as: $\lceil$’a: * $\rightarrow\ $ *,
f:$\forall$ ’b. ’b $\rightarrow\ $ ’a ’b $\rightarrow\ $ int $\vdash$
int$\rceil$

The support of type templates that have contextual kinds means that Mœbius
sits between System Fω where we have type level functions and System F. Using
type variables that have a contextual kind brings a distinct advantage over
System Fω: as we apply the substitution associated with the type variable ’a
as soon as we know its instantiation, we can compare two types simply by
structural equality, and we do not need to reason about type-level
computation.

The ability to characterize holes in types and terms is particularly important
when we consider pattern matching on code. In our setting, polymorphic
programs may contain explicit type applications, and hence, we not only
pattern match on terms but also on types.

###  2.4. Example: Lift Polymorphic Data Structures

In Mœbius, as in other similar frameworks, we need to lift values explicitly
to the next stage. Lifting integers is done by simply traversing the input and
turning it into its syntax representation. This is straightforward. We write
here $\lceil$int$\rceil$ as an abbreviation for $\lceil$ $\vdash$1
int$\rceil$, which describes a closed integer at level $1$, i.e. the minimum
level that generated code can have.

⬇

lift_int : int $\rightarrow\ $ $\lceil$int$\rceil$

lift_int n = if n = 0 then box(0) else let box(X) = lift_int (n - 1) in box(X
+ 1)

To lift polymorphic lists, we need to lift values of type ’a to their
syntactic representations and then lift lists themselves. This generic lifting
function for values of type ’a will intuitively have the type ’a $\rightarrow\
$ $\lceil$’a$\rceil$. But how can we ensure that the type variable ’a can be
used inside a contextual type at level $1$? – To put it differently, how can
we guarantee that the type variable persists when we transition inside the
contextual box type? We again use the intuition that _code and types at stage
$n$, have locally bound variables from levels less than $n$, but they may
depend on outer variables that have levels greater or equal to $n$._ For
$\lceil$’a$\rceil$ to be a well-formed type, the type variable ’a must be
declared at level $1$ or higher.

Hence, we declare the type variable ’a as a type template ’a: ( $\vdash$ *).
We omit here again the level $1$, since it can be inferred from the
surrounding context.

⬇

lift_list : (’a:( $\vdash$ *)) $\rightarrow\ $ ’a list $\rightarrow\ $ (’a
$\rightarrow\ $ $\lceil$’a$\rceil$) $\rightarrow\ $ $\lceil$’a list$\rceil$

lift_list l lift = match l with

| [] $\rightarrow\ $ box([])

| x::xs $\rightarrow\ $ let box X = lift x in let box XS = lift_list xs lift
in box(X::XS)

For terms, we have a natural interpretation of running and evaluating code.
This rests on the idea that a term at stage 1 can always be used at stage 0.

⬇

eval_int : $\lceil$int$\rceil$ $\rightarrow\ $ int

eval_int x = let box X = x in X

eval_list : (’a:( $\vdash$ *)) $\rightarrow\ $ $\lceil$’a list$\rceil$
$\rightarrow\ $ ’a list

eval_list v = let box V = v in V

Similarly, we can run and evaluate polymorphic code. Again we rely on the idea
that the type variable a is describing types at level $1$ or below.

This concept also allows us to lift the result of a function rev (’a:*)
$\rightarrow\ $ ’a list $\rightarrow\ $ ’a list. In the code below, we simply
call rev with ’a (or more precisely with ’a with .).

⬇

lift_rev_list : (’a:( $\vdash$ *)) $\rightarrow\ $ ’a list $\rightarrow\ $ (’a
$\rightarrow\ $ $\lceil$’a$\rceil$) $\rightarrow\ $ $\lceil$’a list$\rceil$

lift_rev_list l = lift_list (rev l)

###  2.5. Example: Staged Polymorphic Map

With the ability to generate polymorphic code, there are many useful programs
we can write, for example a staged polymorphic map function. We omit again the
levels, as they can be inferred.

⬇

% Similarly, we can implement a staged version of fold.

% \begin{lstlisting}

% fold : (a:( $\vdash$1 *)) $\rightarrow\ $ a list $\rightarrow\ $ (a
$\rightarrow\ $ $\lceil$ $\vdash$1 a)$\rceil$) $\rightarrow\ $ $\lceil$b:*,
g:a $\rightarrow\ $ b $\rightarrow\ $ b, base:b $\vdash$ b$\rceil$

% fold l lift = match l with

% | [] $\rightarrow\ $ box( b, g, base . base )

% | x::xs $\rightarrow\ $ let box (b,g,base. R) = (fold xs lift) in

% let box X = lift x in

% box( b, g, base. R with _, g, g X base )

% \end{lstlisting}

% Here we see the power of using an open code with an associated

% substitution. While we simply rename the type variable \lstinline!b!

% and the name of the function \lstinline!g!, we instantiate the

% variable \lstinline!base! with the term \lstinline!g X base!. The

% delayed substitutions that we associate with a contextual variable

% will be eagerly applied as soon as we know what \lstinline!R! stands

% for. The alternative to contextual types and contextual variables

% would be to represent code fragments using functions that abstract

% over \lstinline!b!, \lstinline!g!, and \lstinline!base!. However, to

% use this function we need to apply it \-- this function application is

% however not done eagerly as soon as we know what the function stands

% for. It will only happen when we run the generated code. As a

% consequence, the actual generated code will contain these

% administrative redexes that will always reduce. Associating contextual

% variables with a substitution anticipates the creation and reduction

% of the redex and avoids it by creating a closure with a suspended

% substitution.

\subsection{Example: Multi-Staged Polymorphic Code}

We now give an example of multi-staged polymorphic code generation. Here,
names

\lstinline!l! and \lstinline!liftA! in the function type are to help

the understanding, and are not part of our syntax. It is a multi-staged
version of

\lstinline!map_reduce!. We annotate all the contextual types and kinds

with their level, although the level can be inferred from where the

type variable is used. It serves as another illustration that the

level manages variable dependencies and cross-stage
persistence\cite{Taha:TCS00}, while

the staging manages when code is generated. In the code below, we omit

writing the identity substitution that is associated with variables

writing for example simply \lstinline!R! instead of \lstinline!(R with
’b,f,liftB)!.

\begin{lstlisting}

map_reduce : (’a:( $\vdash$${}^{2}\;$*)) $\rightarrow\ $ (l:’a list)
$\rightarrow\ $ (liftA:’a $\rightarrow\ $ $\lceil$
$\vdash$${}^{2}\;$’a$\rceil$)

$\rightarrow\ $ $\lceil$’b:( $\vdash$${}^{1}\;$*), f:’a $\rightarrow\ $ ’b,
liftB:’b $\rightarrow\ $$\lceil$ $\vdash$${}^{2}\;$’b$\rceil$

$\vdash$${}^{2}\;$$\lceil$’c:*, g:’b $\rightarrow\ $’c $\rightarrow\ $’c,
base:’c $\vdash$${}^{1}\;$’c$\rceil$$\rceil$

map_reduce l liftA = match l with

| [] $\rightarrow\ $ box (’b,f,liftB. box(’c,g,base. base) )

| x::xs $\rightarrow\ $

let box (’b,f,liftB. R) = map_reduce xs liftA in

let box A = liftA x in box (’b,f,liftB.

let box (’c,g,base. M) = R in

let box X’ = liftB (f A) in box (’c,g,base. M with ’c, g, (g X’ base)))

Multi-stage code generation generates code incrementally in several stages.
For example, map_reduce generates the final code in $2$ stages. This is
evident, since the return type has a boxed type nested inside another boxed
type.

In the function declaration of map_reduce, we declare (’a:( $\vdash$2 *)), as
we want to use a at any stage $2$ or below. However, the other declarations l
and liftA are declared at level $0$ – they will be inaccessible inside a box-
expression. Therefore, this forces us to lift the head of the list (liftA x)
first before we build our result, as when we enter the scope of ’b:( $\vdash$1
*); f:’a $\rightarrow\ $ ’b, liftB:’b $\rightarrow\ $ $\lceil$ $\vdash$2
’b$\rceil$ we only keep the declaration (’a:( $\vdash$2 *)), but the outer
declarations at level $0$ get dropped as they become inaccessible. Similarly,
when we enter the inner contextual box $\lceil$’c:*, g:’b $\rightarrow\ $ ’c
$\rightarrow\ $ ’c, base:’c $\vdash$1 ’c$\rceil$, we will drop all the outer
assumptions at level $0$ (as they get overwritten by the new local context
’c:*, g:’b $\rightarrow\ $ ’c $\rightarrow\ $ ’c, base:’c, but assumptions at
levels higher than $0$ remain accessible. The levels, therefore, manage scope
dependencies – especially as we cross different stages.

###  2.6. Example: Working with Church Encodings and Pattern Matching

The last example illustrates the benefits of generating code as intended by
programmers and the use of pattern matching. We represent the type of natural
numbers using Church encoding as $\lceil$’a:*, x:’a, f:’a $\rightarrow\ $ ’a
$\vdash$ ’a$\rceil$. However, unlike the usual Church encoding where we use
functions and function application, we exploit the power of contextual types
instead. This then allows for elegant implementations of addition or other
arithmetic operations. We will again omit writing the identity substitutions,
i.e. for example, writing simply N instead of (N with ’a,x,f).

⬇

gen_church: int $\rightarrow\ $ $\lceil$’a:*,x:’a, f:’a $\rightarrow\ $ ’a
$\vdash$ ’a$\rceil$

gen_church n = if n = 0 then box(’a,x,f. x)

else let box(’a,x,f. N) = gen_church (n-1) in box(’a,x,f. f N)

add: $\lceil$’a:*,x:’a, f:’a $\rightarrow\ $ ’a $\vdash$ ’a$\rceil$
$\rightarrow\ $ $\lceil$’a:*,x:’a, f:’a $\rightarrow\ $ ’a $\vdash$ ’a$\rceil$

$\rightarrow\ $ $\lceil$’a:*,x:’a, f:’a $\rightarrow\ $ ’a $\vdash$ ’a$\rceil$

add n m = let box (’a,x,f. N) = n in

let box (’a,x,f. M) = m in box(’a,x,f. N with ’a, M, f)

Working with the Church encoding directly as syntactic representations again
allows us to generate code as the programmer intended. For example adding the
Church encoding of $2$ and the Church encoding of $3$ will yield the Church
encoding of $5$ – not some program that will evaluate to $5$ when we run the
result. As we know the structure of the Church encoding for numbers, we can
also inspect it via pattern matching. This opens new possibilities to
implement the predecessor function directly via pattern matching instead of
the usual more painful solution when we work with functions and function
applications.

⬇

pred n = case n of

| box(’a,x,f. x) $\rightarrow\ $ box(’a,x,f. x)

| box(’a,x,f. f X) $\rightarrow\ $ box(’a,x,f. X)

The first case captures the fact that the input n is a representation of $0$,
and we simply return it. In the second case, we know that it is an application
f X where $X$ is the pattern variable denoting a code template of type
(’a:*,x:’a,f:’a $\rightarrow\ $ ’a $\vdash$ ’a). We hence simply strip off the
f.

We delay a more in-depth discussion of pattern matching on code to Sec. 4.

##  3\. A Multi-level Modal Lambda-Calculus with Polymorphism

We describe first a modal polymorphic lambda-calculus where we use multi-level
contextual types to characterize open code. This calculus serves as a
foundation to generate polymorphic open code. We then extend this calculus to
support pattern matching on polymorphic code in Sec. 4.

$\begin{array}[]{llcl}\mbox{Types}&T,S&\mathrel{::=}&\alpha[\sigma]\mathrel{\mid}T_{1}\rightarrow
T_{2}\mathrel{\mid}(\alpha{:}(\Psi\vdash^{n}*))\rightarrow
T\mathrel{\mid}\lceil\Psi\vdash^{n}T\rceil\\\
\mbox{Terms}&e&\mathrel{::=}&x[\sigma]\mathrel{\mid}\mathsf{fn}\;x\rightarrow
e\mathrel{\mid}e_{1}\;e_{2}\mathrel{\mid}\mathsf{Fn}\;\alpha^{n}\rightarrow
e\mathrel{\mid}e\;(\hat{\Psi}^{n}.T)\mathrel{\mid}\\\
&&&\mathsf{box}(\hat{\Gamma}^{n}.\,e)\mathrel{\mid}\mathsf{let}\,\mathsf{box}\;(\hat{\Gamma}^{n}.u)\;{=}\;e_{1}\;\mathsf{in}\;e_{2}\\\\[5.0pt]
\hline\cr\\\\[-5.0pt]
\mbox{Substitution}&\sigma&\mathrel{::=}&\cdot\mathrel{\mid}\sigma,\hat{\Psi}^{n}.e\mathrel{\mid}\sigma;x^{n}\mathrel{\mid}\sigma,\hat{\Psi}^{n}.T\mathrel{\mid}\sigma;\alpha^{n}\\\
\mbox{Context}&\Gamma,\Psi,\Phi&\mathrel{::=}&\cdot\mathrel{\mid}\Gamma,x{:}(\Psi\vdash^{n}T)\mathrel{\mid}\Gamma,\alpha{:}(\Psi\vdash^{n}*)\\\
\mbox{Erased
context}&\hat{\Gamma},\hat{\Psi},\hat{\Phi}&\mathrel{::=}&\cdot\mathrel{\mid}\hat{\Gamma},x^{n}\mathrel{\mid}\hat{\Gamma},\alpha^{n}\end{array}$
Figure 1. Syntax of Multi-Level Modal Lambda-Calculus

###  3.1. Syntax

We describe the syntax of Mœbius in Fig. 1. Central to Mœbius are multi-level
contextual types and kinds that describe code and type templates together with
the context in which they are meaningful. A multi-level contextual type
$(\Psi\vdash^{n}T)$ describes code of type $T$ in a context $\Psi$ where all
assumptions in $\Psi$ are themselves at levels below $n$. Variables at level
$n$ or above are viewed as global variables whose values will be computed
during run-time. Similarly, a multi-level contextual kind $(\Psi\vdash^{n}*)$
describes a type fragment in a context $\Psi$.

We treat all variable declarations in our context uniformly; hence our typing
context keeps track of variable declarations $x:(\Psi\vdash^{n}T)$ and type
declarations $\alpha:(\Psi\vdash^{n}*)$. If $n=0$, then we recover our
ordinary bound variables of type $T$ from $x:(\cdot\vdash^{0}T)$. As there are
no possible declarations at a level below $0$, this context is necessarily
empty (in fact it doesn’t even exist). Similarly, a type declaration
$\alpha:(\cdot\vdash^{0}*)$ denotes simply a type variable $\alpha$.

A contextual type or term variable is associated with a substitution, written
here as $\alpha[\sigma]$ and $x[\sigma]$. Intuitively, if a contextual
variable $x:(\Psi\vdash^{n}\\_)$ is declared in some context $\Phi$, then the
substitution $\sigma$ provides instantiations for variables in $\Psi$ in terms
of $\Phi$. As soon as we know the instantiation for $x$, we apply the
substitution $\sigma$. We previously wrote (x with $\sigma$) as concrete
source syntax in our code examples in Sec. 2.

Mœbius is a generalization of the modal lambda-calculus described by Davies
and Pfenning [2001] or Nanevski et al. [2008] which separates the global
assumptions in a meta-context from the local assumptions. This gives us a two-
zone representation of the modal lambda-calculus. Mœbius generalizes this work
to an $n$-ary zone representation. If $n=1$, then we obtain the two-zone
representation from the previous work. Variables at level $1$ correspond to
the meta-variables which live in the global meta-context, and variables at
level $0$ correspond to the ordinary bound variables.

Our notion of multi-level contextual types is also similar to the work by
Boespflug and Pientka [2011]. However, this work was concerned with developing
a multi-level contextual logical framework. We adopt the ideas to polymorphic
multi-staged programming.

Mœbius supports boxed contextual types, $\lceil\Psi\vdash^{n}T\rceil$ which
describe a code template of type $T$ in the context $\Psi$. The level $n$
enforces that the given template can only depend locally on variables at
levels below $n$. This will allow us to cleanly manage variable dependencies
between stages and will serve as a central guide in the design of Mœbius. In
addition, we support function types (written as $T_{1}\rightarrow T_{2}$) and
polymorphic function $(\alpha{:}(\Psi\vdash^{n}*))\rightarrow T$ which
abstract over type variables $\alpha$. The ordinary polymorphic function space
is a special case where $n=0$. As a type variable $\alpha$ stands in general
for a type-level template, we associate it with a substitution $\sigma$,
written as $\alpha[\sigma]$. As soon as we know what type variable $\alpha$
stands for, we splice it in and apply $\sigma$. This ensures that the type
makes sense in the context where it is used. When $n=1$, we can model types in
System Fω. For example, in System Fω, we might define:
$(\alpha{:}*\rightarrow*)\rightarrow(\beta:*)\rightarrow\alpha~{}\beta$. In
Mœbius, we declare it instead as:
$(\alpha{:}(\\_{:}*\vdash^{1}*))\rightarrow(\beta:*)\rightarrow\alpha[\beta]$
avoiding type-level functions and creating a type-level function application.

Our core language of Mœbius includes functions ($\mathsf{fn}\;x\rightarrow
e$), function application ($e_{1}\;e_{2})$, type abstractions
($\mathsf{Fn}\;\alpha^{n}\rightarrow e$) and type application
($e\;(\hat{\Psi}^{n}.T)$). We carry the level $n$ of $\alpha$ as an
annotation; this is needed for technical reasons when we define simultaneous
substitution operations. Further, we include $\mathsf{box}$ and
$\mathsf{let}\,\mathsf{box}$ expressions to generate code and use code. In
particular, $\mathsf{box}(\hat{\Gamma}^{n}.\,e)$ describes code $e$ together
with the list of (local) variables $\hat{\Gamma}^{n}$ which may be used in
$e$. The level $n$ states again that these bound variables are below level $n$
and we ensure that $n$ here is greater than 0 during typing, as an expression
$e$ at level $0$ is an ordinary expression, not a code fragment. To use a
program $e_{1}$ that generates a code template, we bind a contextual variable
$u$ to the result of evaluation of $e_{1}$ and use the result in a body
$e_{2}$. This is accomplished via
$\mathsf{let}\,\mathsf{box}\;(\hat{\Gamma}^{n}.u)\;{=}\;e_{1}\;\mathsf{in}\;e_{2}$.

A substitution is formed by extending a given substitution with a contextual
term $(\hat{\Psi}^{n}.e)$, a contextual type $(\hat{\Psi}^{n}.T)$, a term
variable $x$, or a type variable $\alpha$. The latter extensions are necessary
to allow us to treat substitutions as simultaneous substitutions. In
particular, when pushing a substitution $\sigma$ inside a function
$\mathsf{Fn}\;\alpha^{n}\rightarrow e$, we need to extend it with a mapping
for $\alpha$. However, we would need to eta-expand $\alpha$ based on its type
to obtain a proper contextual object, as $\alpha$ by itself would not be a
legitimate type. Therefore, we allow extensions of substitutions with an
identity mapping, which is written as $\sigma;\alpha^{n}$. Similarly, if we
push the substitution inside $\mathsf{box}(\hat{\Gamma}^{n}.\,e)$ then we may
need to extend the simultaneous substitution with mappings for the variables
listed in $\hat{\Gamma}$, but we lack the type information to expand a term
variable $x$ to a proper contextual term. This issue is not new and is handled
similarly in Nanevski et al. [2008] in a slightly different setting.

In contrast to the two-zone formulation of the modal lambda-calculus in
Nanevski et al. [2008], which has different substitution operations for
ordinary bound variables (variables at level $0$) and meta-variables
(variables at level $1$), our substitution encompasses both kinds of
substitutions.

#### Remark 1:

We define the level of a context: $\mathsf{level}(\Psi)=n$ iff for all
declarations $x{:}(\\_\vdash^{k}\\_)$ in $\Psi$ have $k<n$. In other words,
the level of context $\Psi$ ensures that all variables in $\Psi$ are at
strictly smaller levels. We often make the level explicit as a superscript,
$\Psi^{n}$, which describes a context $\Psi$ where $\mathsf{level}(\Psi)=n$.
Note that we abuse the functional notation here, since $\mathsf{level}$ does
not have a unique result for a given context $\Psi$.

#### Remark 2:

The erasure of type annotations from the context $\Psi^{n}$ drops all the type
and kind declarations from $\Psi$, but retains the level to obtain
$\hat{\Psi}^{n}$.

$\begin{array}[]{lcl}\mathsf{erase}(\cdot)&=&\cdot\\\
\mathsf{erase}(\Psi,x{:}(\Phi\vdash^{n}T))&=&\mathsf{erase}(\Psi),x^{n}\\\
\mathsf{erase}(\Psi,\alpha{:}(\Phi\vdash^{n}*))&=&\mathsf{erase}(\Psi),\alpha^{n}\end{array}$

Abusing notation, we often simply write $\hat{\Psi}^{n}$ for the erasure of
type annotations from the context $\Psi^{n}$ instead of
$\mathsf{erase}(\Psi)=\hat{\Psi}$.

#### Remark 3:

We write $\mathsf{id}(\hat{\Phi})$ for the identity substitution that has
domain $\Phi$. It is defined as follows:

$\begin{array}[]{lcl}\mathsf{id}(\cdot)&=&\cdot\\\
\mathsf{id}(\hat{\Phi},~{}x^{n})&=&\mathsf{id}(\hat{\Phi});x^{n}\\\
\mathsf{id}(\hat{\Phi},~{}\alpha^{n})&=&\mathsf{id}(\hat{\Phi});\alpha^{n}\end{array}$

#### Remark 4:

We sometimes write simply $x{:}T$ for $x{:}(\Psi\vdash^{0}T)$ for readability;
similarly we write simply $x$ for $x[\mathsf{id}{(\hat{\Psi})}]$, i.e. when
$x$ is associated with the identity substitution and
$\mathsf{erasure}(\Psi)=\hat{\Psi}$.

Before moving to the typing rules, we take a closer look first at our typing
contexts and then at our substitutions, because they are both key parts of the
design of our language and they hopefully give a good general intuition about
the way the system works.

###  3.2. Context operations

First, we note that we maintain order in a context and hence contexts must be
sorted according to the level of assumptions $x{:}(\Psi\vdash^{n}T)$. One
should conceptualize this ordered context as a stack of sub-contexts, one for
each level of variables. Let $\Psi(k)$ be the subcontext of $\Psi^{n}$ with
only assumptions of level $k$. Then,
$\Psi^{n}=\Psi(n-1),\Psi(n-2),\ldots,\Psi(1),\Psi(0)$. Slightly abusing
notation we write ${{\Psi(i)},{\Psi(i-1)}}$ for appending the context
$\Psi(i)$ and the context $\Psi(i-1)$. Note that $\Psi(0)$ contains only
declarations of type $(\cdot\vdash^{0}T)$ and we recover our ordinary typing
context which simply contains variable declarations $x{:}T$. The context
$\Psi^{n}$ is essentially an $n$-ary zone generalization of the two-zone
context present in Davies and Pfenning [2001] work. We can recover their two
zones when $n=1$. We opt here for a flattened presentation of the $n$-ary
zones of contexts in order to simplify operations on contexts. Keeping the
context sorted not only provides conceptual guidance, but also helps us to
handle cleanly the dependencies among variable declarations.

Keeping the context sorted comes at a cost: extending a context must preserve
this invariant. However, restricting a context, which is necessary as we move
up one stage, i.e. we move inside a box, is simpler. We therefore define and
explain two main operations on context: restricting a context and merging two
contexts. To chop off all variables below level $n$ from an ordered context
$\Gamma$, we write $\Gamma|_{n}$. To merge two ordered contexts $\Gamma$ and
$\Psi$ we write ${{\Gamma}\oplus{\Psi}}$. With merging defined, insertion of a
new assumption into a context is a special case. For compactness, we write $K$
for a type or a kind in the definition of the context operations in Fig. 2.

$\begin{array}[]{lcll}\lx@intercol\mbox{Merging
contexts:}\quad{{\Psi}\oplus{\Phi}}=\Gamma\hfil\lx@intercol\\\
{{\cdot}\oplus{\Phi}}&=&\Phi\\\ {{\Psi}\oplus{\cdot}}&=&\Psi\\\
{{\Psi,x{:}(\Gamma\vdash^{n}K)}\oplus{\Phi,y{:}({\Gamma^{\prime}}\vdash^{k}K^{\prime})}}&=&({{\Psi,x{:}(\Gamma\vdash^{n}K)}\oplus{\Phi}}),y{:}({\Gamma^{\prime}}\vdash^{k}K^{\prime})&\text{if
$k\leq n$}\\\
{{\Psi,x{:}(\Gamma\vdash^{n}K)}\oplus{\Phi,y{:}({\Gamma^{\prime}}\vdash^{k}K^{\prime})}}&=&({{\Psi}\oplus{\Phi,y{:}({\Gamma^{\prime}}\vdash^{k}K^{\prime})}}),x{:}({\Gamma}\vdash^{n}K)&\text{otherwise}\\\\[7.5pt]
\lx@intercol\mbox{Chopping lower
context:}\quad\Psi|_{n}~{}=~{}\Phi\hfil\lx@intercol\\\ (\cdot)|_{n}&=&\cdot\\\
(\Psi,x{:}(\Phi\vdash^{k}K)|_{n}&=&\Psi|_{n}&\text{if $k<n$}\\\
(\Psi,x{:}(\Phi\vdash^{k}K))|_{n}&=&\Psi,x{:}(\Phi\vdash^{k}K)&\text{otherwise}\end{array}$
Figure 2. Merging and chopping of contexts

The chopping operation for the lower context allows us to drop all variable
assumptions below the given level from a context. If $k\leq n$, then
$(\Psi^{k})|_{n}=\cdot$.

Merging of two independent, sorted contexts is akin to the merge step of the
merge-sort algorithm and therefore inherits many of its properties. In
particular, the merge of two sorted independent contexts is again a sorted
context. It is also stable, in the sense that the relative positions of any
two assumptions in $\Psi^{n}$ or in $\Phi^{k}$ is preserved in
${{\Psi^{n}}\oplus{\Phi^{k}}}$.

When we merge two sorted contexts $\Psi$ and $\Phi$, i.e. when for every
declaration $x{:}(\\_\vdash^{n}\\_)$ in $\Psi$, we have
$\mathsf{level}(\Phi)\leq n+1$, we simply write ${{\Psi},{\Phi}}$ (see
Appendix A for the definition). While defining a separate append operation on
sorted contexts is not necessary, it is often conceptually easier to read and
use. It is also more concise.

###  3.3. Simultaneous Substitution Operation

We concentrate here on the simultaneous substitution operation, but the single
substitution operation follows similar ideas.

In our grammar, simultaneous substitutions are defined without their domain.
However, when applying a simultaneous substitution $\sigma$, we can always
recover its domain $\hat{\Psi}$. The idea is that $\sigma$ provides
instantiations for all variables in $\hat{\Psi}$ where
$\mathsf{level}(\hat{\Psi})=n$. All variables at levels greater or equal to
$n$ are treated as global variables and are untouched by the substitution
operation. We note that since contexts are ordered, simultaneous substitutions
are also ordered.

Applying the substitution operation is written in prefix as
$[\sigma/\hat{\Psi}]T$ (see Fig. 3). Note that the closure of a variable with
a substitution is written in postfix (see $x[\sigma]$ and $\alpha[\sigma]$
resp.).

We describe here in detail applying a substitution to a type
$[\sigma/\hat{\Phi}]T$. Due to space, we omit the definition for
$[\sigma/\hat{\Phi}]e$ which applies the substitution $\sigma$ to a term $e$,
composing substitutions, and applying a substitution to a context. They can be
found in the Appendix B.3. In the definition of these substitution operations,
we rely on chopping, merging, and appending simultaneous substitutions,
written $(\sigma/\hat{\Phi})|_{k}$,
${{(\sigma/\hat{\Phi})}\oplus{(\sigma^{\prime}/\hat{\Psi})}}$ and
${{(\sigma/\hat{\Phi})},{(\sigma^{\prime}/\hat{\Psi})}}$. Those operations
correspond to the equivalent context operations and are also defined in the
Appendix B.

$\begin{array}[]{@{}l@{~=~}l@{}}[\sigma/\hat{\Psi}](\alpha[\sigma^{\prime}])\hfil~{}=~{}&\alpha[\sigma^{\prime\prime}]\hfill\alpha\not\in\hat{\Psi}\text{
and }[\sigma/\hat{\Psi}]\sigma^{\prime}=\sigma^{\prime\prime}\\\
[\sigma/\hat{\Psi}](\alpha[\sigma^{\prime}])\hfil~{}=~{}&T^{\prime}\qquad\quad\hfill\textrm{lkp}(\sigma/\hat{\Psi})~{}\alpha=(\hat{\Phi}^{n}.T)~{}\mbox{and}~{}\mathsf{level}(\hat{\Psi})>n\\\
\lx@intercol\hfil\qquad\quad\mbox{and}~{}[\sigma/\hat{\Psi}]\sigma^{\prime}=\sigma^{\prime\prime}~{}\mbox{and}~{}[\sigma^{\prime\prime}/\hat{\Phi}]T=T^{\prime}\lx@intercol\\\
[\sigma/\hat{\Psi}](\alpha[\sigma^{\prime}])\hfil~{}=~{}&\beta[\sigma^{\prime\prime}]\hfill\textrm{lkp}(\sigma/\hat{\Psi})~{}\alpha=\beta^{n}~{}\mbox{and}~{}\mathsf{level}(\hat{\Psi})>n~{}\mbox{and}~{}[\sigma/\hat{\Psi}]\sigma^{\prime}=\sigma^{\prime\prime}\\\
[\sigma/\hat{\Psi}](T\rightarrow S)\hfil~{}=~{}&T^{\prime}\rightarrow
S^{\prime}\hfill[\sigma/\hat{\Psi}]T=T^{\prime}~{}\mbox{and}~{}[\sigma/\hat{\Psi}]S=S^{\prime}\\\
[\sigma/\hat{\Psi}]((\alpha{:}(\Phi\vdash^{n}*))\rightarrow
T)\hfil~{}=~{}&((\alpha{:}(\Phi\vdash^{n}*))\rightarrow
T^{\prime})\hfill\qquad\mbox{level}(\hat{\Psi})>n\text{ and
}[{{(\sigma/\hat{\Psi})}\oplus{(\alpha/\alpha^{n})}}]T=T^{\prime}\\\
[\sigma/\hat{\Psi}]((\alpha{:}(\Phi\vdash^{n}*))\rightarrow
T)\hfil~{}=~{}&((\alpha{:}(\Phi\vdash^{n}*))\rightarrow
T^{\prime})\hfill\mbox{level}(\hat{\Psi})\leq n\text{ and
}[\sigma/\hat{\Psi}]T=T^{\prime}\\\
[\sigma/\hat{\Psi}](\lceil\Phi\vdash^{n}T\rceil)\hfil~{}=~{}&\lceil\Phi^{\prime}\vdash^{n}T^{\prime}\rceil\hfill\begin{array}[t]{@{}r@{}}\mbox{level}(\hat{\Psi})\geq
n\text{ and
}(\sigma/\hat{\Psi})|_{n}=\sigma^{\prime}/\hat{\Psi}^{\prime}\text{ and }\\\
{[\sigma^{\prime}/\hat{\Psi}^{\prime}]\Phi=\Phi^{\prime}}\text{ and
}[{{(\sigma^{\prime}/\hat{\Psi})},{(\mathsf{id}(\hat{\Phi})/\hat{\Phi})}}]T=T^{\prime}\end{array}\\\
[\sigma/\hat{\Psi}](\lceil\Phi\vdash^{n}T\rceil)\hfil~{}=~{}&\lceil\Phi\vdash^{n}T\rceil\hfill\begin{array}[t]{@{}r@{}}\mbox{level}(\hat{\Psi})<n\end{array}\end{array}$
Figure 3. Simultaneous Substitution Operation for Types:
$[\sigma/\hat{\Psi}]T=S$

The substitution operation $[\sigma/\hat{\Psi}]T$ is then mostly
straightforward and applied recursively to $T$. In the variable case
$\alpha[\sigma^{\prime}]$, we distinguish between three cases:

If $\alpha$ is not in $\hat{\Psi}$, then $\alpha$ denotes a “global” variable;
we leave $\alpha$ untouched and only apply $\sigma$ to $\sigma^{\prime}$.

If $\alpha$ is in $\hat{\Psi}$, then we have either a corresponding
instantiation $(\hat{\Phi}^{n}.T)/\alpha^{n}$ or simply $\beta^{n}$ for
$\alpha$ in $\sigma/\hat{\Psi}$ (see Appendix B for the definition of the
lookup operation, $\textrm{lkp}((\sigma/\hat{\Psi}))~{}\alpha$). In both
cases, we apply the simultaneous substitution $\sigma$ to $\sigma^{\prime}$
giving us some substitution $\sigma^{\prime\prime}$. In the former case (where
$(\hat{\Phi}^{n}.T)/\alpha^{n}$), we now apply the substitution
$\sigma^{\prime\prime}$ to $T$. Applying the substitution will terminate, as
$\sigma^{\prime\prime}$ provides instantiations for variables at lower levels
than $n$. In the latter case (where $\beta^{n}/\alpha^{n}$), we simply pair
$\beta$ with $\sigma^{\prime\prime}$ creating a new closure.

For polymorphically quantified types, we push the substitution inside and
extend the substitution with the identity, if its level $n$ satisfies
$n<\mbox{level}(\hat{\Psi})$. Although we quantify over (contextual) type
variables that have type $(\Phi\vdash^{n}*)$, we do not have to apply the
substitution to $\Phi$ itself, as $\Phi$ is a context containing only type
variable declarations111Generalizing this to contain both type and term
variable declarations is straightforward and follows the similar principle as
in the boxed type case where we apply to $\Phi$ the substitution
$(\sigma/\hat{\Psi})|_{n}$.. For boxed types such as
$\lceil\Phi\vdash^{n}T\rceil$, we push $\sigma$ inside the box, if
$\mathsf{level}(\hat{\Psi})\geq n$. To do this, we first drop all the mappings
for variables below $n$ from the substitution $\sigma$, since those variables
will be replaced by $\Phi$. Then, we apply
$\sigma^{\prime}/\hat{\Psi}^{\prime}$ to $\Phi$ (see Fig. 12 in the Appendix
B). Further, we extend $\sigma^{\prime}$ with the identity mapping for
variables in $\Phi$ before applying it to $T$. If
$\mathsf{level}(\hat{\Psi})\leq n$, then we do not apply the substitution to
$\Phi$ or $T$, since it concerns variables that will be replaced by $\Phi$ and
those variables are locally bound.

###### Theorem 3.1 (Termination).

The substitution operation $[\sigma/\hat{\Phi}]T$, $[\sigma/\hat{\Phi}]e$, and
$[\sigma/\hat{\Phi}]\sigma^{\prime}$ terminates.

###### Proof.

By induction on the $\mathsf{level}(\hat{\Phi})$ and structure of $T$ and $e$
and $\sigma^{\prime}$. Either $\mathsf{level}(\hat{\Phi})$ stays the same and
$T$ (resp. $e$ or $\sigma$) is decreasing or $\mathsf{level}(\hat{\Phi})$ is
decreasing. ∎

###  3.4. Typing Rules

With the context and substitution operations in place, we can now define the
typing rules for the multi-level contextual modal lambda-calculus in an
elegant way. The levels provide us with enough structure to keep track of the
scope of variables, terms and types.

To distinguish the notation for contextual types, written as
$\lceil\Psi\vdash^{n}T\rceil$ from the typing judgment, we use
$\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}$ for all the typing judgments.

We begin with defining well-formed contexts. A context
$\Gamma,x{:}(\Phi\vdash^{n}T)$ is well-formed, if $\Gamma$ is well-formed,
$\Phi$ is well-formed with respect to $\Gamma|_{n}$, and $T$ is well-kinded in
the context $({{\Gamma|_{n}},{\Phi}})$.

$\begin{array}[]{c}\lx@intercol\mbox{Well-formed contexts:
<EMAIL_ADDRESS>\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma},{x{:}(\Phi\vdash^{n}T)}}\lx@proof@logical@and\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma\mathsf{level}(\Phi)\leq
n\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma|_{n}},{\Phi}}\Gamma|_{n},\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\quad\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma},{\alpha{:}(\Phi\vdash^{n}*)}}\lx@proof@logical@and\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma\mathsf{level}(\Phi)\leq
n\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma|_{n}},{\Phi}}\quad\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\cdot\end{array}$

With the context operations in place, the kinding rules for types are
straightforward.

$\begin{array}[]{c}\raisebox{8.61108pt}{\mbox{Kinding rules for types:
\framebox{$\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T$}}}\quad\qquad\qquad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha[\sigma]\lx@proof@logical@and\Gamma(\alpha)=(\Phi\vdash^{n}*)\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi\\\\[7.5pt]
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S\rightarrow
T\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\quad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\alpha{:}(\Phi\vdash^{n}*))\rightarrow
T\lx@proof@logical@and\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma|_{n},\Phi{{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{n}*)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\quad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\lceil\Phi\vdash^{n}T\rceil\lx@proof@logical@and\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma|_{n},\Phi\Gamma|_{n},\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\end{array}$

Type variables $\alpha[\sigma]$ where $\alpha:(\Phi\vdash^{n}*)$ in $\Gamma$
are well-kinded, if the associated substitution $\sigma$ maps variables from
$\Phi$ to the present context $\Gamma$. Function types, $S\rightarrow T$ are
well-kinded, if both $S$ and $T$ are well-kinded. When we check that
$(\alpha{:}(\Phi\vdash^{n}*))\rightarrow T$ is well-kinded in a context
$\Gamma$, we ensure that $\Phi$ is well-formed with respect to $\Gamma|_{n}$,
as the local context $\Phi$ will replace all the variables at levels below $n$
in the original $\Gamma$; this is accomplished by
$\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma|_{n},\Phi$. We then check that
$T$ is well-formed, in the context $\Gamma$ extended with the assumption
$\alpha{:}(\Phi\vdash^{n}*)$ where the assumption is inserted at the
appropriate position in $\Gamma$. For the kinding of
$\lceil\Phi\vdash^{n}T\rceil$, we proceed similarly. We again replace all the
variables at levels below $n$ in the original $\Gamma$ with $\Phi$ using the
previously defined context operations.

Using the context operations for restricting and extending contexts, the
typing rules for expressions (Fig. 4) are mostly straightforward and follow
the general principle that we have seen before. To show that a function
$\mathsf{fn}\;x\rightarrow e$ has type $S\rightarrow T$, we extend the context
$\Gamma$ with the declaration $x{:}(\cdot\vdash^{0}S)$ and check that the body
$e$ has type $T$. As we remarked before, no typing context with assumptions
below level $0$ exists, and this declaration can be viewed as $x{:}T$.
However, giving it level $0$ allows for a uniform treatment. To show that a
type abstraction, $\mathsf{Fn}\;\alpha^{n}\rightarrow e$, has the appropriate
type, we extend the context with type variable declaration for $\alpha$.

Applications, $e_{1}~{}e_{2}$ are defined as expected. For type applications,
$e\;(\hat{\Phi}^{n}.T)$, we need to be a bit more careful: in addition to
verifying that $e$ has type $(\alpha{:}(\Phi\vdash^{n}*))\rightarrow S$, we
again verify that $T$ is well-kinded in a new context, where we replace the
assumptions at level below $n$ in $\Gamma$ with the declarations from $\Phi$.
To accomplish this, we again rely on our context operations, first restricting
$\Gamma$ and then appending $\Phi$. As the type of $e$ will be polymorphic,
namely $(\alpha{:}(\Phi\vdash^{n}*))\rightarrow S$, we return as the type of
$e\;(\hat{\Phi}^{n}.T)$ the type $S$ where we have replaced $\alpha$ with
$(\hat{\Phi}^{n}.T)$.

The rules for $\mathsf{box}$ and $\mathsf{letbox}$ again appropriately
restrict and extend $\Gamma$ based on the level where $n>0$. This side
condition simply allows us to distinguish between code, i.e. terms that are
boxed and represent syntax, and programs, i.e. terms that will be evaluated
and run.

$\begin{array}[]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}x[\sigma]:[\sigma/\hat{\Phi}]T\lx@proof@logical@and\Gamma(x)=(\Phi\vdash^{n}T)\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi\quad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{fn}\;x\rightarrow
e:S\rightarrow
T\Gamma,x{:}(\cdot\vdash^{0}S)\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T\qquad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{1}\;e_{2}:T\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{1}:S\rightarrow
T\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{2}:S\\\\[7.5pt]
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{Fn}\;\alpha^{n}\rightarrow
e:(\alpha{:}(\Phi\vdash^{n}*))\rightarrow
T{{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{n}*)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T\qquad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e\;(\hat{\Phi}^{n}.T):[\hat{\Phi}^{n}.T/\alpha^{n}]S\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:(\alpha{:}(\Phi\vdash^{n}*))\rightarrow
S{{\Gamma|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\\\\[7.5pt]
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{box}(\hat{\Phi}^{n}.\,e):\lceil\Phi\vdash^{n}T\rceil{{\Gamma|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T\qquad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{let}\,\mathsf{box}\;(\hat{\Phi}^{n}.u)\;{=}\;e_{1}\;\mathsf{in}\;e_{2}:T\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{1}:\lceil\Phi\vdash^{n}S\rceil{{\Gamma}\oplus{u{:}(\Phi\vdash^{n}S)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{2}:T\end{array}$
Figure 4. Typing rules for expressions
$\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T$

A substitution $(\sigma,\hat{\Psi}^{n}.e)$ provides a mapping from
$(\Gamma^{\prime},x{:}(\Psi\vdash^{n}T))$ to the context $\Gamma$, if $\sigma$
maps variables from $\Gamma^{\prime}$ to $\Gamma$ and if $e$ is well-typed. As
the type $(\Psi\vdash^{n}T)$ is well-formed with respect to $\Gamma^{\prime}$,
we will need to transport both $\Psi$ and $T$ to $\Gamma$. Since $\Psi$
depends only on $\Gamma^{\prime}|_{n}$, we only need to apply the restricted
substitution
$(\sigma/\hat{\Gamma}^{\prime})|_{n}=(\sigma^{\prime\prime}/\hat{\Gamma}^{\prime\prime})$
to $\Psi$. Since we work with simultaneous substitution, we need to extend
this restricted substitution with the identity mapping for $\Psi$, before we
can apply it to the type $T$ and effectively move the type to the new context
$(\Gamma|_{n},[\sigma^{\prime\prime}/\hat{\Gamma}^{\prime\prime}]\Psi)$ in
which $e$ will be well-typed. The cases where we extend a substitution with a
variable (i.e. $\sigma;x^{n}$) is a special case of the previous cases. The
extension of a substitution with a type $(\hat{\Psi}^{n}.T)$ or a type
variable $\alpha^{n}$ follows the similar idea and are a special case of
handling the term extension. We omit them here due to space, but their
definition is given in the Appendix C.

$\begin{array}[]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\cdot:\cdot\quad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\sigma,\hat{\Psi}^{n}.e)~{}:~{}(\Gamma^{\prime},x{:}(\Psi\vdash^{n}T))\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma^{\prime}(\sigma/\hat{\Gamma}^{\prime})|_{n}=(\sigma^{\prime}/\hat{\Gamma}^{\prime\prime}){{\Gamma|_{n}},{[\sigma^{\prime}/\hat{\Gamma}^{\prime\prime}]\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:[{{(\sigma^{\prime}/\hat{\Gamma}^{\prime\prime})},{(\mathsf{id}(\hat{\Psi})/\hat{\Psi})}}]T\\\\[7.5pt]
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\sigma;x)~{}:~{}(\Gamma^{\prime},x{:}(\Psi\vdash^{n}T))\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma^{\prime}(\sigma/\hat{\Gamma}^{\prime})|_{n}=(\sigma^{\prime\prime}/\hat{\Gamma}^{\prime\prime})\Gamma(x)=([\sigma^{\prime\prime}/\hat{\Gamma}^{\prime\prime}]\Psi\vdash^{n}[\sigma^{\prime\prime}/\hat{\Gamma}^{\prime\prime}]T)\\\\[7.5pt]
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\sigma,\hat{\Psi}^{n}.T)~{}:~{}(\Gamma^{\prime},\alpha{:}(\Psi\vdash^{n}*))\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma^{\prime}(\sigma/\hat{\Gamma}^{\prime})|_{n}=(\sigma^{\prime}/\hat{\Gamma}^{\prime\prime}){{\Gamma|_{n}},{[\sigma^{\prime}/\hat{\Gamma}^{\prime\prime}]\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\\\\[7.5pt]
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\sigma;\alpha)~{}:~{}(\Gamma^{\prime},\alpha{:}(\Psi\vdash^{n}*))\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma^{\prime}(\sigma/\hat{\Gamma}^{\prime})|_{n}=(\sigma^{\prime\prime}/\hat{\Gamma}^{\prime\prime})\Gamma(\alpha)=([\sigma^{\prime\prime}/\hat{\Gamma}^{\prime\prime}]\Psi\vdash^{n}*)\end{array}$
Figure 5. Typing rules for substitutions
$\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi$

###  3.5. Substitution properties

We now establish substitution properties. Recall that a context
$\Psi^{k}=\Psi(k-1),\Psi(k-2),\ldots,\Psi(1),\Psi(0)$ where $\Psi(j)$ is the
subcontext of $\Psi^{k}$ with only assumptions of level $j$. For easier
readability, we will simply write
${{{{\Gamma_{1}},{\alpha{:}(\Phi\vdash^{n})}}},{\Gamma_{0}}}$ for a context
where all assumptions in $\Gamma_{1}$ are at level $n$ or above and all
assumptions in $\Gamma_{0}$ are at level $n$ or below.

We first state that the generation of identity substitutions yields well-typed
substitutions.

###### Lemma 3.2 (Identity Substitution).

${{\Gamma},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{id}(\hat{\Phi}):\Phi$

###### Proof.

Induction on $\Phi$. ∎

Next, we generalize a property that already exists in Nanevski et al. [2008]
and Pientka [2003]. In this previous work, it states that the substitution for
locally bound variables and the substitution operation for meta-variables
commute. Here we state more generally that substitution for a variable with
level $m$ and substitution for a variable with level $n$ commute, as long as
$m$ is greater or equal to $n$.

###### Lemma 3.3 (Commuting Substitutions).

  1. (1)

If $m\geq n$, then
$[(\hat{\Psi}^{m}.S_{2})/\beta^{m}][(\hat{\Phi}^{n}.S_{1})/\alpha^{n}]T=[(\hat{\Phi}^{n}.[(\hat{\Psi}^{m}.S_{2})/\beta^{m}]S_{1})/\alpha^{n}][(\hat{\Psi}^{m}.S_{2})/\beta^{m}]T$.

  2. (2)

If $m\geq n$, then
$[(\hat{\Psi}^{m}.e_{2})/y^{m}][(\hat{\Phi}^{n}.e_{1})/x^{n}]e_{0}=[(\hat{\Phi}^{n}.[(\hat{\Psi}^{m}.e_{2})/y^{m}]e_{1})/x^{n}][(\hat{\Psi}^{m}.e_{2})/y^{m}]e_{0}$.

###### Proof.

By induction on $T$ and $e_{0}$. ∎

Last, we state the substitution properties for type variables, term variables
and simultaneous substitutions. Since the single substitution operation relies
on simultaneous substitution, we prove them all mutually. However, for
clarity, we state them separately.

###### Lemma 3.4 (Type Substitution Lemma).

Assuming
$\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{{{\Gamma_{1}},{\alpha{:}(\Phi\vdash^{n}*)}}},{\Gamma_{0}}}$
and ${{\Gamma_{1}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T$.

  1. (1)

Then
$\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma_{1}},{[(\hat{\Phi}^{n}.T)/\alpha^{n}]\Gamma_{0}}}$.

  2. (2)

If
${{{{\Gamma_{1}},{\alpha{:}(\Phi\vdash^{n}*)}}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S$
then
${{\Gamma_{1}},{[(\hat{\Phi}^{n}.T)/\alpha^{n}]\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\hat{\Phi}^{n}.T)/\alpha^{n}]S$.

  3. (3)

If
${{{{\Gamma_{1}},{\alpha{:}(\Phi\vdash^{n}*)}}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{2}:S$
then
${{\Gamma_{1}},{[(\hat{\Phi}^{n}.T)/\alpha^{n}]\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\hat{\Phi}^{n}.T)/\alpha^{n}]e_{2}:[(\hat{\Phi}^{n}.T)/\alpha^{n}]S$.

  4. (4)

If
${{{{\Gamma_{1}},{\alpha{:}(\Phi\vdash^{n}*)}}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Psi$
then
${{\Gamma_{1}},{[(\hat{\Phi}^{n}.T)/\alpha^{n}]\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\hat{\Phi}^{n}.T)/\alpha^{n}]\sigma:[(\hat{\Phi}^{n}.T)/\alpha^{n}]\Psi$.

###### Lemma 3.5 (Term Substitution Lemma).

Assuming
$~{}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{{{\Gamma_{1}},{u{:}(\Phi\vdash^{n}T)}}},{\Gamma_{0}}}$
and ${{\Gamma_{1}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T$.

  1. (1)

If
${{{{\Gamma_{1}},{u{:}(\Phi\vdash^{n}T)}}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{2}:S$
then
${{\Gamma_{1}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\hat{\Phi}^{n}.e)/u]e_{2}:S$.

  2. (2)

If
${{{{\Gamma_{1}},{u{:}(\Phi\vdash^{n}T)}}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Psi$
then
${{\Gamma_{1}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\hat{\Phi}^{n}.e)/u]\sigma:\Psi$.

###### Lemma 3.6 (Simultaneous Substitution Lemma).

Assuming
${{\Gamma_{1}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma_{0}$.

  1. (1)

If
$~{}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{{{\Gamma_{1}},{\Gamma_{0}}}},{\Psi}}$
then
$\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{{{\Gamma_{1}},{\Phi}}},{([\sigma/\hat{\Gamma}_{0}]\Psi)}}$.

  2. (2)

If ${{\Gamma_{1}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S$ then
${{\Gamma_{1}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma/\hat{\Gamma}_{0}]S$.

  3. (3)

If ${{\Gamma_{1}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:S$
then
${{\Gamma_{1}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma/\hat{\Gamma}_{0}]e:[\sigma/\hat{\Gamma}_{0}]S$.

  4. (4)

If
${{\Gamma_{1}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma_{2}:\Psi$
then
${{\Gamma_{1}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma/\hat{\Gamma}_{0}]\sigma_{2}:[\sigma/\hat{\Gamma}_{0}]\Psi$.

###### Proof.

By induction on the first derivation. For more details, see Appendix D. ∎

###  3.6. Local Soundness and completeness

With the substitution properties in place, we establish local soundness and
completeness properties of our calculus. Local soundness guarantees that our
typing rules are not too strong, i.e. they do not allow us to infer more than
we should. Dually, local completeness guarantees that the rules are
sufficiently strong.

The local soundness property also gives natural rise to reduction rules in our
operational semantics and can be viewed as showing that types are preserved
during reduction.

#### Function type

For local soundness, we refer to the term substitution lemma 3.5 to obtain
$\mathcal{D^{\prime}}$.

_Local Soundness_ :

$\begin{array}[b]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\mathsf{fn}\;x\rightarrow
e)~{}e^{\prime}:T\rightarrow
S\lx@proof@logical@and\begin{array}[b]{c}\mathcal{D}\\\
\Gamma,x{:}(\cdot\vdash^{0}T)\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e\end{array}\begin{array}[b]{c}\mathcal{E}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e^{\prime}:T\end{array}\end{array}\Longrightarrow\begin{array}[b]{c}\mathcal{D^{\prime}}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\cdot.e^{\prime})/x^{0}]e:S\end{array}$

Local completeness derivation follows directly from the given typing rules.

_Local Completeness_ :

$\begin{array}[b]{c}\mathcal{D}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T\rightarrow
S\end{array}\Longrightarrow\begin{array}[b]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{fn}\;x\rightarrow
e~{}x[\cdot]:T\rightarrow
S\Gamma,x{:}(\cdot\vdash^{0}T)\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e~{}x[\cdot]:S\lx@proof@logical@and\begin{array}[b]{c}{\mathcal{D}}\\\
{\Gamma,x{:}(\cdot\vdash^{0}T)\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T\rightarrow
S}\end{array}\begin{array}[b]{c}\Gamma,x{:}(\cdot\vdash^{0}T)\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}x[\cdot]:T{\Gamma,x{:}(\cdot\vdash^{0}T)\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\cdot:\cdot}\end{array}\end{array}$

#### Polymorphic type

The local soundness and completeness property for the polymorphic type are
similar.

_Local Soundness_ :

$\begin{array}[b]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\mathsf{Fn}\;\alpha^{n}\rightarrow
e)~{}(\hat{\Phi}^{n}.T):[\hat{\Phi}^{n}.T/\alpha^{n}]S\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{Fn}\;\alpha^{n}\rightarrow
e:(\alpha{:}(\Phi\vdash^{n}*))\rightarrow S\begin{array}[b]{c}\mathcal{D}\\\
{{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{n}*)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:S\end{array}\begin{array}[b]{c}\mathcal{E}\\\
{{\Gamma|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\end{array}\end{array}\Longrightarrow\begin{array}[b]{c}\mathcal{D^{\prime}}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\hat{\Phi}^{n}.T)/\alpha^{n}]e:[\hat{\Phi}^{n}.T/\alpha^{n}]S\end{array}$

We note that ${{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{n}*)}}$ results in an
ordered context of the form $\Gamma_{1},\alpha{:}(\Phi\vdash^{n}*),\Gamma_{0}$
where all declarations in $\Gamma_{1}$ are at level $n$ or above and all
declarations in $\Gamma_{0}$ are below $n$. The derivation
$\mathcal{D^{\prime}}$ is then obtained using the type substitution lemma 3.4.

Local Completeness:

$\begin{array}[b]{c}\mathcal{D}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:(\alpha{:}(\Phi\vdash^{n}*))\rightarrow
S\end{array}\Longrightarrow\begin{array}[b]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{Fn}\;\alpha^{n}\rightarrow
e~{}(\hat{\Phi}^{n}.\alpha[\mathsf{id}(\hat{\Phi})]):(\alpha{:}(\Phi\vdash^{n}*))\rightarrow
S{{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{n}*)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e~{}(\hat{\Phi}^{n}.\alpha[\mathsf{id}(\hat{\Phi})]):S\lx@proof@logical@and\begin{array}[b]{@{}c}{\mathcal{D}}\\\
{{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{n}*)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:(\alpha{:}(\Phi\vdash^{n}*))\rightarrow
S\end{array}\begin{array}[b]{c@{}}{{\Gamma|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha[\mathsf{id}(\hat{\Phi})]{{\Gamma|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{id}(\hat{\Phi}):\Phi\end{array}\end{array}$

We use the identity substitution lemma 3.2 to justify the derivation
${{\Gamma|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha[\mathsf{id}(\hat{\Phi})]$
and exploit the fact that
$[(\hat{\Phi}^{n}.\alpha[\mathsf{id}(\hat{\Phi})])/\alpha^{n}]S=S$.

#### Multi-level contextual type

Local soundness and completeness follows similar ideas. For local soundness,
we note that ${{\Gamma}\oplus{u{:}(\Phi\vdash^{n}T)}}$ results in an ordered
context $\Gamma^{\prime}$ where the declaration $u{:}(\Phi\vdash^{n}T)$ is
inserted at the appropriate level. The derivation $\mathcal{D^{\prime}}$ is
then obtained by referring to the term substitution lemma 3.5 using
$(\hat{\Phi}^{n}.e)$ for $u$, $\mathcal{E}$, and $\mathcal{D}$.

_Local Soundness_ :

$\begin{array}[b]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{let}\,\mathsf{box}\;(\hat{\Phi}^{n}.u)\;{=}\;\mathsf{box}(\hat{\Phi}^{n}.\,e)\;\mathsf{in}\;e_{2}:S\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{box}(\hat{\Phi}^{n}.\,e):\lceil\Phi\vdash^{n}T\rceil\begin{array}[b]{c}\mathcal{E}\\\
{{\Gamma|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T\end{array}\begin{array}[b]{c}\mathcal{D}\\\
{{\Gamma}\oplus{u{:}(\Phi\vdash^{n}T)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{2}:S\end{array}\end{array}\Longrightarrow\begin{array}[b]{c}\mathcal{D^{\prime}}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[(\hat{\Phi}^{n}.e)/u^{n}]e_{2}:S\end{array}$

For local completeness, we again use Lemma 3.2 for identity substitutions to
justify the derivation
${{({{\Gamma}\oplus{{u{:}(\Phi\vdash^{n}T)}}})|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}u[\mathsf{id}(\hat{\Phi})]:T$.

_Local Completeness_ :

$\begin{array}[b]{c}\mathcal{D}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:\lceil\Phi\vdash^{n}T\rceil\end{array}\Longrightarrow\begin{array}[b]{c}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{let}\,\mathsf{box}\;(\hat{\Phi}^{n}.u)\;{=}\;e\;\mathsf{in}\;\mathsf{box}(\hat{\Phi}.\,u[\mathsf{id}(\hat{\Phi})]):\lceil\Phi\vdash^{n}T\rceil\lx@proof@logical@and\begin{array}[b]{c}\mathcal{D}\\\
\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:\lceil\Phi\vdash^{n}T\rceil\end{array}{{\Gamma}\oplus{u{:}(\Phi\vdash^{n}T)}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{box}(\hat{\Phi}.\,u[\mathsf{id}(\hat{\Phi})]):\lceil\Phi\vdash^{n}T\rceil{{({{\Gamma}\oplus{{u{:}(\Phi\vdash^{n}T)}}})|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}u[\mathsf{id}(\hat{\Phi})]:T{{({{\Gamma}\oplus{{u{:}(\Phi\vdash^{n}T)}}})|_{n}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{id}(\hat{\Phi}):\Phi\end{array}$

##  4\. Extension to pattern matching

We now extend the multi-level programming foundation to support pattern
matching on code, i.e. expressions of type $\lceil\Gamma\vdash^{n}T\rceil$.
This generalizes the expressions
$\mathsf{let}\,\mathsf{box}\;(\hat{\Gamma}^{n}.u)\;{=}\;e_{1}\;\mathsf{in}\;e_{2}$
to support not only binding of code to a variable $u$, but also inspecting
this piece of code by pattern matching. In general, one may view the
expression
$\mathsf{let}\,\mathsf{box}\;(\hat{\Gamma}^{n}.u)\;{=}\;e_{1}\;\mathsf{in}\;e_{2}$,
as a match on $e_{1}$ where the pattern consists only of a pattern variable
$u$ and $e_{2}$ is the branch of the case-expressions. We view code patterns
as higher-order abstract syntax trees; this abstraction allows us to choose
any encoding internally in the implementation.

Adding pattern matching on code in a type-safe manner has been a challenge for
two reasons:

#### 1) Representation of Code and Refinement of Types

In general, we want to pattern match on $\lceil\Gamma\vdash^{n}\alpha\rceil$
(where we omit the identity substitution that is associated with the type
variable $\alpha$ for better readability). As a consequence, a pattern may
impose some constraints on $\alpha$. For example, a code pattern
$\mathsf{box}(\hat{\Gamma}.\,\mathsf{fn}\;x\rightarrow p)$ which has type
$\lceil\Gamma\vdash^{n}\beta_{1}\rightarrow\beta_{2}\rceil$ generates the
constraint that $\alpha:=\beta_{1}\rightarrow\beta_{2}$. A similar situation
exists in dependently typed systems. Hence, it is not surprising that
constraints arise.

#### 2) Characterizing pattern variables at different stages.

A key question is what type to assign to pattern variables in code and type
patterns. When we capture a code pattern
$\mathsf{box}(\hat{\Gamma}.\,\mathsf{fn}\;x\rightarrow p)$, it seems natural
that we assign $p$ the type $\beta_{2}$ in the context $\Gamma$ extended with
the declaration for $x$ of type $\beta_{1}$. This follows, for example, the
approach taken in the proof environment Beluga[Pientka 2008; Pientka and
Dunfield 2010; Pientka and Cave 2015] where the pattern variable $p$ depends
on the bound variables from $\hat{\Gamma}$ extended with $x$. However, in our
setting, we want to also allow code patterns of the form
$\mathsf{box}(\hat{\Gamma}.\,\mathsf{let}\,\mathsf{box}\;(\hat{\Phi}^{k}.u)\;{=}\;p\;\mathsf{in}\;q)$.
As a consequence, we need to capture the type of $q$, which may depend not
only on the variables from $\hat{\Gamma}$, but also on the variable $u$. Or we
might want to allow code patterns that themselves contain code! For example,
$\mathsf{box}(\hat{\Gamma}.\,\mathsf{box}(\hat{\Phi}.\,p))$. This is where our
multi-level context approach pays off. Since we associate every variable with
a level, we simply view $q$ in the extended context with the variable $u$
where $u$ has been inserted at the appropriate position. Similarly, in the
code pattern
$\mathsf{box}(\hat{\Gamma}^{k}.\,\mathsf{box}(\hat{\Phi}^{n}.\,p))$, the
levels associated with $\hat{\Gamma}$ and $\hat{\Phi}$ give us the structure
to determine in which context $p$ is making sense.

These two considerations lead us to generalize our term language and our
contexts. In particular, we track and reason about two kinds of constraints:
the first one $\alpha:=(\Psi\vdash^{n}T)$ refines a type declaration
$\alpha:(\Psi\vdash^{*})$ and the second one $\\#$ denotes an inconsistent set
of constraints. The latter allows for elegant handling of impossible cases
that may arise. We note that these constraints arise only during typing, and
programmers will write only pure contexts, i.e. contexts without any
constraints.

$\begin{array}[]{llcl}\mbox{Terms}&e,p,q&\mathrel{::=}&\ldots\mathrel{\mid}\mathsf{case}_{\lceil\Phi\vdash^{k}T\rceil}\
{e}\
\mathsf{of}~{}\overrightarrow{(\Psi_{i}.(\hat{\Phi}_{i}.p_{i}):(\Phi_{i}\vdash^{k}T_{i})\rightarrow
e_{i})}\\\
\mbox{Context}&\Gamma,\Psi,\Phi&\mathrel{::=}&\ldots\mathrel{\mid}\Gamma,\alpha:=(\hat{\Psi}^{n}.T):(\Psi\vdash^{n}*)\mathrel{\mid}\Gamma,\\#\end{array}$

For simplicity and clarity, we define pattern matching and branches in a case-
expression in such a way that all pattern variables are explicitly listed as
part of the branch in the context $\Psi_{i}$. The context $\Phi_{i}$ contains
all the locally bound variables that may be used in the pattern $p_{i}$. We
concentrate here on patterns that are terms, but not case-expressions
themselves to explain the main ideas. In practice, we would infer the type
associated with those pattern variables. We note that for all variables
$x{:}(\\_\vdash^{n}\\_)$ in $\Psi_{i}$, we have that
$n>\mathsf{level}(\Phi_{i})$, since pattern variables abstract over
holes/variables in a code pattern. Further, these pattern variables themselves
may depend on the context $\Phi_{i}$ where all variables in $\Phi_{i}$ denote
bound variables within the code pattern and hence are variables defined at
levels higher than $n+1$. We also add a type annotation
$(\Phi_{i}\vdash^{k}T_{i})$ to each pattern which states that the pattern
$p_{i}$ has type $T_{i}$ in the context ${{\Psi_{i}},{\Phi_{i}}}$.

Last but not least, we add a type annotation to the case-expression itself. It
describes the type of the scrutinee $e$. This is used during run-time where we
first find the compatible branch by matching the type of the scrutinee against
one of type annotations in branches and subsequently match the scrutinee
against the pattern in the selected branch. Before giving a more detailed
explanation of the static and dynamic semantics for case-expressions and
turning our previous kinding and typing rules from Sec. 3.4 into shallow
pattern rules (see Sec. 4.4), we consider the generation and handling of type
constraints next.

###  4.1. Typing modulo

To handle constraints during type checking, we extend our definition of well-
formed contexts s.t. $\Gamma,\alpha:=(\Psi\vdash^{n}T)$ is a well-formed
context if $\Gamma$ is well-formed, and the type $T$ is well-formed in
${{\Gamma|_{n}},{\Psi}}$. We also must ensure that there are no circularities
in $\Gamma$. A context $\Gamma,\\#$ which contains a contradiction marked by
$\\#$ is well-formed, if $\Gamma$ is.

$\begin{array}[]{c}\lx@intercol\text{Additional rules for context well-
<EMAIL_ADDRESS>\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma,\alpha:=(\hat{\Psi}^{n}.T):(\Psi\vdash^{n}*)\lx@proof@logical@and\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}({{\Gamma|_{n}},{\Psi}})({{\Gamma|_{n}},{\Psi}})\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\quad\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma,\\#\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma\end{array}$

We also revisit the typing rules for substitutions. To ensure that
$\sigma,~{}(\hat{\Psi}^{k}.T)$ is a well-typed substitution for a context
$\Phi,\alpha{:=}(\hat{\Psi}^{k}.S):(\Psi\vdash^{k}*)$, we check in addition to
the fact that $\sigma$ and $T$ are well-typed, that $T$ and $S$ are equal in
the range of the substitution. We also note that, if the domain of a
substitution contains a contradiction, then the range must also contain a
contradiction.

$\begin{array}[]{c}\lx@intercol\text{Additional rules for well-typed
<EMAIL_ADDRESS>\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma,~{}(\hat{\Psi}^{k}.T):\Phi,\alpha{:=}(\hat{\Psi}^{k}.S):(\Psi\vdash^{k}*)\lx@proof@logical@and\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi~{}~{}\quad{{\Gamma|_{k}},{\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=[{{((\sigma/\hat{\Phi})|_{k})},{(\mathsf{id}(\hat{\Psi})/\hat{\Psi})}}]S~{}~{}\quad{{\Gamma|_{k}},{\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\quad\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi,\\#\lx@proof@logical@and\\#\in\Gamma\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi\end{array}$

Last, we add a type conversion rule that lets us prove that two types are
equal modulo the constraints in $\Psi$.

$\begin{array}[]{c}\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T\lx@proof@logical@and\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:S\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S=T\end{array}$

###  4.2. Type equality modulo constraints

Since we accumulate equality constraints in our context $\Psi$ during type
checking, declarative equality is not purely structural – it can also exploit
the equality constraints. Structural equality on types modulo constraints is
defined using the judgment: $\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S$.

Most structural equality rules are as expected, and we omit them for brevity.
To, for example, compare two function types for equality, we simply compare
their components. For polymorphic types, we similarly compare their components
and make sure to extend the context with the declaration for $\alpha$ when
comparing the result types. If $\Psi$ contains a contradiction, then we simply
succeed. The only interesting case is : $\alpha[\sigma]=T$ where
$\alpha{:=}(\hat{\Phi}^{n}.S):(\Phi\vdash^{n}*)\in\Psi$. In this case, we
continue to compare $T$ with $[\sigma/\hat{\Phi}]S$. The complete set of
structural equality rules can be found in the Appendix Ethe long version.

###  4.3. Typing Rule for Case-Expressions

We now discuss the typing rule for case-expressions which is the centrepiece
of supporting typed code analysis.

$\begin{array}[]{c}\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{case}_{\lceil\Phi\vdash^{k}T\rceil}\
{e}\
\mathsf{of}~{}{\overrightarrow{(\Psi_{i}.(\hat{\Phi}_{i}.p_{i}):(\Phi_{i}\vdash^{k}T_{i})\rightarrow
e_{i})}}:S\begin{array}[]{l}\qquad\quad\quad\\!\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:\lceil\Phi\vdash^{k}T\rceil\qquad\qquad\quad\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\lceil\Phi\vdash^{k}T\rceil\\\\[5.0pt]
\mbox{For all
$i$}~{}\left\\{\begin{array}[]{l}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}({{\Psi_{i}},{\Phi_{i}}})\qquad\qquad\Psi_{i};(\Phi_{i})^{k}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T_{i}\qquad\quad\Psi_{i};(\Phi_{i})^{k}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}p_{i}:T_{i}\\\
\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}({{\Psi_{i}}\oplus{\Psi|_{k}}})\qquad({{\Psi_{i}}\oplus{\Psi|_{k}}})\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\Phi\vdash^{k}T)=(\Phi_{i}\vdash^{k}T_{i})\searrow\Gamma_{i}\qquad{{\Gamma_{i}},{\Psi|^{k}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{i}:S\end{array}\right.\end{array}\end{array}$

We first check that the guard $e$ has type $\lceil\Phi\vdash^{k}T\rceil$ and
that the given type annotation is a well-kinded type. For each branch, we then
check the following conditions:

  1. (1)

The type annotation in the pattern is well-kinded. This entails verifying that
the context ${{\Psi_{i}},{\Phi_{i}}}$ is well-formed and that the type $T_{i}$
is well-kinded. Recall that ${{\Psi_{i}},{\Phi_{i}}}$ is only defined, when
all declarations in $\Psi_{i}$ are at higher levels than $k$, i.e. the level
of $\Phi_{i}$.

  2. (2)

The pattern $p_{i}$ has type $T_{i}$ in the context ${{\Psi_{i}},{\Phi_{i}}}$.
In fact, we ensure something stronger, namely that $\Psi_{i}$ contains the
pattern variables and the code pattern $\mathsf{box}(\hat{\Phi}_{i}.\,p_{i})$
has type $\lceil\Phi_{i}\vdash^{k}T_{i}\rceil$. This is accomplished by the
judgment $\Psi_{i};\Phi_{i}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}p_{i}:T_{i}$
(see Sec. 4.4).

  3. (3)

We match the type of the pattern, $(\Phi_{i}\vdash^{k}T_{i})$ against the type
of the scrutinee $(\Phi\vdash^{k}T)$ using the judgment

$({{\Psi_{i}}\oplus{\Psi|_{k}}})\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\Phi\vdash^{k}T)=(\Phi_{i}\vdash^{k}T_{i})\searrow\Gamma_{i}$

This generates a new context $\Gamma_{i}$ which constrains some type variables
in $\Psi|_{k}$. Recall that all variables in $\Psi$ which are below $k$ will
be replaced by $\Phi_{i}$, and hence only the declarations in $\Psi|_{k}$
matter. Further, ${{\Psi_{i}}\oplus{\Psi|_{k}}}$ only contains variable
declarations at levels above $k$ and therefore also $\Gamma_{i}$ contains only
variables above $k$.

Last, we ensure that the resulting context $\Gamma_{i}$ is well-formed, by
starting with the joint context $({{\Psi_{i}}\oplus{\Psi|_{k}}})$. The order
will in fact ensure that type variables in $\Psi|_{k}$ (the type of the
scrutinee) can be constrained by variables in $\Psi_{i}$ (the type of the
pattern). We describe matching and the generation of constraints in Sec. 4.5.

  4. (4)

Finally, we check that the body $e_{i}$ of the branch has type $S$ in the
constrained context $\Gamma_{i}$ extended with the $\Psi|^{k}$ where we remove
all assumptions that are at level $k$ or higher. Note that all removed
assumptions are in fact present in $\Gamma_{i}$ and have possibly been refined
in the previous step.

We now describe pattern typing and constraint generation.

###  4.4. Pattern Typing

Pattern kinding and typing rules are derived from kinding and typing rules for
types and terms in Sec. 3.4. They are a special case of those rules. In all
the pattern typing judgments, we separate the pattern variables $\Psi$ from
the bound variables $\Gamma$, writing $\Psi;\Gamma^{n}$ instead of
$\Psi,\Gamma$ where $\mathsf{level}(\Gamma)=n$ and for every declaration
$x{:}(\\_\vdash^{j}\\_)$ in $\Psi$, we have $j>n$. Although this separation is
not strictly necessary for ensuring that a pattern is well-typed, it is
necessary when we define unification on code and types, since only pattern
variables in $\Psi$ can be instantiated, while bound variables in $\Gamma$
remain fixed. Further, to ensure that unification falls into the decidable
higher-order pattern fragment (see Miller [1991]), pattern variables must be
associated with a variable substitution. For simplicity, we choose here the
identity substitution, which we in fact omit for better readability.

$\begin{array}[]{c}\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha[\sigma]\lx@proof@logical@and\alpha:(\Phi\vdash^{k}*)\in\Gamma\Psi;\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi\quad\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha\alpha:(\Gamma\vdash^{n}*)\in\Psi\\\\[7.5pt]
\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\lceil\Phi\vdash^{k}\beta\rceil\lx@proof@logical@and
k>0\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}({{\Gamma|_{k}},{\Phi}})\beta:(({{\Gamma|_{k}},{\Phi}})\vdash^{\mathsf{max}(n,k)}*)\in\Psi\\\\[7.5pt]
\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\beta\rightarrow\alpha\lx@proof@logical@and\beta:(\Gamma\vdash^{n}*)\in\Psi\alpha:(\Gamma\vdash^{n}*)\in\Psi\quad\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\alpha{:}(\Phi\vdash^{k}*))\rightarrow\beta\lx@proof@logical@and\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Psi},{{{\Gamma|_{k}},{\Phi}}}}\beta:(({{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{k}*)}})\vdash^{\mathsf{max}(n,k)}*)\in\Psi\end{array}$
Figure 6. Type Pattern rules:
$\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T$

We first consider type patterns (see Fig. 6). For type variables, we
distinguish two cases. When the type variable $\alpha$ is in $\Psi$, it must
have type $(\Gamma\vdash^{n}*)$ and describes a pattern type variable. A bound
variable occurrence, $\alpha[\sigma]$, is well-kinded, if $\alpha$ is declared
in $\Gamma$ to have kind $(\Phi\vdash^{k}*)$ and $\sigma$ is a substitution
mapping variables from $\Phi$ to $\Psi;\Gamma$. Pattern kinding for function
types $\beta\rightarrow\alpha$ is straightforward: each pattern variable must
be declared in $\Psi$ with kind $(\Gamma\vdash^{n}*)$. For polymorphic type
patterns, $(\alpha{:}(\Phi\vdash^{k}*))\rightarrow\beta$, we note that $\beta$
is the pattern variable that makes sense in the extended context
$({{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{k}*)}})$. Note that in general, $k$
could be greater than $\mathsf{level}(\Gamma)=n$. Hence, the type variable
$\alpha$ can increase the overall level of the extended context, if $k>n$, and
the extended context has level $\mathsf{max}(n,k)$. Therefore, the pattern
type variable $\beta$ must be declared in $\Psi$ with kind
$(({{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{k}*)}})\vdash^{\mathsf{max}(n,k)}*)$.
Last, we consider the contextual type pattern,
$\lceil\Phi\vdash^{k}\beta\rceil$, where $\beta$ is the pattern type variable.
It is meaningful in the context $({{\Gamma|_{k}},{\Phi}})$. The level of this
resulting context is $\mathsf{max}(n,k)$ depending on whether $n$ is greater
or less than $k$. Hence, it must be declared in $\Psi$ with kind
$(({{\Gamma|_{k}},{\Phi}})\vdash^{\mathsf{max}(n,k)}*)$.

$\begin{array}[]{c}\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}x[\sigma]:[\sigma/\hat{\Phi}]T\lx@proof@logical@and
x:(\Phi\vdash^{k}T)\in\Gamma\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi\quad\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}x:Tx:(\Gamma\vdash^{n}T)\in\Psi\quad\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{fn}\;x\rightarrow
p:S\rightarrow
Tp{:}({{\Gamma},{x{:}(\cdot\vdash^{0}S)}}\vdash^{n}T)\in\Psi\\\\[7.5pt]
\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}p\;q:T\lx@proof@logical@and
p{:}(\Gamma\vdash^{n}S\rightarrow T)\in\Psi
q{:}(\Gamma\vdash^{n}S)\in\Psi\qquad\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{Fn}\;\alpha^{k}\rightarrow
p:(\alpha{:}(\Phi\vdash^{k}*))\rightarrow
Tp{:}({{\Gamma}\oplus{\alpha{:}(\Phi\vdash^{k}*)}}\vdash^{\mathsf{max}(n,k)}T)\in\Psi\\\\[7.5pt]
\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}p\;(\hat{\Phi}^{k}.\beta):[\hat{\Phi}^{k}.\beta[\mathsf{id}(\hat{\Phi})]/\alpha^{k}]S\lx@proof@logical@and
p:(\Gamma\vdash^{n}(\alpha{:}(\Phi\vdash^{k}*))\rightarrow
S)\in\Psi\beta{:}({{\Gamma|_{k}},{\Phi}}\vdash^{\mathsf{max}(n,k)}*)\in\Psi\\\\[7.5pt]
\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{box}(\hat{\Phi}^{k}.\,p):\lceil\Phi\vdash^{k}T\rceil\lx@proof@logical@and
k>0p{:}({{\Gamma|_{k}},{\Phi}}\vdash^{\mathsf{max}(n,k)}T)\in\Psi\quad\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{let}\,\mathsf{box}\;(\hat{\Phi}^{k}.u)\;{=}\;p\;\mathsf{in}\;q:T\lx@proof@logical@and
p{:}(\Gamma\vdash^{n}\lceil\Phi\vdash^{k}S\rceil)\in\Psi
q{:}({{\Gamma}\oplus{u{:}(\Phi\vdash^{k}S)}}\vdash^{\mathsf{max}(n,k)}T)\in\Psi\end{array}$
Figure 7. Code Pattern Typing
$\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}p:T$

We describe code pattern typing in Fig. 7. A code pattern $p$ is the sub-term
in $\mathsf{box}(\hat{\Gamma}^{n}.\,p)$ which has type
$\lceil\Gamma\vdash^{n}T\rceil$. Our code pattern typing rules follow the
typing rules for terms given earlier, and we assume that
$\lceil\Gamma\vdash^{n}T\rceil$ is a well-formed pattern type. We again
separate the pattern variables (declared in $\Psi$) from the bound variables
(declared in $\Gamma$) (see Fig. 7). A pattern variable $x$ of type $T$ is
implicitly associated with the identity substitution and hence must be
declared in $\Psi$ with the type $(\Gamma\vdash^{n}T)$. A bound variable
occurrence, written as a closure $x[\sigma]$, is well-typed, if $x$ is
declared to have type $(\Phi\vdash^{k}T)$ in $\Gamma$ and $\sigma$ is a
substitution pattern that maps variables from $\Phi$ to $\Psi;\Gamma$. In code
patterns for functions, $\mathsf{fn}\;x\rightarrow p$, of type $S\rightarrow
T$, the pattern variable $p$ is meaningful in the extended context
${{\Gamma},{x{:}(\cdot\vdash^{0}S)}}$. It hence must be declared in $\Psi$
with type $({{\Gamma},{x{:}(\cdot\vdash^{0}S)}}\vdash^{n})T$. Code patterns
for applications, $p~{}q$ are straightforward given that we adapt a
declarative formulation. Polymorphic code patterns,
$\mathsf{Fn}\;\alpha^{k}\rightarrow p$, and type application patterns,
$p\;(\hat{\Phi}^{k}.\beta)$, follow the same principles as in polymorphic type
patterns discussed earlier; similarly, boxed code patterns,
$\mathsf{box}(\hat{\Phi}^{k}.\,p)$, follow the same principles as for
contextual type patterns. In each of these cases, the pattern variable is
declared in the extended context at level $\mathsf{max}(n,k)$. For
$\mathsf{let}\,\mathsf{box}\;(\hat{\Phi}^{k}.u)\;{=}\;p\;\mathsf{in}\;q$, we
follow the typing rules given earlier: $p$ must be declared with type
$(\Gamma\vdash^{n}\lceil\Phi\vdash^{k}S\rceil)$ and $q$ with type
$({{\Gamma}\oplus{u{:}(\Phi\vdash^{k}S)}}\vdash^{\mathsf{max}(n,k)}T)$ in
$\Psi$.

Last, we describe typing rules for substitution patterns (Fig. 8) which follow
the corresponding typing rules for simultaneous substitutions.

$\begin{array}[]{c}\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\cdot:\cdot\quad\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma,(\hat{\Phi}^{k}.p):(\Phi^{\prime},x{:}(\Phi\vdash^{k}T))\lx@proof@logical@and\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi^{\prime}p{:}({{\Gamma|_{k}},{[\sigma/\hat{\Phi}^{\prime}]\Phi}}\vdash^{\mathsf{max}(n,k)}[\sigma/\hat{\Phi}^{\prime},\mathsf{id}(\hat{\Phi})/\hat{\Phi}]T)\in\Psi\\\\[7.5pt]
\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma,(\hat{\Phi}^{k}.\alpha):(\Phi^{\prime},\alpha{:}(\Phi\vdash^{k}*))\lx@proof@logical@and\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi^{\prime}\alpha{:}({{\Gamma|_{k}},{\Phi}}\vdash^{\mathsf{max}(n,k)}*)\in\Psi\end{array}$
Figure 8. Substitution Pattern Typing
$\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi$

Whenever a pattern is well-typed using the pattern kinding and typing rules,
the pattern is also well-typed when viewed as an expression.

###### Lemma 4.1 (Pattern Reflection).

Let $\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Psi},{\Gamma^{n}}}$.

  1. (1)

If $\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T$ then
$\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\lceil\Gamma\vdash^{n}T\rceil$

  2. (2)

If $\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}p:T$ then
$\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{box}(\hat{\Gamma}^{n}.\,p):\lceil\Gamma\vdash^{n}T\rceil$

  3. (3)

If $\Psi;\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi$ then
$\Psi,\Gamma^{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Phi$

###### Proof.

For (3), by induction on the first derivation. For others, by case analysis. ∎

###  4.5. Unification on Types: constraint generation

$\begin{array}[]{@{}c@{}}\mbox{}\hfill\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha=\alpha\searrow\Gamma\alpha{:}(\Phi\vdash^{k}*)\in\Gamma\hfill\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha=T\searrow\Gamma,\\#\lx@proof@logical@and\Gamma=\Gamma_{1},\alpha{:}(\Phi\vdash^{k}*),\Gamma_{0}\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha\in
T\hfill\mbox{}\\\\[7.5pt]
\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha=T\searrow\Gamma^{\prime}\lx@proof@logical@and\Gamma=\Gamma_{1},\alpha{:}(\Phi\vdash^{k}*),\Gamma_{0}{{\Gamma_{1}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha\not\in
T\Gamma^{\prime}=\Gamma_{1},\alpha{:=}(\hat{\Phi}.T):(\Phi\vdash^{k}*),\Gamma_{0}\\\\[7.5pt]
\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha=T\searrow\Gamma^{\prime}\lx@proof@logical@and\Gamma=\Gamma_{1},\alpha{:=}(\hat{\Phi}.T^{\prime}):(\Phi\vdash^{k}*),\Gamma_{0}\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha\not\in
T\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T^{\prime}=T\searrow\Gamma^{\prime}\\\\[7.5pt]
\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\alpha[\sigma]=\alpha[\sigma^{\prime}]\searrow\Gamma^{\prime}\lx@proof@logical@and\alpha{:}(\Psi\vdash^{k}*)\in\Phi\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma=\sigma^{\prime}:\Psi\searrow\Gamma^{\prime}\quad\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\lceil\Psi\vdash^{n}T\rceil=\lceil\Psi^{\prime}\vdash^{n}S\rceil\searrow\Gamma^{\prime\prime}\lx@proof@logical@and\Gamma;\Phi|_{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Psi^{\prime}\searrow\Gamma^{\prime}\Gamma^{\prime};({{\Phi|_{n}},{\Psi}})\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime\prime}\\\\[7.5pt]
\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T_{1}\rightarrow
T_{2}=S_{1}\rightarrow
S_{2}\searrow\Gamma_{0}\lx@proof@logical@and\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T_{1}=S_{1}\searrow\Gamma_{1}\Gamma_{1};\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T_{2}=S_{2}\searrow\Gamma_{0}\quad\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\alpha{:}(\Psi\vdash^{n}*))\rightarrow
T=(\alpha{:}(\Psi^{\prime}\vdash^{n}*))\rightarrow
S\searrow\Gamma^{\prime}\lx@proof@logical@and\Gamma;\Phi|_{n}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Psi^{\prime}\Gamma;{{\Phi}\oplus{(\alpha{:}(\Psi\vdash^{n}*))}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}\\\\[7.5pt]
\end{array}$ Figure 9. Type
Unification:$\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}$

We define the refinement of types using unification via the judgment

$\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\Phi\vdash^{k}T)=(\Phi_{i}\vdash^{k}T_{i})\searrow\Gamma$

Without loss of generality, we assume that $\Psi$ is a context that contains
variables at levels higher than $k$. In particular, it contains the pattern
variables.

$\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\Phi\vdash^{k}T)=(\Phi_{i}\vdash^{k}T_{i})\searrow\Gamma_{2}\lx@proof@logical@and\Gamma;\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Phi=\Phi_{i}\searrow\Gamma_{1}\Gamma_{1};\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=T_{i}\searrow\Gamma_{2}$

To unify a contextual type $(\Phi\vdash^{k}T)$ against
$(\Phi_{i}\vdash^{k}T_{i})$, we first unify $\Phi$ against $\Phi_{i}$ and
subsequently unify $T$ against $T_{i}$ given the (bound) variable context
$\Phi$. To separate between the bound variables $\Phi$ that are fixed and
bound and pattern variables $\Gamma$ that can be refined and instantiated, we
again use the symbol ; and write $\Gamma;\Phi$. Context and type unification
are then defined in Fig. 9 and Fig. 10 using the judgments
$\Gamma;\Phi^{k}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}$
and
$\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Phi\searrow\Gamma^{\prime}$.

We only unify well-kinded types $T$ and $S$; in particular, if $T$ and $S$ are
well-typed in ${{\Gamma},{\Phi^{k}}}$, then they remain well-typed in
${{\Gamma^{\prime}},{\Phi^{k}}}$ where $\Gamma^{\prime}$ is a refinement of
$\Gamma$, i.e. some type variable declarations that occur in $T$ and in $S$
are constrained s.t.
${{\Gamma^{\prime}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S$.

$\begin{array}[]{c}\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\cdot=\cdot\searrow\Gamma\quad\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\Psi,\alpha{:}(\Psi^{\prime}\vdash^{n}*))=(\Phi,\beta{:}(\Phi^{\prime}\vdash^{n}*))\searrow\Gamma^{\prime\prime}\lx@proof@logical@and\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Phi\searrow\Gamma^{\prime}\Gamma^{\prime};{{\Gamma_{0}},{\Psi|_{n}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi^{\prime}=\Phi^{\prime}\searrow\Gamma^{\prime\prime}\\\\[7.5pt]
\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}(\Psi,x{:}(\Psi^{\prime}\vdash^{n}T^{\prime}))=(\Phi,y{:}(\Phi^{\prime}\vdash^{n}S^{\prime}))\searrow\Gamma^{\prime\prime\prime}\lx@proof@logical@and\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Phi\searrow\Gamma^{\prime}\Gamma^{\prime};{{\Gamma_{0}},{\Psi|_{n}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi^{\prime}=\Phi^{\prime}\searrow\Gamma^{\prime\prime}\Gamma^{\prime\prime};{{\Gamma_{0}},{{{\Psi|_{n}},{\Psi^{\prime}}}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T^{\prime}=S^{\prime}\searrow\Gamma^{\prime\prime\prime}\\\\[7.5pt]
\mbox{[All other cases yield $\Gamma,\\#$]}\end{array}$
Figure 10. Context Unification:
$\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Phi\searrow\Gamma^{\prime}$

We write $\Gamma^{\prime}\succeq\Gamma$ to describes context refinement where
a declaration $\alpha{:}(\Phi\vdash^{n}*)$ in $\Gamma$ has been updated to
$\alpha{:=}(\hat{\Phi}^{n}.T):(\Phi\vdash^{n}*)$ and all variable declarations
present in $\Gamma$ are also present in $\Gamma^{\prime}$.

Unification is defined recursively based on the type $T$ and $S$. In
particular, if $T=T_{1}\rightarrow T_{2}$ and $S=S_{1}\rightarrow S_{2}$, we
first match $T_{1}$ against $S_{1}$ which returns a refined context
$\Gamma_{1}$ and we subsequently match $T_{2}$ against $S_{2}$ yielding a
further refinement $\Gamma_{2}$. We similarly proceed to match
$\lceil\Psi\vdash^{n}T\rceil$ against $\lceil\Psi^{\prime}\vdash^{n}S\rceil$
given the pattern variable context $\Gamma$ and the bound variable context
$\Phi$. Since $\lceil\Psi\vdash^{n}T\rceil$ is well-kinded type pattern in
$\Gamma;\Phi$, we know that $T$ is a well-kinded type pattern in
$\Gamma;{{\Phi|_{n}},{\Psi}}$. We therefore first match $\Psi$ against
$\Psi^{\prime}$ in $\Gamma;\Phi|_{n}$. This returns an updated context
$\Gamma^{\prime}$. Next, we match $T$ against $S$ in the context
$\Gamma^{\prime};{{\Phi|_{n}},{\Psi}}$.

To unify two polymorphic types, $(\alpha{:}(\Psi\vdash^{n}*))\rightarrow T$
against $(\alpha{:}(\Psi^{\prime}\vdash^{n}*))\rightarrow S$, we first match
$\Psi$ against $\Psi^{\prime}$ and subsequently match $T$ against $S$. The
first context match is not strictly necessary in our setting, as $\Psi$ and
$\Psi^{\prime}$ are type variable contexts and hence do not themselves contain
any pattern variables themselves. Nevertheless, we keep the general form, as
it highlights how one would extend it to a fully dependently typed system
where types could also depend on term variables.

For pattern variables, where we match $\alpha$ against a type $T$, there are
three cases we need to consider. Note that we again omit writing the identity
substitution that is associated with the pattern type variable $\alpha$.

1) if $T$ contains $\alpha$ (occur’s check), then we return a context where we
add a contradiction. The constraints are unsatisfiable, and hence, we can
conclude anything.

2) if $\alpha$ is not yet constrained, we add $(\hat{\Phi}^{k}.T)$ as a
constraint, making sure that $T$ is well-typed in ${{\Gamma_{1}},{\Phi}}$.
This will ensure that the resulting constrained context is well-formed.

3) if $\alpha$ was associated with a constraint $\alpha:=(\hat{\Phi}^{k}.S)$,
then we continue to match $S$ against $T$.

We omit here the symmetric variable cases where $T=\alpha$ for compactness and
lack of space, but they follow the same principle

Further, we mostly concentrate here on the cases where unification succeeds;
the omitted cases, where $T$ is not a pattern type variable and $T$ and $S$ do
not share the top-level type constructor, lead to a contradiction. This is
reflected in returning the context $\Gamma,\\#$.

In practice, we use the given unification algorithm for bi-directional
matching where both sides $T$ and $T_{i}$ have distinct unification variables.
During type-checking, we match $T_{i}$ (type of the pattern) against $T$ (the
type of the scrutinee), and we instantiate meta-variables in $T$. During
runtime, the type $T$ is concrete, and we match $T$ against $T_{i}$ to select
the appropriate branch in the case-expression.

As a consequence, our unification algorithm is biased. For example, if $\beta$
occurs before $\alpha$ in $\Gamma$, and we encounter a unification problem
$\alpha=\beta$, we will instantiate $\alpha$. If $\alpha\rightarrow\alpha$ is
the type of the pattern and $\beta$ is the type of the scrutinee, the
algorithm will fail. This is in line with our intuition that the pattern
refines the type of the scrutinee, but not vice versa.

Unification on contexts proceeds recursively using the judgment
$\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Phi\searrow\Gamma^{\prime}$.
Here $\Gamma$ denote the pattern variables. The context
${{\Gamma_{0}},{\Psi}}$ and ${{\Gamma_{0}},{\Phi}}$ are well-formed, i.e., all
declarations in $\Gamma$ are at higher levels than declarations in
$\Gamma_{0}$, and all declarations in $\Gamma_{0}$ are at higher levels than
declarations in $\Psi$ and $\Phi$. We maintain these criteria during
unification, which helps us to cleanly manage variable dependencies.

###### Lemma 4.2.

If $~{}\Gamma^{\prime}\succeq\Gamma$ and
$\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=T^{\prime}$ then
$\Gamma^{\prime}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=T^{\prime}$.

We next state and prove some properties of unification.

###### Lemma 4.3 (Well-defined Unification).

Assume
$\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma},{{{\Gamma_{0}},{\Psi}}}}$.

  1. (1)

If $\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma},{{{\Gamma_{0}},{\Phi}}}}$
then there is a $\Gamma^{\prime}$ s.t.
$\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Psi=\Phi\searrow\Gamma^{\prime}$.

  2. (2)

If ${{\Gamma},{\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T$
${{\Gamma},{\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S$ then there is a
$\Gamma^{\prime}$ s.t.
$\Gamma;\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}$

###### Lemma 4.4 (Soundness of Unification).

  1. (1)

If
$\Gamma;\Gamma_{0}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Phi=\Psi\searrow\Gamma^{\prime}$
then
${{\Gamma^{\prime}},{\Gamma_{0}}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Phi=\Psi$
and $\Gamma^{\prime}\succeq\Gamma$.

  2. (2)

If $\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}{{\Gamma},{\Phi}}$ and
$\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}$
then $\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\Gamma^{\prime}$ and
${{\Gamma^{\prime}},{\Phi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S$ and
$\Gamma^{\prime}\succeq\Gamma$.

###### Lemma 4.5 (Unification is stable under substitution).

If ${{\Gamma},{\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T$ and
${{\Gamma},{\Psi}}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S$ and
$\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}$
and $\Gamma_{1}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma$ then
there is $\Gamma^{\prime}_{1}$ such that
$\Gamma_{1};[\sigma/\hat{\Gamma}]\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[{{(\sigma/\hat{\Gamma})},{(\mathsf{id}(\hat{\Phi})/\hat{\Phi})}}]T=[{{(\sigma/\hat{\Gamma})},{(\mathsf{id}(\hat{\Phi})/\hat{\Phi})}}]S\searrow\Gamma^{\prime}_{1}$
and
$\Gamma^{\prime}_{1}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma^{\prime}$

###### Proof.

By induction on the structure of
$\Gamma;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}$.
Note that if $\Gamma^{\prime}_{1}$ contains $\\#$,
$\Gamma^{\prime}_{1}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma^{\prime}$
becomes trivial with
$\Gamma_{1}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma:\Gamma$. ∎

###### Lemma 4.6 (Unification is Compatible with Structural Equality).

For pure context $\Psi$, if $\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T$ and
$\Psi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S$ and
$\mathcal{D}:\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S$ and
$\mathcal{E}:\cdot;\Phi\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}T=S\searrow\Gamma^{\prime}$
then $\Gamma^{\prime}=\cdot$

###### Proof.

By induction on the structure of $\mathcal{D}$ and case analysis on the
structure of $\mathcal{E}$. ∎

###  4.6. Operational Semantics for Case-expressions

We define here the operational semantics of case-expressions and show that
types are preserved. Together with the reduction rules for our core multi-
level lambda-calculus that emerge from Sec. 3.6 this provides an operational
semantics for Mœbius.

$\begin{array}[]{lcl}(\mathsf{fn}\;x\rightarrow
e)~{}v&\Longrightarrow&[(~{}.v)/x^{0}]e\\\ (\mathsf{Fn}\;\alpha^{n}\rightarrow
e)~{}(\hat{\Phi}^{n}.T)&\Longrightarrow&[(\hat{\Phi}^{n}.T)/\alpha^{n}]e\\\
\mathsf{let}\,\mathsf{box}\;\hat{\Phi}^{n}.u\;{=}\;\mathsf{box}(\hat{\Phi}^{n}.\,e)\;\mathsf{in}\;e^{\prime}&\Longrightarrow&[(\hat{\Phi}^{n}.e)/u^{n}]e^{\prime}\\\\[7.5pt]
\lx@intercol\hfil\mathsf{case}_{\lceil\Phi\vdash^{k}T\rceil}\
{(\mathsf{box}(\hat{\Phi}^{k}.\,e))}\
\mathsf{of}{~{}\overrightarrow{(\Psi_{i}.(\hat{\Phi}_{i}.q_{i}):(\Phi_{i}\vdash^{k}T_{i})\rightarrow
e^{\prime}_{i})}}\Longrightarrow[\sigma_{i}/\hat{\Psi}_{i}]e^{\prime}_{i}\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma_{i}:\Psi_{i}\qquad\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma_{i}/\hat{\Psi}_{i}]\lceil\Phi_{i}\vdash^{k}T_{i}\rceil=\lceil\Phi\vdash^{k}T\rceil\qquad\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma_{i}/\hat{\Psi}_{i}]\mathsf{box}(\hat{\Phi}_{i}.\,q_{i})=\mathsf{box}(\hat{\Phi}^{k}.\,e)\hfil\lx@intercol\end{array}$
Figure 11. Operational Semantics: $e\Longrightarrow e^{\prime}$

Last, we prove type preservation. In the proof below, we only concentrate on
case-expressions; the remaining cases follow the arguments for local soundness
given in Sec. 3.6.

###### Theorem 4.7 (Type preservation).

If $\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e:T$ and $e\Longrightarrow
e^{\prime}$ then $\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e^{\prime}:T$.

###### Proof.

By case analysis on the second derivation. We show below only the case where
$e$ is a $\mathsf{case}$ expression.

#### Case

$\mathsf{case}_{\lceil\Phi\vdash^{k}T\rceil}\
{(\mathsf{box}(\hat{\Phi}^{k}.\,e))}\
\mathsf{of}{~{}\overrightarrow{(\Psi_{i}.(\hat{\Phi}_{i}.q_{i}):(\Phi_{i}\vdash^{k}T_{i})\rightarrow
e^{\prime}_{i})}}\Longrightarrow[\sigma_{i}/\hat{\Psi}_{i}]e^{\prime}_{i}$
$\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\mathsf{case}_{\lceil\Phi\vdash^{k}T\rceil}\
{(\mathsf{box}(\hat{\Phi}^{k}.\,e))}\
\mathsf{of}{~{}\overrightarrow{(\Psi_{i}.(\hat{\Phi}_{i}.q_{i}):(\Phi_{i}\vdash^{k}T_{i})\rightarrow
e^{\prime}_{i})}}:S$ by assumption
$\Psi_{i}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\lceil\Phi_{i}\vdash^{k}T_{i}\rceil=\lceil\Phi\vdash^{k}T\rceil\searrow\Psi^{\prime}_{i}$
by inversion
$\Psi^{\prime}_{i}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}e_{i}:S$ by inversion
$\mbox{there
exists}~{}\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma_{i}:\Psi_{i}$ by
reduction rule for $\mathsf{case}$
$\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma_{i}/\hat{\Psi}_{i}]\lceil\Phi_{i}\vdash^{k}T_{i}\rceil=\lceil\Phi\vdash^{k}T\rceil\searrow\Gamma$
$\Gamma\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma_{i}:\Psi^{\prime}_{i}$ by
unification stability under substitution lemma 4.5
$\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma_{i}/\hat{\Psi}_{i}]\lceil\Phi_{i}\vdash^{k}T_{i}\rceil=\lceil\Phi\vdash^{k}T\rceil$
by reduction rule for $\mathsf{case}$
$\Gamma=\cdot$ by unification compatibility with structural equality 4.6
$\Psi^{\prime}_{i}\succeq\Psi_{i}$ and therefore
$\hat{\Psi}^{\prime}_{i}=\hat{\Psi}_{i}$ by soundness of unification lemma 4.4
and inversion on
$\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}\sigma_{i}:\Psi^{\prime}_{i}$
$\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma_{i}/\hat{\Psi}^{\prime}_{i}]e_{i}:S$
by simultaneous substitution lemma 3.6 and the fact that
$\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}S$
$\cdot\mathrel{\vdash{\\!\\!\\!\\!\\!}\vdash}[\sigma_{i}/\hat{\Psi}_{i}]e_{i}:S$
since $\hat{\Psi}^{\prime}_{i}=\hat{\Psi}_{i}$
∎

##  5\. Related Work

#### Early staged computation systems

Davies and Pfenning [2001] first observed that the necessity modality of the
S4 modal logic is ideally suited to distinguish between closed code which has
type ${\square}\tau$ and programs, which have type $\tau$ in multi-staged
programming setting. To characterize open code fragments, Davies [1996]
proposed $\lambda^{\bigcirc}$ which corresponds to linear temporal logic. Open
code is characterized by the type ${\bigcirc}\tau$. While this logical
foundation provides an explanation for generating and splicing in open code,
we cannot distinguish open from closed code and the type system of
$\lambda^{\bigcirc}$ does not provide guarantees for its safe evaluation. The
reason is exactly in the openness: it is not sound to evaluate an open
expression before all of its free variables are bound. This openness also
makes it difficult to support pattern matching on (open) code.

The desire to combine the advantages of $\lambda^{\square}$ and
$\lambda^{\bigcirc}$ has inspired a long line of research on type systems for
staged computation, most notable being MetaML [Taha and Sheard 2000] and in
particular, the work of Taha and Nielsen [2003] on environment classifiers
which allows manipulation of open code and supports type inference.
Environment classifiers give names for typing environments to specify when
exactly its $\mathsf{eval}$ function can correctly insert code, but unlike
contextual types does not list the variables that may occur in an environment
(or context) concretely. Instead, we reason about environments and their
extensions abstractly. Inherent in the nature of that work is that we do not
reason about the concrete variables that occur in a given piece of code. It
seems hence less expressive than using contextual types, and, in particular,
it seems difficult to extend to support pattern matching on code. As Taha
[2000] observed, adding intensional analysis to MetaML would make many
optimizations unsound. Environment classifiers also seem too coarse to
characterize the dependencies that exist within the context of assumptions.
This however seems critical when adding System F style polymorphism, as we do
in this work, or extending such a system to dependent types.

#### Reflecting contexts in types

Subsequent work by Kim et al. [2006] characterizes open code using typing
environments (using extensible records). Since their goal is to extend ML with
Lisp’s ability to write both hygienic (via capture-avoiding substitution) and
unhygienic (via capturing substitution) templates, variables are treated
symbolically, unlike with contextual types. As a result, code templates are
not guaranteed to be lexically well-scoped.

Kiselyov et al. [2016] describes a staged calculus <NJ> that safely permits
open code movements across different binding environments. The key to ensuring
hygiene and type safety when manipulating open code is reflecting free
variables of a code fragment in its type, which evokes contextual modal type
theory. However, unlike CMTT, that work uses environment classifiers with the
argument that a type does not need to know exactly in which order free
variables are bound. We would disagree. Especially when moving to a richer
type system where we track dependencies among assumptions, we do need to know
the order. Contextual types provide a more exact and general approach to model
and reason about variable dependencies.

Rhiger [2012] shows a typed Kripke-style calculus for staged computation
$\lambda^{[]}$, supporting evaluation under binders in future stages,
manipulation of open code, and mutable state. It uses its own notion of
contextual modal types, which models linear time (the typing judgment tracks
all future stages), rather than the branching time of our contextual modal
types. As in the work on MetaML, the context is still represented abstractly,
and we hence lack the ability to express dependencies among assumptions.

#### Inspecting code

Closely related to using contextual types to model typed code fragments, Chen
and Xi [2003, 2005] characterize typeful code representations pairing the list
of value types that may appear in a given code together with the type of the
code itself. This is reminiscent of what contextual types accomplish, but
fundamentally uses a de Bruijn representation to model bound variables
occurring in code. This is also a popular approach when modeling object
languages in proof assistants and supporting mechanizing meta-theory (see for
example [Benton et al. 2012]). In Chen and Xi [2005], the authors sketch how
to add pattern matching on code, but it remains unclear how to exploit the
full potential of pattern matching. In particular, the refinement of types,
which happens when pattern matching on polymorphic code, is omitted.

One of the few works that have investigated code inspection via pattern
matching in a typed multi-staged programming setting is by Viera and Pardo
[2006]. Similar to contextual types, the type of code fragments,
$\mathsf{cod}^{\Gamma}$, are annotated with a typing environment of the free
variables. However, unlike Mœbius, the type of the code fragment is not
tracked, and hence we cannot fully reason about the type of open code.
Instead, type-checking of evaluated code fragments is deferred to runtime. The
complexity that arises from pattern matching on typed code fragments is hence
sidestepped.

Parreaux et al. [2018] describe Squid, a Scala macro library which supports
code generation and code inspection using a rewrite primitive. This allows
programmers to define code transformations without extra code for the
traversal through the program itself. This is very convenient in practice.
Yet, from a theoretical point of view, it remains unclear how these rewrite
rules are applied (i.e. in what context is a rule applied) and what conditions
the rewrite rules must satisfy (i.e. should these rules be non-overlapping,
deterministic in how they are applied, etc.).

#### Beside multi-staged programming: Typed Self-Interpreter

Many popular languages have a self-interpreter, that is, an interpreter for
the language written in itself. In this line of work we do not reason about
different stages of computation, however we can respresent programs within the
language and recover a program from its representation. Most recently, Brown
and Palsberg [2016] show that System Fω is capable of representing a self-
interpreter, a program that recovers a program from its representation and is
implemented in the language itself. To circumvent the limits of the type
language, they encode types and type-level functions extensionally as an
instantiation function. Our work, which sits between System Fω and System F,
faced a similar problem and choses an intensional encoding instead. While we
do not literally support type-level computation as in System Fω, we do support
contextual kinds and view contextual type variables as a closure. This
simplifies the equational theory compared to System Fω. Further, our notion of
levels gives us the appropriate structure to describe type and code pattern
typing in case-expressions enabling an intensional analysis of code.

#### Modal Dependent Type Theory

Recently, there has been also interest in developing a dependently typed modal
type theory that includes the box-modality. In particular, Gratzer et al.
[2019] describe such a type theory which, in principle, allows us to describe
the generation of dependently typed and polymorphic code using box and unbox.
Their modal dependent type theory exploits a Fitch-style system where locks
are added to the context of assumptions. Those locks manage access to
variables in a similar fashion as context stacks in Kripke-style modal type
systems. Intuitively existing assumptions are locked when we enter a new stage
and go under a box expression. But in that work, _all_ prior assumptions are
unlocked. This essentially removes the ability to reason about different
stages, as all prior stages are treated the same; the system also has no
ability to run code. Hence, this work lacks the ability to reason about multi-
staged code and run it. It also does not support reasoning about open code nor
pattern matching on code, which raise independent issues.

Pientka et al. [2019] present a Martin Löf type theory that uses the box
modality. This work allows the generation and analysis of code using pattern
matching. However code is represented in the logical framework LF and only a
subset of the computation language can be directly embedded into LF. As such,
the system is not a homogeneous programming language and not rich enough to
generally model code that contains nested boxed and let box expressions. It
also does not allow us to model multi-staged metaprogramming, as the system is
fundamentally restricted to two stages.

Kawata and Igarashi [2019] develop a dependently typed multi-stage calculus
based on the logical framework LF that supports execution of code and cross-
stage persistence, but does not handle pattern matching or polymorphism. Their
approach based on environment classifiers and cross-stage persistence
annotations provides less fine-grained control compared to the use of
contextual types and level annotations.

##  6\. Conclusion

This paper describes a metaprogramming foundation that, for the first time,
supports the generation of typed polymorphic code and its analysis via pattern
matching. This is accomplished by generalizing contextual types to a multi-
level contextual type system. This allows us to disentangle the notions of
levels and stages. While a stage refers to when at run-time code is generated
vs executed, levels are annotations on code and the variables that appear
inside the code. These level annotations on variables allow us to cleanly
distinguish between holes whose value is supplied at runtime (global
variables) and holes (local variables) that will be instantiated when the code
is spliced into another code fragment. Hence levels enforce a stratification
of variables based on how they are used.

The multi-level contextual types are the key to defining pattern matching on
code and type fragments and unlocking the full potential of typed meta-
programming. More specifically, the multiple levels are crucial to support
generating and inspecting code which itself generates code.

An important benefit of multi-level contextual types is that they allow us to
work with clean and high-level type and code pattern abstractions where we
neither expose nor commit to a concrete representation of variable bindings
and contexts. We see our work as a step towards building a general type-
theoretic foundation for multi-staged metaprogramming that, on the one hand,
enforces strong type guarantees and, on the other hand, makes it easy to
generate and manipulate code. This will allow us to exploit the full potential
of metaprogramming without sacrificing the reliability of and trust in the
code we are producing and running.

In the immediate future, we aim to add context abstraction to Mœbius following
the approach taken in Beluga. Abstracting over contexts is an orthogonal
issue, which, we believe, is compatible with the foundation of Mœbius. In the
longer term, we aim to generalize the foundations to dependent types. This
would provide the first dependently-type meta-programming language.

##  7\. Acknowledgments

This work was funded by the Natural Sciences and Engineering Research Council
of Canada (grant number 206263), Fonds de recherche du Québec - Nature et
technologies (grant number 253521), and a graduate fellowship from Fonds de
recherche du Québec - Nature et technologies (grant number 304215) awarded to
the first author.

## References

  * [1]
  * Anand et al. [2018] Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018.  Towards Certified Meta-Programming with Typed Template-Coq. In _9th International Conference Interactive Theorem Proving (ITP’18)_ _(Lecture Notes in Computer Science (LNCS 10895))_. Springer, 20–39.  https://doi.org/10.1007/978-3-319-94821-8_2
  * Benton et al. [2012] Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride. 2012.  Strongly Typed Term Representations in Coq.  _J. Autom. Reasoning_ 49, 2 (2012), 141–159.  https://doi.org/10.1007/s10817-011-9219-0
  * Boespflug and Pientka [2011] Mathieu Boespflug and Brigitte Pientka. 2011.  Multi-level Contextual Modal Type Theory. In _6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP’11)_ _(Electronic Proceedings in Theoretical Computer Science (EPTCS))_ , Vol. 71. 29–43.
  * Brown and Palsberg [2016] Matt Brown and Jens Palsberg. 2016.  Breaking through the normalization barrier: a self-interpreter for F-Omega. In _43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’16)_. ACM, 5–17.  https://doi.org/10.1145/2837614.2837623
  * Chen and Xi [2003] Chiyan Chen and Hongwei Xi. 2003.  Meta-Programming through Typeful Code Representation. In _8th ACM SIGPLAN International Conference on Functional Programming (ICFP’03)_. 275–286.
  * Chen and Xi [2005] Chiyan Chen and Hongwei Xi. 2005.  Meta-programming through Typeful Code Representation.  _Journal of Functional Programming_ 15, 5 (2005), 797–835.  https://doi.org/10.1017/S0956796805005617
  * Davies [1996] Rowan Davies. 1996\.  A Temporal-Logic Approach to Binding-Time Analysis. In _11th IEEE Symposium on Logic in Computer Science (LICS)_. IEEE Computer Society, 184–195.  https://doi.org/10.1109/LICS.1996.561317
  * Davies and Pfenning [2001] Rowan Davies and Frank Pfenning. 2001.  A modal analysis of staged computation.  _J. ACM_ 48, 3 (2001), 555–604.  https://doi.org/10.1145/382780.382785
  * Gratzer et al. [2019] Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. 2019\.  Implementing a Modal Dependent Type Theory.  _Proceedings of the ACM on Programming Languages (PACMPL)_ 3, ICFP (2019), 107:1–107:29.  https://doi.org/10.1145/3341711
  * Kawata and Igarashi [2019] Akira Kawata and Atsushi Igarashi. 2019.  A Dependently Typed Multi-stage Calculus. In _17th Asian Symposium on Programming Languages and Systems (APLAS)_ _(Lecture Notes in Computer Science)_ , Vol. 11893. Springer, 53–72.  https://doi.org/10.1007/978-3-030-34175-6_4
  * Kim et al. [2006] Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. 2006\.  A Polymorphic Modal Type System for Lisp-like Multi-Staged Languages. In _33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06)_. ACM Press, 257–268.  https://doi.org/10.1145/1111037.1111060
  * Kiselyov et al. [2016] Oleg Kiselyov, Yukiyoshi Kameyama, and Yuto Sudo. 2016\.  Refined Environment Classifiers - Type- and Scope-Safe Code Generation with Mutable Cells. In _14th Asian Symposium on Programming Languages and Systems (APLAS’16)_ _(Lecture Notes in Computer Science)_ , Vol. 10017. 271–291.  https://doi.org/10.1007/978-3-319-47958-3_15
  * Miller [1991] Dale Miller. 1991\.  Unification of Simply Typed Lambda-Terms as Logic Programming. In _8th International Logic Programming Conference_. MIT Press, 255–269.
  * Nanevski et al. [2008] Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008\.  Contextual Modal Type Theory.  _ACM Trans. Comput. Logic_ 9, 3 (June 2008), 1–49.  https://doi.org/10.1145/1352582.1352591
  * Parreaux et al. [2018] Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch. 2018.  Unifying Analytic and Statically-Typed Quasiquotes.  _Proceedings of the ACM on Programming Languages (PACMPL)_ 2, POPL (2018), 13:1–13:33.  https://doi.org/10.1145/3158101
  * Pientka [2003] Brigitte Pientka. 2003\.  _Tabled higher-order logic programming_.  Ph.D. Dissertation. Department of Computer Science, Carnegie Mellon University.  CMU-CS-03-185.
  * Pientka [2008] Brigitte Pientka. 2008\.  A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In _35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08)_. ACM Press, 371–382.
  * Pientka et al. [2019] Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, and Rebecca Zucchini. 2019\.  A Type Theory for Defining Logics and Proofs. In _34th IEEE/ ACM Symposium on Logic in Computer Science (LICS’19)_. IEEE Computer Society, 1–13.
  * Pientka and Cave [2015] Brigitte Pientka and Andrew Cave. 2015.  Inductive Beluga:Programming Proofs (System Description). In _25th International Conference on Automated Deduction (CADE-25)_ _(Lecture Notes in Computer Science (LNCS 9195))_. Springer, 272–281.
  * Pientka and Dunfield [2008] Brigitte Pientka and Jana Dunfield. 2008.  Programming with proofs and explicit contexts. In _ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’08)_. ACM, 163–173.
  * Pientka and Dunfield [2010] Brigitte Pientka and Jana Dunfield. 2010.  Beluga: a Framework for Programming and Reasoning with Deductive Systems (System Description). In _5th International Joint Conference on Automated Reasoning (IJCAR’10)_ _(Lecture Notes in Artificial Intelligence (LNAI 6173))_. Springer, 15–21.
  * Rhiger [2012] Morten Rhiger. 2012\.  Staged Computation with Staged Lexical Scope. In _21st European Symposium on Programming Languages and Systems (ESOP’12)_ _(Lecture Notes in Computer Science)_ , Vol. 7211. Springer, 559–578.  https://doi.org/10.1007/978-3-642-28869-2_28
  * Sheard and Jones [2022] Tim Sheard and Simon Peyton Jones. 2022.  Template Meta-Programming for Haskell. In _ACM SIGPLAN Workshop on Haskell_ _(Haskell’02)_. ACM, 1–16.  https://doi.org/10.1145/581690.581691