A Specification for Typed Template Haskell

Matthew Pickering

Department of Computer Science
University of Bristol

United Kingdom

Andres Löh

Well-Typed LLP

Nicolas Wu

Department of Computing
Imperial College London

United Kingdom

Multi-stage programming is a proven technique that provides predictable
performance characteristics by controlling code generation.
We propose a core semantics for Typed Template Haskell, an extension of Haskell
that supports multi staged programming that interacts well with polymorphism
and qualified types.
Our semantics relates a declarative source language with qualified types to a core language
based on the the polymorphic lambda calculus augmented with multi-stage constructs.

[B]concept95 id>10011007.10011006.10011008</concept95 id>[E]

[B]concept95 desc>Software and its engineering∼General programming languages</concept95 desc>[E]

[B]concept95 significance>500</concept95 significance>[E]

[B]concept95 id>10003456.10003457.10003521.10003525</concept95 id>[E]

[B]concept95 desc>Social and professional topics∼History 𝐨𝐟 programming languages</concept95 desc>[E]

[B]concept95 significance>300</concept95 significance>[E]

[500]Software and its engineering General programming languages
[300]Social and professional topics History of programming languages

§ INTRODUCTION

Producing optimal code is a difficult task that is greatly assisted by staging
annotations, a technique which has been extensively studied
and implemented in a variety of languages
<cit.>. These annotations give programmers fine control
by instructing the compiler to generate code in one stage of compilation that
can be used in another.

The classic example of staging is the  function, where the value $n^k$
can be efficiently computed for a fixed $k$ by generating code where the
required multiplications have been unrolled and inlined.  The incarnation of
staged programming in Typed Template Haskell
[Typed Template Haskell is a variation of the Template
Haskell <cit.> that adds types in the style of MetaML <cit.>.
The abstract datatype  in this paper is a newtype wrapper around .
In GHC, typed quotes are implemented by 91124124 12412493 and typed splices by 363640 41
, rather than  and . It was implemented in 2013 by Geoffrey Mainland (who also used  as a motivating example) under a proposal by
Simon Peyton Jones.]
benefits from
type classes, one of
the distinguishing features of Haskell <cit.>, allowing a
definition that can be reused for any type that is qualified to be numeric:
B@>l<@10@>l<@14@>c<@14E@l@17@>l<@E@>l<@[B]power::Num a⇒Int→Code a→Code a[E]

[B]power 0 [10]

[B]power k [10]
[17]$(cn)*$(power (k-1) cn)[E]
Any value  can
be quoted to create ,
then spliced in the
expression  to generate
Thanks to type class polymorphism, this works when  has any fixed type
that satisfies the  interface, such as ,  and countless
other types.

It is somewhat surprising, then, that the following function fails to compile
in the latest implementation of Typed Template Haskell in GHC 8.10.1:
B@>l<@E@>l<@[B]power5::Num a⇒a→a[E]

[B]power5 n=$(power 5 n)[E]
Currently, GHC complains that there is no instance for
available, which is strange because the type signature explicitly
states that  may be assumed. But this is not the only problem with
this simple example:
in the definition of , the constraint is used
inside a quotation but is bound outside.
As we will see, this is an ad-hoc decision that then leads to subtle inconsistencies.

This paper sets out to formally answer the question of how a language with
polymorphism and qualified types should interact with a multi-stage programming
As well as the fact that all code generation happens at compile time,
these are features that distinguish Typed Template Haskell,
which until now has had no formalism even though it is an extension already
fully integrated into GHC.  We extend previous work that looked at cross-stage
persistence in this setting <cit.> by more closely
modelling the reality of the type system implemented in GHC. In particular the
implications of compile-time code generation are considered, as are the
impredicativity restriction and the interaction with instance definitions.

Providing a formalism for the interaction of polymorphism, qualified types, and
multi-stage programming has important consequences for Typed Template Haskell
and other future implementations that combine these features. This
specification resolves the uncertainty about how it should interact with new
language features. It has also been unclear how to fix a large number of bugs
in the implementation because there is no precise semantics it is supposed to
operate under. Presently these deficiencies hampered the adoption of
meta-programming in Haskell as a trusted means of producing code with
predictable performance characteristics. This untapped potential has been
demonstrated to be beneficial in other staged
systems in
MetaML <cit.>,
Scala's LMS <cit.>,
MetaOCaml <cit.>.
State that staging allows control of performance without having to look at
core, which is infamously difficult to work with

At first glance it may appear that constructing programs using only quotations
and splices is restrictive.  However, multi-stage programming is widely
applicable to any domain in which statically known abstractions should be
eliminated. Some particular examples include removing the overhead of using
parser combinators <cit.>, generic programming <cit.> and effect handlers <cit.>. Furthermore, there
are certain interesting techniques and tricks which are useful when
constructing multi-stage programs that can vastly improve performance

Following a brief introduction to staging with Typed Template Haskell
(Section <ref>), this paper makes the following contributions:

* We demonstrate the problems that arise from the subtle interaction between qualified constraints and staging, which highlights the need for a clear specification (Section <ref>).

* We introduce a type system for a source language which models Typed
Template Haskell and introduces a new constraint form (Section <ref>).

* We introduce an explicitly typed core language which is System F extended
with multi-stage features (Section <ref>).

* We give the elaboration semantics from the source language into the core
language (Section <ref>).

Future directions including type inference, the latest developments in
supporting impredicativity and notes about an implementation are then
discussed (Section <ref>). This work is put into the context of
related work (Section <ref>), before finally concluding
(Section <ref>).

§ BACKGROUND: MULTI-STAGED PROGRAMMING

This section describes the fundamental concepts of Typed Template
Haskell as currently implemented in GHC. In these aspects, the current
implementation coincides with our proposed specification of Typed Template Haskell,
as we are excluding polymorphism and
type classes. This serves as preparation for more interesting
examples that are discussed later (Section <ref>).

Typed Template Haskell is an extension to Haskell which implements the two
standard staging annotations of multi-stage programming: quotes and
splices.  An expression  can be quoted to generate
the expression . Conversely, an expression
can be spliced to extract the expression . An expression of
type  is a representation of an expression of type .
Given these definitions, it may seem that quotes and splices can be
used freely so long as the types align: well-typed problems don't go wrong, as
the old adage says; but things are not so simple for staged programs. As well
as being well-typed, a program must be well-staged, whereby the level of variables is considered.

The concept of a level is of fundamental importance in multi-stage programming.
The level of an expression is an integer given by the number of quotes that
surround it, minus the number of splices: quotation increases the level and
splicing decreases the level.
Negative levels are
evaluated at compile time, level  is evaluated at runtime and positive levels
are future unevaluated stages.[Unlike MetaML <cit.>, code
generation in Typed Template Haskell is only supported at compile time, and
therefore there is no  operation.]
The goal of designing a staged calculus is to ensure that the levels of the
program can be evaluated in order so that an expression at a particular level
can only be evaluated when all expressions it depends on at previous levels
have been first evaluated.
Would it make sense to define “stage” here? “The goal of designing a staged
calculus is to ensure that the levels of the program can be evaluated in stages
so that …?

In the simplest setting, a program is well-staged if each variable it
mentions is used only at the level in which it is bound. Doing so in any other
stage may simply be impossible, or at least require special attention.
The next three example programs, , , and , are all well-typed,
but only the first is well-staged.

Using a variable that was defined in the same stage is permitted. A variable
can be introduced locally using a lambda abstraction inside a quotation and then used
freely within that context:
B@>l<@E@>l<@[B]timely::Code (Int→Int)[E]

Of course, the variable is still subject to the usual scoping rules of abstraction.

Using a variable at a level before it is bound is
problematic because at the point we wish to evaluate the prior stage, we will
not yet know the value of the future stage variable and so the evaluation will
get stuck:
B@>l<@E@>l<@[B]hasty::Code Int→Int[E]

[B]hasty c=$(c)[E]
Here, we cannot splice  without knowing the concrete representation that
will be instantiated to.
There is no recovery from this situation without violating the fact that lower
levels must be fully evaluated before higher ones.

Using a variable at a stage after it is bound is problematic because the
variable will not generally be in the environment.  It may, for instance, be
bound to a certain known value at compile time but no longer present at runtime.
B@>l<@E@>l<@[B]tardy::Int→Code Int[E]

[B]tardy 𝑥=𝑥[E]
In contrast to the  example, the situation is not hopeless here: there are ways to
support referencing previous-stage variables, which is called cross-stage
persistence <cit.>.

One option is to interpret a variable from a previous stage using a lifting
construct which copies the current value of the variable into a future-stage
representation. As the process of lifting is akin to serialisation, this can be
achieved quite easily for base types such as strings and integers, but more
complex types such as functions are problematic.

Another option is to use path-based persistence: for example, a top-level
identifier defined in another module can be persisted, because we can assume that
the other module has been separately compiled, so the top-level identifier is still
available at the same location in future stages.

I think this commented para is redundant?

GHC currently implements the restrictions described above. For cross-stage
persistence, it employs both lifting and path-based persistence. Top-level
variables defined in another module can be used at any level. Lifting is
restricted to types that are instances of a type class  and witnessed
by a method
B@>l<@E@>l<@[B]lift::Lift a⇒a→Code a[E]
which notably excludes function types and other abstract types such as .
An example such as  can then be viewed as being implicitly rewritten
B@>l<@E@>l<@[B]tardy'::Int→Code Int[E]

[B]tardy' 𝑥=$(lift 𝑥)[E]
in which the reference of  occurs at the same level as it is bound.
For this reason, our formal languages introduced in Section <ref>
and Section <ref>
will consider path-based persistence, but not implicit lifting, as this is
easy to add separately in the same way as GHC currently implements it.

Let us consider the example from the introduction once again:
B@>l<@10@>l<@14@>c<@14E@l@17@>l<@E@>l<@[B]power 0 [10]

[B]power k [10]
[17]$(cn)*$(power (k-1) cn)[E]
This example makes use of quotes and splices. The references to the
variables ,  and  are all at the same level as their
binding occurrence, as they occur within one splice and one quote.
The static information is the exponent  and the run-time information
is the base . Therefore by using the staged function the static information
can be eliminated by partially evaluating the function at compile-time by using
a top-level splice. The generated code does not mention the static

When using Typed Template Haskell, it is common to just deal with two stages, a
I've changed “two levels” to “two stages” here. I think even in Typed Template
Haskell, one is actually using at least three levels frequently: , , and .
compile-time stage and a run-time stage. The compile-time stage contains all
the statically known information about the domain, the typing rules ensure that
information from the run-time stage is not needed to evaluate the compile-time
stage and then the program is partially evaluated at compile-time to evaluate
the compile-time fragment to a value.  It is a common misconception that Typed
Template Haskell only supports two stages, but there is no such
restriction.[There is, however, an artificial restriction about
nesting quotation brackets which makes writing programs with more than two
stages difficult. It is ongoing work to lift this restriction.]

Maybe kill this paragraph entirely
I commented it for now, as I also think it does not fit.

§ STAGING WITH TYPE CLASSES AND POLYMORPHISM

I've changed the title from “Motivation: A Problem and an Informal
Solution” as I totally did not get what “the” Problem and what the
Informal Solution is.
You made it “Typed Template Haskell with Type Classes and Polymorphism”, which is better. I think I like “Problems with Type Classes and Polymorphism” or “Understanding Staging with Type Classes and Polymorphism” more. I want to avoid TTH being the only focus. Besides, our position is that TTH includes type classes and polymorphism by specficiation.

The examples in the previous section were simple demonstrations of the
importance of considering levels in a well-staged program.
This section discusses more complicated cases which involve class constraints,
top-level splices, instance definitions and type variables. It is here where
our proposed version of Typed Template Haskell deviates from GHC's current
implementation. Therefore, for each example we will report how the program
should behave and contrast it with how the current implementation in
GHC behaves.

I don't think it's important to flag the  discussion in the signposting, so I'm commenting it out.

§.§ Constraints

Constraints introduced by type classes have the potential to cause staging
errors: type classes are implemented by passing dictionaries as evidence, and the
implicit use of these dictionaries must adhere to the level restrictions discussed in
Section <ref>. This requires a careful
treatment of the interaction between constraints and staging, which GHC
currently does not handle correctly.

Consider the use of a type class method inside a quotation, similarly
to how  is used in  in the introduction:
B@>l<@E@>l<@[B]c_1::Show a⇒Code (a→String)[E]

Thinking carefully about the levels involved, the signature indicates
that the evidence for , which is available at stage , can
be used to satisfy the evidence needed by  at stage .

In the normal dictionary passing implementation of type classes, type class
constraints are elaborated to a function which accepts a dictionary which acts
as evidence for the constraint. Therefore we can assume that the elaborated
version of  looks similar to the following:
B@>l<@E@>l<@[B]d_1::ShowDict a→Code (a→String)[E]

[B]d_1 dShow=show dShow[E]
Now this reveals a subtle problem: naively elaborating without considering
the levels of constraints has introduced a cross-stage reference where
the dictionary variable  is introduced at level  but used at level .
As we have learned in Section <ref>, one remedy of this situation
is to try to make  cross-stage persistent by lifting. However, in general,
lifting of dictionaries is not straightforward to implement. Recall that lifting
in GHC is restricted to instances of the  class which excludes functions –
but type class dictionaries are nearly always a record of functions, so
automatic lifting given the current implementation is not possible.

GHC nevertheless accepts this program, with the underlying problem only being
revealed when subsequently trying to splice the program. We instead argue that
the program  is ill-typed and should therefore be rejected at compilation time.
Our solution is to introduce a new constraint form, , which indicates
that constraint  is available to be used in the next stage. Using this,
the corrected type signature for example <ref> is as follows:

B@>l<@E@>l<@[B]c_1'::CodeC (Show a)⇒Code (a→String)[E]

The  constraint is introduced at level  but indicates that the
constraint will be available to be used at level . Therefore the
constraint can be used to satisfy the  method used inside the
The corresponding elaborated version is similar to the following:
B@>l<@E@>l<@[B]d_1'::Code (ShowDict a)→Code (a→String)[E]

[B]d_1' cdShow=show $(cdShow)[E]
As  is now the representation of a dictionary, we can splice the representation
inside the quote. The reference to  is at the correct level and
the program is well-staged.

Mention about impredicativity here?
Not yet, I think. Let's give more good news first.

The example <ref> uses a locally provided constraint which causes us some
difficulty. We have a different situation if a constraint can be
solved by a concrete global type class instance:

B@>l<@E@>l<@[B]c_2::Code (Int→String)[E]

In , the global  instance is used to satisfy the  constraint
inside the quotation. Since this elaborates to a reference to a top-level
instance dictionary, the reference can be persisted using path-based persistence.
Therefore it is permitted to use top-level instances to satisfy constraints inside
a quotation, in the same way that it is permitted to refer to top-level variables.

Can the following be phrased better?
Maybe improved by stating how GHCs solution could potentially be harmful? Should we say explicitly that our calculus accepts this?
It's not guaranteed that the same  dictionary will be present
in both places using overlapping instances, there is an example if our previous
GHC currently correctly accepts this program. However, it does not actually
perform the dictionary translation until the program is spliced, which is harmless
in this case, because the same  instance is in scope at both points.

§.§ Top-level splices

A splice that appears in a definition at the top-level scope of a module[
Do not confuse this use of “top-level” with the staging level.]
introduces new scoping challenges
because it can potentially require class constraints to be used at levels prior
to the ones where they are introduced.

Since a top-level splice is evaluated at compile time, it should be clear
that no run-time information must be used in a top-level splice definition.
In particular, the definition should not be permitted to access local variables
or local constraints defined at a higher level.
I changed “prior” to “higher” because otherwise, it does not make
sense to me.
This is because local
information which is available only at runtime cannot be used to
influence the execution of the expression during compilation.

In the following example there are two modules.  Module  defines the  class and
contains the definition of a global instance . The  function
from this instance is used in module  in the definition of , which is a
top-level definition. The reference to  occurs inside a top-level splice,
thus at level , and so the  instance is needed a compile time.

B@>l<@3@>l<@E@>l<@[B]𝐦𝐨𝐝𝐮𝐥𝐞 A 𝐰𝐡𝐞𝐫𝐞[E]

[B]𝐜𝐥𝐚𝐬𝐬 Lift a 𝐰𝐡𝐞𝐫𝐞[E]

[3]lift::a→Code a[E]

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 Lift Int 𝐰𝐡𝐞𝐫𝐞[E]

B@>l<@E@>l<@[B]𝐦𝐨𝐝𝐮𝐥𝐞 B 𝐰𝐡𝐞𝐫𝐞[E]

[B]𝐢𝐦𝐩𝐨𝐫𝐭 A[E]

[B]ts_1=$(lift 5)[E]

This program is currently accepted by GHC, and it should be, because the evidence
for a top-level instance is defined in a top-level variable and top-level definitions defined
in other modules are permitted to appear in top-level splices.

I am not terribly happy with the following paragraph. Should this restriction be mentioned
in Section <ref>? Also, the use of “mirror” is wrong because the purpose
of this section is to a large extent to describe how GHC is behaving currently.
The situation is subtly different to top-level quotations as in example <ref>,
because the instance
must be defined in another module which mirrors the restriction
implemented in GHC that top-level definitions can only be used in top-level splices
if they are defined in other modules.

deleted an incorrect sentence here about instanitating a type
On the other hand, constraints introduced locally by a type signature for a
top-level definition must not be allowed.  In the following example, the
constraint is introduced at level  by the type signature of
but used at level  in the body:

B@>l<@E@>l<@[B]𝐝𝐚𝐭𝐚 A=A[E]

[B]ts_2::Lift A⇒A[E]

[B]ts_2=$(lift A)[E]
We assume  is imported from another module as in Example <ref>
and therefore cross-stage persistent.
However, the problem is that the dictionary that will be used to implement the
constraint will not be known until runtime.

Therefore the definition of  is not available to be used
at compile-time in the top-level splice, and GHC correctly rejects this program.
It is evident why this program should be rejected considering the dictionary
translation, in a similar vein to <ref>. The elaboration would amount
to a future-stage reference inside the splice.

So far we have considered the interaction between constraints and quotations
separately to the interaction between constraints and top-level splices.
The combination of the two reveals further subtle issues.
The following function  is at the top-level and
uses a constrained type. This example is both well-typed and well-staged.

B@>l<@E@>l<@[B]ts_3::Ord a⇒a→a→Ordering[E]

In , the body of the top-level splice is a simple quotation of the
method. This method requires an  constraint which is provided by the context
on . The constraint is introduced at level  and also used at level , as
the top-level splice and the quotation cancel each other out. It is therefore
perfectly fine to use the dictionary passed to  to satisfy the requirements
of .

Unfortunately, the current implementation in GHC rejects this program. It generally
excludes local constraints from the scope inside top-level splices, in order to reject
programs like Example <ref>. Our
specification accepts the example by tracking the levels of local constraints.

§.§ The  function revisited

Having discussed constraints and also their interaction with top-level splices, we
can now fully explain
why  function discussed in Section <ref> works in current
GHC when spliced at a concrete type, but fails when spliced with an overloaded type,
whereas it should work for both:

[10]::Num a⇒a→a[30]

[B]power5 n=$(power 5 n)[E]

The two problems are that GHC accepts  at the incorrect type
B@>l<@E@>l<@[B]power::Num a⇒Int→Code a→Code a[E]
(as in Example <ref>)
and that it does not actually perform a dictionary translation for this until
this is spliced. Option M works in GHC, because it finds the  global
instance when splicing, similarly to Example <ref>, and everything is
(accidentally) fine. However, Option P fails because the local constraint is
not made available in the splice as in Example <ref>, and even if it was,
it would be a reference at the wrong level.

As with Example <ref>, we argue that the function
should instead only be accepted at type
B@>l<@E@>l<@[B]power::CodeC (Num a)⇒Int→Code a→Code a[E]
Then, Option M is fine due to the cross-stage persistence of the global
instance declaration; and Option P works as well, as the program will
elaborate to code that is similar to:
B@>l<@E@>l<@[B]power5'::NumDict a→a→a[E]

[B]power5' dNum n=$(power dNum 5 n)[E]
By quoting , the argument to  is a representation
of a dictionary as required, and reference is at the correct level.

§.§ Instance Definitions

The final challenge to do with constraints is dealing with instance definitions
which use top-level splices. This situation is of particular interest as there
are already special typing rules in GHC for instance methods which bring into
scope the instance currently being defined in the body of the instance
definition. This commonly happens in recursive datatypes where the instance
declaration must be recursively defined.

In the same manner as a top-level splice, the body of an instance method
cannot use a local constraint, in particular the instance currently
being defined or any of the instance head in order to influence the code generation
in a top-level splice. On the other hand, the generated code should certainly
be permitted to use the instances from the instance context and the currently
defined instance. In fact, this is necessary in order to generate the majority
of instances for recursive datatypes!
Here is a instance definition that is defined recursively.
B@>l<@3@>l<@13@>c<@13E@l@16@>l<@E@>l<@[B]𝐝𝐚𝐭𝐚 Stream=Cons {1.5mu hd::Int,tl::Stream1.5mu}[E]

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 Eq Stream 𝐰𝐡𝐞𝐫𝐞[E]

[16]hd s_1hd s_2&&tl s_1tl s_2[E]
The instance for  compares the tails of the streams using the
equality instance for  that is currently being defined. This code works
well, as it should, so there is reason to believe that a staged version should
also be definable.

The following is just a small variation of Example <ref> where the body
of the method is wrapped in a splice and a quote:

B@>l<@3@>l<@E@>l<@[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 Eq Stream 𝐰𝐡𝐞𝐫𝐞[E]

[3]()=$(λs_1 s_2→hd s_1hd s_2&&tl s_1tl s_2)[E]
This program should be accepted and equivalent to <ref>,
because in general, .
However, it is presently rejected by GHC, with the claim that the recursive use
of  for comparing the tails is not stage-correct, when in principle
it could and should be made cross-stage persistent.
Is this explanation sufficient?

Yet another variant of Example <ref> is to try to move the recursion
out of the instance declaration, as follows:
B@>l<@E@>l<@[B]eqStream::CodeC (Eq Stream)⇒Code (Stream→Stream→Bool)[E]

[B]eqStream=λs_1 s_2→hd s_1hd s_2&&tl s_1tl s_2[E]
Then, in a different module, we should be able to say:
B@>l<@3@>l<@E@>l<@[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 Eq Stream 𝐰𝐡𝐞𝐫𝐞[E]

It is important that the definition of  uses the new constraint
form  so that the definition of
is well-staged. As  is the instance which is
currently being defined, the  constraint is introduced at level 0 when typing the
instance definition. Therefore, in a top-level splice the local constraint can only be used
by functions which require a  constraint.
This example is similar to  in
Section <ref> but the local constraint is introduced
implicitly by the instance definition.

It is somewhat ironic that while one of the major use cases of untyped
Template Haskell is generating instance definitions such as this one,
it seems impossible to use the current implementation of Typed Template
Haskell for the same purpose.

§.§ Type Variables

This subsection is quite weak. The example does not make sense
( defined in terms of ?). Furthermore, it could easily be
“fixed” anyway because the type variable is used at a single level.
The second half of this section is very technical and abstract, and
I think it distracts from the flow of the paper. Also, the main
argument of not having case distinctions on types prompts the question
is we have difficulties handling equality constraints and/or type
families. I'll defer this for now, but will try to look at this

The previous examples showed that type constraints require special attention in
order to ensure correct staging. It is therefore natural to consider type
variables as well, and indeed previous work by <cit.> ensured that type
variables are were level-aware in order to ensure a sound translation.
However, our calculus will show that this is a conservative position in a
language based on the polymorphic lambda calculus which enforces a phase distinction <cit.> where
typechecking happens entirely prior to running any stages of a program.

Consider the following example that turns a list of quoted
values into a quoted list of those values:
B@>l<@16@>l<@E@>l<@[B]list::∀a.[1.5mu Code a1.5mu]→Code [1.5mu a1.5mu][E]

[B]list [1.5mu 1.5mu][16]
[16]=[1.5mu 1.5mu] @a[E]

[B]list (𝑥:xs)[16]
[16]=(:) @a $(𝑥) $(list @a xs)[E]
The type variable  is bound at level $0$ and used both at at level $1$ (in
its application to the type constructors), and at level $0$ (in its recursive
application to the  function).
If we took the
lead from values then this program would be rejected by the typechecker.
However, because of the in-built phase distinction, evaluation
cannot get stuck on an unknown type variable as all the types will be
fixed in the program before execution starts.  We just need to make sure that
the substitution operation can substitute a type inside a quotation.

As it happens, this definition is correctly accepted by GHC, which is
promising. However, it cannot actually be used since GHC produces compile error
when given an expression such as , since it complains that the type variable  is not in scope during type
checking, and eventually generates an internal error in GHC itself.

Axed this as it amounts to saying "there is a phase-distinction"

I've axed the next para which talks about the solution, since we don't do that in this section and I want this part to be brief.

§.§ Intermediate Summary

This section has uncovered the fact that the treatment of
constraints is rather arbitrary in the current implementation of GHC.
The examples we discussed have been motivated by three different ad-hoc
restrictions that the current implementation exhibits.
Firstly, prior stage constraint references (Section <ref>) are
permitted without any checks.
Secondly, top-level splices
(Section <ref>)
are typechecked in an environment isolated from the
local constraint environment which is an overly conservative restriction.
Thirdly, in an instance definition (Section <ref>), any reference
to the instance currently being defined inside a top-level splice is rejected
even if it is level-correct.
we showed that although
constraints have a role to play in understanding staging, type variables need
no special treatment beyond the correct use of type application
(Section <ref>).

Do the problems uncovered threaten the soundness of the language? In the case
of prior-stage references, they do. The current representation form of
quotations in GHC is untyped and therefore any evidence is erased from the internal
representation of a quotation.
The instance is therefore “persisted by inference”, which operates under
the assumption that enough information is present in an untyped representation
to re-infer all the contextual type information erased after typechecking.
This assumption leads to unsoundness as generated programs will fail to
typecheck, as discussed already by <cit.>.
Future-stage references are forbidden by conservative checks,
which we will aim to make more precise in our calculus in order to accept more programs.

The problems observed so far are the result of interactions between class
constraints and staging.  Our goal now will be to develop a formal calculus to
model and resolve these problems. The approach will be to
introduce a source language  that includes type constraints in addition to
quotes and splices (Section <ref>), and
a core language that is a variant of the explicit polymorphic lambda calculus with multi-stage constructs
(Section <ref>). We then show how the source language can be
translated into a core language where constraints have been elaborated away
into a representation form for a quotation that is typed and where all
contextual type information is saved (Section <ref>).

§ SOURCE LANGUAGE

The source language we introduce has been designed to incorporate the essential
features of a language with metaprogramming and qualified types that is able to
correctly handle the situations discussed in Section <ref>.
We try to stay faithful to GHC's current implementation of Typed Template Haskell
where possible, with the addition of the quoted constraint form  for the reasons
discussed in Section <ref>.

The key features of this language are:

I'm not sure what the status of this list is. Points 1–3 are really about
our contributions. Point 4 is more general, which is why I added point 5. Still
feels a bit arbitrary though.

* Values and constraints are always indexed by the level at which
they are introduced to ensure that they are well-staged.

* The constraint form  indicates that a constraint is
available at the next stage.

* Types (including type variables) are not level-indexed and can be used at any level.

* There is no  operation in the language. All evaluation of code is performed
at compile-time by mean of top-level splices which imply the existence of negative levels.

* Path-based cross-stage persistence is supported.
I removed the discussion of impredicativity here because it is advanced material that hasn't yet been defined. It is now incorporated into the description of syntax.

My gut feeling is that we've compared to GHC's TTH enough already. I want
to remove this paragraph and instead say something pithy: “These features have
been carefully chosen to allow a specification of Typed Template Haskell
that does not suffer from the shortcomings of the current implementation.”

These features have been carefully chosen to allow a specification of Typed
Template Haskell that addresses all the shortcomings identified in Section <ref>
while staying close to the general flavour of meta-programming that
is enabled in its current implementation in GHC.

§.§ Syntax

[23]e|def;pgm|cls;pgm|inst;pgm [E]

[23]𝐝𝐞𝐟 k=e [E]

[23]𝐜𝐥𝐚𝐬𝐬  TC a 𝐰𝐡𝐞𝐫𝐞 {1.5mu k::σ1.5mu} [E]

[23]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞  C⇒TC τ 𝐰𝐡𝐞𝐫𝐞 {1.5mu k=e1.5mu} [E]

[125]  [130]

[18] [18E]
[125]  [130]

[23]λ𝑥τ.e|e e[125]
[125]  [130]

[125]   [130]

[125]  [130]

[18] [18E]
[125]  [130]

[125]  [130]

[23]Code τ[125]
[125]   [130]

[125]  [130]
[125]  [125E]
[23]TC τ|CodeC C[125]
[125]  [125E]
[23]∙|Γ,𝑥(τ,n)|Γ,a|Γ, ev(C,n)[127]
[127]  [127E]
[23]∙|P, ev(∀a.C⇒C)|P,kσ[127]
[127]  [127E]
Source Syntax

The syntax of the source language (Figure <ref>) models programs
with type classes and metaprogramming features.  This syntax
closely follows the models of languages with type classes of
<cit.> and <cit.>,
but with the addition of multi-stage features and without equality or
quantified constraints.

A program  is a sequence of value definitions , class definitions
, and instance definitions  followed by a top-level expression .

Top-level definitions  are added to the calculus to model separate compilation
and path-based cross-stage persistence in a way similar to what GHC currently
implements: only variables previously defined in a
top-level definition can be referenced at arbitrary levels.

Both type classes and instances are in the language, but simplified as far as
possible: type class definitions  have precisely one method and no superclasses;
instance definitions  are permitted to have an instance context.

The expression language  is a standard $\lambda$-calculus
with the addition of the two multi-stage constructs, quotation  and splicing
which can be used to separate a program into stages.

Just as in Haskell, our language is predicative: type variables that appear as
class parameters and in quantifiers range only over monotypes. This is modelled
by the use of a Damas-Milner style Cite Damas-Milner?
type system which distinguishes between monotypes , qualified types  and
polytypes . The type argument to the representation constructor
must be a monotype.

A constraint  is either a type class constraint , or a representation of a constraint .

The environment  is used for locally introduced information, including
value variables , type variables , and local type class axioms
. The environment keeps track of the (integer) level  that value and
constraint variables are introduced at; the typing rules ensure that the
variables are only used at the current level.

The program theory  is an environment of the type class axioms introduced by
instance declarations and of type information for names introduced by top-level
definitions. The axioms are used to dictate whether the usage of a
type class method is allowed or not. The names indicate which variables can
be used in a cross-stage persistent fashion.

§.§ Typing Rules

The typing rules proceed in a predicable way for anyone familiar with
qualified type systems. The difference is that the source expression typing
judgement (Figure <ref>) and constraint entailment judgement
(Figure <ref>) are now indexed by a level.
Furthermore, since these rules are the basis for elaboration into the core
language, they have
been combined with the elaboration rules, as highlighted by a

box whose contents
can be safely ignored until the discussion of elaboration (Section <ref>).

The typing rules also refer to type and constraint formation rules
(Figures <ref> and <ref>),
which check just that type variables are well-scoped (our language does not
include an advanced kind system).

B@>l<@E@>l<@[B]P;Γn e : σt | TSP[E]

B@>l<@E@>l<@[B]𝑥(τ,n) ∈Γ[E]

B@>l<@E@>l<@[B]P;Γn 𝑥 : τ𝑥 | ∙[E]

B@>l<@E@>l<@[B]P;Γn k : σk | ∙[E]

B@>l<@E@>l<@[B]P;Γ,𝑥(τ_1,n) n e : τ_2t | TSP[E]

B@>l<@E@>l<@[B]P;Γn λ𝑥τ_1.e : τ_1→τ_2λ𝑥τ_1'.t | TSP[E]

B@>l<@E@>l<@[B]P;Γn e_1 : τ_1→τ_2t_1 | TSP_1[E]
B@>l<@E@>l<@[B]P;Γn e_2 : τ_1t_2 | TSP_2[E]

B@>l<@E@>l<@[B]P;Γn e_1 e_2 : τ_2t_1 t_2 | TSP_1 ∪TSP_2[E]

B@>l<@E@>l<@[B]a ∉Γ[E]
B@>l<@E@>l<@[B]P;Γ,a n e : σt | TSP[E]

B@>l<@E@>l<@[B]P;Γn e : ∀a.σΛa.t | TSP[E]

B@>l<@E@>l<@[B]P;Γn e : ∀a.σt | TSP[E]

B@>l<@E@>l<@[B]P;Γn e : σ[τ/a]e ⟨τ^'⟩ | TSP[E]

B@>l<@E@>l<@[B]P;Γn+1 e : τt | TSP[E]

B@>l<@54@>l<@E@>l<@[B]P;Γn e : Code τ[54]
[54]t_TSP_n | ⌊TSP⌋^n[E]

B@>l<@E@>l<@[B]P;Γn-1 e : Code τt | TSP[E]
B@>l<@E@>l<@[B]𝖿𝗋𝖾𝗌𝗁 sp[E]

B@>l<@E@>l<@[B]P;Γn $(e) : τsp | {Δ⊢spτ^'=t} ∪_n-1TSP[E]

B@>l<@E@>l<@[B]P;Γ, ev(C,n) n e : ρt | TSP[E]
B@>l<@E@>l<@[B]𝖿𝗋𝖾𝗌𝗁 ev[E]

B@>l<@E@>l<@[B]P;Γn e : C⇒ρλevτ.t | TSP[E]

B@>l<@E@>l<@[B]P;Γn e : C⇒ρt_1 | TSP_1[E]
B@>l<@E@>l<@[B]P;ΓnCt_2 | TSP_2[E]

B@>l<@E@>l<@[B]P;Γn e : ρt_1 t_2 | TSP_1 ∪TSP_2[E]

Source Expression Typing with Elaboration Semantics

§.§.§ Levels

A large part of the rules are indexed by their (integer) level.
It is standard to index the expression judgement at a specific level but less
standard to index
the constraint entailment judgement. The purpose of
the level index is to ensure that expression variables and constraints
can only be used at the level they are introduced. The result is a program which
is separated into stages in such a way that when imbued with operational semantics,
the fragments at stage  will be evaluated before the fragments at stage .

The full program is checked at level .
Quotation ($\EQuote$) increases the level by one and splicing ($\ESplice$)
decreases the level.
It is permitted to reach negative levels in this source language.
The negative levels indicate a stage which should evaluate at compile-time.

In more detail, the consequence of the level-indexing is that:

* A variable can be introduced at any specific level  by a
$\lambda$-abstraction () and used at precisely that level ().

* Variables introduced by top-level definitions
can be used at any level ().

* Type variables can be introduced () and used at any level ().

* Constraints can be introduced at any level (), but in practice, due
to the system being predicative, this level will always be  (see
Section <ref>).
Constraints are also introduced into the program logic by instance declarations.
Constraints are appropriately eliminated by application ().
The entailment relation (Figure <ref>) ensures
that a constraint is available at the current stage.

Note that we do not allow implicit lifting as discussed in Section <ref>
and implemented in GHC. Explicit lifting via a  class can easily be expressed in
this language, and implicit lifting, if desired, can be orthogonally added as an additional
elaboration step.

The rules furthermore implement the top-level splice restriction present in GHC.
A top-level splice will require its body to be at level  and thereby rule out
the use of any variables defined outside of the splice, with the exception of
top-level variables.

§.§.§ Level of constraints

Inspecting the rule independently it would appear that a local
constraint can be introduced at any level and then be used at that level.
In fact, the rule can only ever be applied at level  because the rule requires that the enclosed expression has a  type. This forbids the
type as produced by and more closely models the restriction
to predicative types as present in GHC.

The new constraint form  can be used to allow local constraints
to be used at positive levels in . The rules and in constraint
entailment can convert from  and  and vice versa. During elaboration,
these rules will insert splices and quotes around the dictionary arguments as needed.

Constraints satisfied by instance declarations can be used at any level by means of .

Let us illustrate this by revisiting Example <ref> and considering the
expression . In this case, we assume the program environment to contain
the type of :
B@>l<@E@>l<@[B]P=∙,show∀a.Show a⇒a→String[E]
From this we can use to conclude that
B@>l<@E@>l<@[B]P;Γ1 show : ∀a.Show a⇒a→String[E]
Because  must have type  for some monotype , we cannot apply
yet, but must first apply and . We can conclude
B@>l<@E@>l<@[B]P;Γ1 show : a→String[E]
if the entailment
B@>l<@E@>l<@[B]P;Γ1Show a[E]
holds. As we do not assume any instances for  in this example, the constraint
can only be justified via the local environment . Because, as discussed above,
any constraint can only have been introduced at level , the only way to move a local
constraint from level  to level  is rule , which requires us to show
B@>l<@E@>l<@[B]P;Γ0CodeC (Show a)[E]
This in turn follows from if we assume that  contains :
B@>l<@E@>l<@[B]Γ=∙, 𝑥(CodeC (Show a),0)[E]
At this point, we know that
B@>l<@E@>l<@[B]P;Γ0 show : Code (a→String)[E]
and by applying and , we obtain
B@>l<@E@>l<@[B]P;∙0 show : ∀a.CodeC (Show a)⇒Code (a→String)[E]
as desired.

B@>l<@E@>l<@[B]P;ΓnCt | TSP[E]

B@>l<@E@>l<@[B]ev(∀a.C_i⇒C) ∈P[E]
B@>l<@E@>l<@[B]P;ΓnC_i[τ/a]t_i | TSP_i[E]

B@>l<@94@>l<@E@>l<@[B]P;ΓnC[τ/a]ev ⟨τ^'⟩ t_i | [94]

B@>l<@E@>l<@[B]ev (C,n) ∈Γ[E]

B@>l<@E@>l<@[B]P;ΓnCev | ∙[E]

B@>l<@E@>l<@[B]P;Γn+1Ct | TSP[E]

B@>l<@E@>l<@[B]P;ΓnCodeC Ct_TSP_n | ⌊TSP⌋^n[E]

B@>l<@E@>l<@[B]P;Γn-1CodeC Ct | TSP[E]
B@>l<@E@>l<@[B]𝖿𝗋𝖾𝗌𝗁 sp[E]

B@>l<@E@>l<@[B]P;ΓnCsp | {Δ⊢spτ=t} ∪_n-1TSP[E]

Source Constraints with Elaboration

§.§.§ Program Typing

A program (Figure <ref>) is a sequence of value, class and instances declarations followed by
an expression. The declaration forms extend the program theory which is used
to typecheck subsequent definitions. Value definitions extend the list of
top-level definitions available at all stages. The judgement makes it clear that
the top-level of the program is level  and that each expression is checked in
an empty local environment.

Class definitions extend the program theory with the qualified class method.
Instance definitions extend the environment with an axiom for the specific instance
which is being defined. The rule checks that the class method is of the type specified in the
class definition.

Notice that before the type class method is checked, the local environment  is
extended with an axiom for the instance we are currently checking. This is
important to allow recursive definitions (Example <ref>) to be defined in a natural fashion.
The constraint is introduced at level , the top-level of the program. It is important
to introduce the constraint to the local environment rather than program theory
because this constraint should not be available at negative levels.
If the constraint was introduced to the program theory, then it could be used
at negative levels, which would amount to attempting to use the instance
in order to affect the definition of said instance. This nuance in the typing
rules explains why Example <ref> is accepted and the necessity of the
constraint in Example <ref>.

B@>l<@E@>l<@[B]pgm | P⊢_𝖽𝖾𝖿def : Ppgm[E]

B@>l<@E@>l<@[B]P;∙0 e : σt | TSP[E]

B@>l<@E@>l<@[B]d=𝐝𝐞𝐟 k τ=t[E]

B@>l<@E@>l<@[B]pgm | P⊢_𝖽𝖾𝖿𝐝𝐞𝐟 k=e : P,kσds[E]

Source Definition Typing with Elaboration

B@>l<@E@>l<@[B]pgm | P⊢_𝖼𝗅𝗌cls : Ppgm[E]

B@>l<@E@>l<@[B]pgm | P⊢_𝖼𝗅𝗌 𝐜𝐥𝐚𝐬𝐬  TC a 𝐰𝐡𝐞𝐫𝐞 {1.5mu k::σ1.5mu} : P,k∀a.TC a⇒σpgm[E]

Source Class Typing with Elaboration

B@>l<@E@>l<@[B]pgm | P⊢_𝗂𝗇𝗌𝗍inst : Ppgm[E]

B@>l<@E@>l<@[B]𝐜𝐥𝐚𝐬𝐬  TC a 𝐰𝐡𝐞𝐫𝐞 {1.5mu k::σ1.5mu}[E]
B@>l<@E@>l<@[B]b95 j=𝖿𝗏(τ)[E]
[14]∙,b95 j⊢_𝖼𝗍C_iτ_i[E]

B@>l<@E@>l<@[B]P;∙,b95 j, ev(TC τ,0),(C_i,0) 0 e : σ[τ/a]t | TSP[E]

B@>l<@68@>l<@E@>l<@[B]dI=𝐝𝐞𝐟 ev (∀b95 j.τ_i→τ^')=[68]

B@>l<@E@>l<@[B]𝖿𝗋𝖾𝗌𝗁 ev[E]

B@>l<@E@>l<@[B]pgm | P⊢_𝗂𝗇𝗌𝗍 𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞  C_i⇒TC τ 𝐰𝐡𝐞𝐫𝐞 {1.5mu k=e1.5mu} : P, ev(∀b95 j.C_i⇒TC τ)ds[E]

Source Instance Typing with Elaboration

B@>l<@E@>l<@[B]P⊢_𝗉𝗀𝗆pgm : σpgm[E]

B@>l<@E@>l<@[B]P;∙0 e : σt | TSP[E]

B@>l<@E@>l<@[B]P⊢_𝗉𝗀𝗆e : σds[E]

B@>l<@E@>l<@[B]P_2⊢_𝗉𝗀𝗆pgm : σpgm[E]
B@>l<@E@>l<@[B]pgm | P_1⊢_𝖽𝖾𝖿def : P_2pgm_1[E]

B@>l<@E@>l<@[B]P_1⊢_𝗉𝗀𝗆def;pgm : σpgm_1[E]

B@>l<@E@>l<@[B]P_2⊢_𝗉𝗀𝗆pgm : σpgm[E]
B@>l<@E@>l<@[B]pgm | P_1⊢_𝖼𝗅𝗌cls : P_2pgm_2[E]

B@>l<@E@>l<@[B]P_1⊢_𝗉𝗀𝗆cls;pgm : σpgm_1[E]

B@>l<@E@>l<@[B]P_2⊢_𝗉𝗀𝗆pgm : σpgm[E]
B@>l<@E@>l<@[B]pgm | P_1⊢_𝗂𝗇𝗌𝗍inst : P_2pgm_1[E]

B@>l<@E@>l<@[B]P_1⊢_𝗉𝗀𝗆inst;pgm : σpgm_1[E]

Source Program Typing with Elaboration

B@>l<@E@>l<@[B]a ∈Γ[E]

B@>l<@E@>l<@[B]Γ⊢_𝗍𝗒Code τCode τ^'[E]

Source Type Formation with Elaboration

TODO: Constraint Formation with Elaboration is slightly different
I think this is ok.

B@>l<@E@>l<@[B]𝐜𝐥𝐚𝐬𝐬  TC a 𝐰𝐡𝐞𝐫𝐞 {1.5mu k::σ1.5mu}[E]

B@>l<@E@>l<@[B]Γ⊢_𝖼𝗍TC ττ^'[E]

B@>l<@E@>l<@[B]Γ⊢_𝖼𝗍CodeC CCode τ[E]

Source Constraint Formation with Elaboration

This is going to be controversial, but I'm dropping the separate
examples section tentatively for the integrated E1 reprisal which can
probably be shortened further. I don't see the second one as sufficiently

§ THE CORE LANGUAGE

In this section we describe an explicitly typed core language which is suitable
as a compilation target for the declarative source language we described in
the Section <ref>.

§.§ Syntax

The syntax for the core language is presented in Figure <ref>.
It is a variant of the explicit polymorphic lambda calculus with
multi-stage constructs, top-level definitions and
top-level splice definitions.

Quotes and splices are represented by the syntactic form , which
is a quotation with an associated splice environment which binds splice variables
for each splice point within the quoted expression. A splice point is
where the result of evaluating a splice will be inserted. Splice variables to represent
the splice points are bound
by splice environments and top-level splice definitions. The expression syntax contains
no splices, splices are modelled using the splice environments which are attached
to quotations and top-level splice definitions.

The splice environment maps a splice point  to a local type
environment , a type  and an expression  which we write as
$\Delta \vdash sp \colonT \tau = e$. The typing rules will ensure that the
expression  has type . The purpose of the environment  is
to support open code representations which lose their lexical scoping when lifted
from the quotation.

A top-level splice definition is used to support elaborating from negative levels
in the source language. These top level declarations are of
the form  which indicates that the expression
will have type  at level  in environment . Top-level splice
definitions also explicitly record the level of the original splice so that
the declaration can be typechecked at the correct level. The level index is not
necessary for the quotation splice environments because the level of the whole environment
is fixed by the level at which the quotation appears.

§.§ Typing Rules

The expression typing rules for the core language are for the most part the
same as those in the source language. The rules that differ are shown in Figure <ref>.

The splice environment typing rules are given in Figure <ref>.
A splice environment is well-typed if each of its definitions is well-typed.
We check that the body of each definition has type  in an environment extended
by . In the rule, the body of the quotation is checked in an environment

extended with the contents of the splice environment. A splice variable  is associated
with an environment , a type  and a level  in
When a splice variable is used, the rule ensures that the claimed local
environment aligns with the actual environment, the type of the variable is correct
and the level matches the surrounding context.

Top-level splice definitions are typed in a similar manner in Figure <ref>.
The body of the definition is checked to have type
at level  in environment , the
program theory is then extended with a splice variable
which can be used in the remainder of the program.

§.§ Dynamic Semantics

It would be good to actually refer to the Figures from here.

The introduction of splice environments makes the evaluation order of
the core calculus evident and hence a suitable target for compilation.

Usually in order to ensure a well-staged evaluation order, the reduction relation
must be level-indexed to evaluate splices inside quotations. In our calculus,
there is no need to do this because the splices have already been lifted outside
of the quotation during the elaboration process. This style is less convenient
to program with, but easy to reason about and implement.

In realistic implementations, the quotations are compiled to a representation form
for which implementing substitution can be difficult. By lifting the splices outside
of the representation, the representation does not need to be inspected or
traversed before it is spliced back into the program. The representation can
be treated in an opaque manner which gives us more implementation freedom about
its form.
In our calculus this is evidenced by the fact there is no reduction rule which
reduces inside a quotation.

The program evaluation semantics evaluate each declaration in turn from top to
bottom. Top-level definitions are evaluated to values and substituted into the
rest of the program. Top-level splice definitions are evaluated to a value of
type  which has the form .
The splice variable is bound to the value  with the substitution  applied
and then substituted into the remainder of the program.

Using splice environments and top-level splice definitions is reminiscent of the approach taken in logically inspired
languages by <cit.> and <cit.>.

§.§ Module Restriction

In GHC, the module restriction dictates that only identifiers bound in other
modules can be used inside top-level splices. This restriction is modelled in
our calculus by the restriction that only identifiers previously bound in
top-level definitions can be used inside a top-level splice. The intention
is therefore to consider each top-level definition to be defined in its
own “module” which is completely evaluated before moving onto the next definition.

This reflects the situation in a compiler such as GHC which supports separate
compilation. When compiling a program which uses multiple modules,
one module may contain a top-level splice which is then used inside another
top-level splice in a different module. Although syntactically both top-level
splices occur at level , they effectively occur at different stages.
In the same way as different modules occur at different stages due to separate
compilation, in our calculus, each top-level definition can be considered to
be evaluated at a new stage.

At this point it is worthwhile to consider what exactly we mean by compile-time
and run-time. So far we have stated that the intention is for splices at negative
levels to represent compile-time evaluation so we should state how we intend
this statement to be understood in our formalism. The elaboration procedure
will elaborate each top-level definition to zero or more splice definitions
(one for each top-level splice it contains) followed by a normal value definition.
Then, during the evaluation of the core program the splice definitions will be evaluated
prior to the top-level definition that originally contained them.

The meaning of “compile-time” is therefore that the evaluation of the top-level
splice happens before the top-level definition is evaluated. It is also possible
to imagine a semantics which partially evaluates a program to a residual by
computing and removing as many splice definitions as possible.

If we were to more precisely model a module as a collection of definitions then
the typing rules could be modified to only allow definitions from previously
defined modules to be used at the top-level and all splice definitions could be
grouped together at the start of a module definition before any of the value definitions.
Then it would be clearly possible to evaluate all of the splice definitions for
a module before commencing to evaluate the module definitions.

[24]𝐝𝐞𝐟 k τ=e [E]

[24]𝐬𝐩𝐝𝐞𝐟 Δnsp τ=e [E]

[157]  [157E]

[19] [19E]
[157]  [157E]

[24]λ𝑥τ.e|e e[157]
[157]  [157E]

[24]Λa.e|e ⟨τ⟩[157]
[157]  [157E]

[157]  [157E]
[157]  [157E]
[157]  [157E]

[19] [19E]
[157]  [157E]

[157]  [157E]

[24]Code τ[157]
[157]  [157E]

[157]  [157E]
[162]  [162E]
[162]  [162E]
Core Language Syntax

B@>l<@E@>l<@[B]P;Γn e : τ[E]

B@>l<@E@>l<@[B]Δ⊢sp(τ,n) ∈Γ[E]

B@>l<@E@>l<@[B]P;Γn sp : τ[E]

B@>l<@E@>l<@[B]sp(Δ,τ) ∈P[E]

B@>l<@E@>l<@[B]P;Γn sp : τ[E]

B@>l<@E@>l<@[B]P;Γ,a n e : τ[E]

B@>l<@E@>l<@[B]P;Γn Λa.e : ∀a.τ[E]

B@>l<@E@>l<@[B]P;Γn e : ∀a.τ_2[E]

B@>l<@E@>l<@[B]P;Γn e ⟨τ_1⟩: τ_2[τ_1/a][E]

B@>l<@E@>l<@[B]P;Γ, sp_i (Δ_i, τ_i, n+1) n+1 e : τ[E]
B@>l<@E@>l<@[B]SP=Δ_i ⊢sp_i τ_i=e_i[E]

B@>l<@E@>l<@[B]P;Γn e_SP : Code τ[E]

Core Expression Typing

B@>l<@E@>l<@[B]P;Γ,Δn e : Code τ[E]

Splice Environment Typing

B@>l<@E@>l<@[B]P;∙0 e : τ[E]

B@>l<@E@>l<@[B]P⊢_𝖽𝖾𝖿𝐝𝐞𝐟 k τ=e:P,kτ[E]

B@>l<@E@>l<@[B]P;Γn e : Code τ[E]

B@>l<@E@>l<@[B]P⊢_𝗌𝗉𝖽𝖾𝖿𝐬𝐩𝐝𝐞𝐟 Γnsp τ=e:P,sp(Γ,τ)[E]

Core Definition Typing

B@>l<@E@>l<@[B]P;∙0 e : τ[E]

Core Program Typing

B@>l<@E@>l<@[B]e_1 e_2e_1' e_2[E]

B@>l<@E@>l<@[B]e_1 e_2e_1 e_2'[E]

B@>l<@E@>l<@[B](λ𝑥τ.e) ve[v/𝑥][E]

B@>l<@E@>l<@[B]e ⟨τ⟩e' ⟨τ⟩[E]

B@>l<@E@>l<@[B](Λa.e) ⟨τ⟩e[τ/a][E]

Dynamic Semantics

Dynamic Semantics for Splice Environment

B@>l<@E@>l<@[B]𝐝𝐞𝐟 k τ=e𝐝𝐞𝐟 k τ=e'[E]

B@>l<@E@>l<@[B]𝐬𝐩𝐝𝐞𝐟 Γnsp τ=e𝐬𝐩𝐝𝐞𝐟 Γnsp τ=e'[E]

Dynamic Semantics for Definitions

B@>l<@E@>l<@[B]𝐝𝐞𝐟 k τ=v;pgmpgm[v/k][E]

B@>l<@E@>l<@[B]𝐬𝐩𝐝𝐞𝐟 Δnsp τ=e_SP;pgmpgm[e[SP]/sp][E]

Dynamic Semantics for Program

§ ELABORATION

In this section we describe the process of elaboration from the source language
to the core language. Elaboration starts from a well-typed term
in the source language and hence is defined by induction
over the typing derivation tree (Figure <ref>).

§.§ Elaboration procedure

There are three key aspects of the elaboration procedure:
Add figure references

* Splices at positive levels are removed in favour of a splice environment. The elaboration process returns
a splice environment which is attached to the quotation form.

* Splices at non-positive levels are elaborated to top-level splice definitions, which are bound
prior to the expression within which they were originally contained.

* Type class constraints are converted to explicit dictionary passing. We describe how to
understand the new constraint form  in terms of quotation.

In order to support elaboration, all implicit evidence from
the program theory and local environment are annotated with variables. The idea
is that in the elaborated program, the evidence for each particular construct will
be bound to a variable of that name. Top-level evidence by top-level variables and
local evidence by $\lambda$-bound variables. The modifications to the
typing rules for the source language syntax necessary in order to explain
elaboration are highlighted by a grey box.

[23]∙|Γ,𝑥(τ,n)|Γ,a|Γ, ev(C,n)[127]
[127]   [132]

[23]∙|P, ev(∀a.C⇒C)|P,kσ[127]
[127]  [132]

The judgement  states
that in program theory  and environment , the expression  has type
at level  and elaborates to term  whilst producing splices .

§.§ Splice Elaboration

The  is a function from a level to a splice environment .
In many rules, we perform level-pointwise union of produced splices,
written $\cup$.

Do we need a more formal description in a figure or as an equation? Perhaps not.
During elaboration, all splices are initially added to the  at
the level of their contents, so a splice that occurs at level  is added
at level  by means of the operation $\cup_{n-1}$ as in rule .

What happens with the splices contained in the  depends on their
level. If they occur at a positive level, they will be bound by a surrounding
quotation in rule . The notation  denotes the
projection of the splices contained in  at level . They become part
of the splice environment associated with the quotation. Via ,
we then truncate  so that it is empty at level  and above.

If a splice
occurs at non-positive level, it is a top-level splice and will become a top-level
splice definition in rules or , in such a way that the splice definitions
are made prior to the value definition which yielded them.
The splice definitions are created by the  judgement (Figure <ref>), which
takes a splice environment returned by the expression elaboration judgement and
creates top-level splice declarations for each negative splice which appeared inside a term.
To guarantee a stage-correct
execution, the splices are inserted in order of their level.

We maintain the invariant on the  where it only contains
splices of levels prior to the current level of the judgement. Therefore,
when the judgement level decreases as in , the splices for that level
are removed from the splice environment and bound at the quotation.
As the top-level of the program is at level , the splice environment
returned by an elaboration judgement at level  will only contain splices at negative
levels, which is why the appeal to the  function starts from level .

§.§ Constraint Elaboration

The second point of interest are the constraint elaboration rules given in
Figure <ref>. Since in our language type classes have just
a single method, we use the function corresponding to the method itself
as evidence for a class instance in rule .

Constraints of the new constraint form
are elaborated into values of type . Therefore
inspecting the entailment elaboration form and must be understood
in terms of quotation. The entailment rule is implemented by a simple
quotation and thus similar to . The rule is conceptually implemented using a splice, but
as the core language does not contain splices it is understood by adding a new definition
to the splice environment, which mirrors . These rules explains the necessity of
level-indexing constraints in the source language; the elaboration would not
be well-staged if the stage discipline was not enforced.

The remainder of the elaboration semantics which elaborate the simple terms and
constraint forms are fairly routine.

§.§ Example

As an example of elaboration, let us consider the expression
where  from Example <ref>. There are two points of interest
here: there is a top-level splice which will be floated to a top-level splice definition,
and the  constraint of  must be elaborated into quoted evidence
using rule .

We assume that the program environment contains :
B@>l<@E@>l<@[B]P=∙,c_1'∀a.CodeC (Show a)⇒Code (a→String)[E]
As our program comprises a single main expression, we have to use rule . This rule
requires us to first elaborate the expression itself at level  in an empty type environment. We obtain
B@>l<@E@>l<@[B]P;∙0 $(c_1') : ∀a.Show a⇒a→String[E]

[B]  Λa.λeva→String.sp | {Δ⊢spa→String=c_1' ⟨a⟩ ev_∙} ∪_-1∙[E]
The splice point  has been introduced for the splice via rule .
Evidence for the  constraint is introduced into the type environment at level
via rule . It is captured in  for use in the splice. Because the use of
the evidence occurs at level  and the required constraint is , rule is used to quote the evidence. The splice environment attached to the quote is empty,
because there are no further splices.

Back to rule , we furthermore obtain that the resulting main expression is of the form
The type of  results from elaborating the original  constraint to the type of its method
via the rule . We can now look at  and observe that it will extract the one splice
at level  passed to it into a top-level splice definition that ends up before , the result
B@>l<@E@>l<@[B]𝐬𝐩𝐝𝐞𝐟 Δ-1sp a→String=c_1' ⟨a⟩ ev_∙;p[E]

The operational semantics for the language evaluates the definition of
first to a quotation before the quoted expression is substituted into the remainder
of the program so that evaluation can continue.

B@>l<@E@>l<@[B]ds=collapse(n-1,⌊TSP⌋^n,spdef95 i;pgm)[E]
B@>l<@E@>l<@[B]spdef95 i=𝐬𝐩𝐝𝐞𝐟 Δ_i nsp_i τ_i=e_i[E]

B@>l<@E@>l<@[B]TSP_n=Δ_i ⊢sp_i τ_i=e_i[E]

Definition of $collapse$

B@>l<@E@>l<@[B]Γ, ev(C,n)Δ,ev(τ,n)[E]

Elaboration of Type Environments

§ PRAGMATIC CONSIDERATIONS

Now that the formal developments are complete and the relationship between the
source language and core language has been established by the elaboration
semantics, it is time to consider how our formalism interacts with
other language extensions, and to discuss implementation issues.

§.§ Integration into GHC

The implementation and integration of this specification into GHC's
sophisticated architecture naturally requires certain design decisions to be
made, which we now discuss.

I have removed the para talking about the fact that typed quotations and the frontend need to be modified. I think that's quite obvious to anybody reading this paper!

§.§.§ Type Inference

Type inference for our new constraint form should be straightforward to integrate
into the constraint solving algorithm used in GHC <cit.>.
The key modification is to keep track of the level of constraints and only solve goals with
evidence at the right level. If there is no evidence available for a constraint at
the correct level, then either the or rule can be invoked
in order to correct the level of necessary evidence.

I do not understand the following sentence.
me neither
Are we advocating the removal of this sentence or rewording? The point
is supposed to be that if you need to generalise at level 0 and require a constraint at
level 1 you should generate a  constraint rather than
commented out

§.§.§ Substituting Types

Substituting inside quotations poses some implementation challenges depending on the
quotation representation.

In previous implementations which used low-level
representations to represent quotations <cit.>
the solution was to maintain a separate environment for free variables which can
be substituted into without having to implement substitution in terms of the low-level
representation. The idea is then that by the time the low-level representation is evaluated
all the variables bound in the environment are already added to the environment and
so computation can proceed as normal when it encounters what was previously a free variable.

Therefore we should treat every free type variable in a quotation as a splice
point, create an environment to attach to the quotation which maps the splice
point to the variable of the name and then when the quotation is interpreted
substitute the type into the quotation.

§.§.§ Erasing Types

The operational semantics of System F do not depend on the type information and
so the types can be erased before
evaluation. It is this observation that leads us to accept Example <ref>.
However, there is another
point in the design space – we could have elaborated to an erased version of System
F where types were replaced by placeholders. This would
save us the complications of having to substitute types inside quotations.
However, the option of maintaining the type information is
important for practical purposes. GHC has an optional internal typechecking phase
called core lint which verifies the correctness of code generation and optimisation, it
would be a shame to lose this pass in any program which used metaprogramming.
In a language where the type information dwarfs the runtime content of terms,
it would be desirable to also explore the option to store erased or partially erased
terms <cit.>.

§.§.§ Cross-Stage Persistence

Earlier work on cross-stage persistence <cit.> has

that implementing cross-stage persistence for instance dictionaries should
be possible because a dictionary was ultimately a collection of top-level functions
so some special logic could be implemented in the compiler to lift a dictionary.

Or perhaps even more drastically, a dictionary embedded into a GADT?
Yes, but not sure how to weave that in

Additional complexity arises when functions with
local constraints are passed an arbitrary dictionary which could have been
constructed from other dictionaries, which in turn come from dictionaries. At
the point the dictionary is passed, the required information about its
structure has been lost so it is
impossible to interpret into a future stage.
A solution to this could be to use a different evidence form which passes the
derivation tree for a constraint to a function as evidence before the function
constructs the required dictionary at the required stage. This would increase
the runtime overhead of using type classes and would not be practical to implement.

§.§ Interaction with Existing Features

So far we have considered how metaprogramming interacts with qualified types,
but of course there are other features that are specific to GHC that need to be considered.

§.§.§ GADTs

Local constraints can be introduced by pattern matching on a GADT.
For simplicity our calculus did not include GADTs or local constraints but
they require similar treatment to other constraints introduced locally. The
constraint solver needs to keep track of the level that a GADT pattern
match introduces a constraint and ensure that the constraint is only used at
that level.

Note that this notion of a “level” is the stage of program execution where the
constraint is introduced and not the same idea of a level the constraint solver
uses to prevent existentially quantified type variables escaping their scope.
Each nested implication constraint increases the level so type variables
introduced in an inner scope are forbidden from unifying with type variables
which are introduced at a previous level.
Cite? http://okmij.org/ftp/ML/generalization.html

§.§.§ Quantified Constraints

The quantified constraints extension <cit.>
relaxes the form of the constraint schemes
allowed in method contexts to also allow the quantified and implication forms
which in our calculus are restricted to top-level axioms. Under this restriction
there are some questions about how the  constraint form should
interact especially with implication constraints. In particular, whether
constraint entailment should deduce that  entails
or the inverse and what consequences this has for
type inference involving these more complicated constraint forms.

§.§ Interaction with Future Features

GHC is constantly being improved and extended to encompass new and ambitious
and so we consider how metaprogramming should interact with features that are
currently in the pipeline.

§.§.§ Impredicativity

For a number of the examples that we have discussed in this paper,
an alternative would be to use impredicative instantiation to more
precisely express the binding position of a constraint.
For instance, the function  from Example <ref> might instead have been expressed in the following manner:
B@>l<@E@>l<@[B]c_1'::Code (∀a.Show a⇒a→String)[E]

The type of  now binds and uses the  constraint at level $1$ without the use of .

However, despite many attempts <cit.>, GHC has never properly
supported impredicative instantiation due to complications with type
Recent work <cit.> has
proposed the inclusion of restricted impredicative instantiations,
and these would accept .
In any case, impredicativity is not a silver bullet, and there is still a need for
the  constraint form. Without the  constraint
form there is no way to manipulate “open” constraints. That is, constraints which
elaborate to quotations containing free variables.

I'm not sure if I concretely get what you mean by “open” constraints.
In my mind, the primary need for  arises from anything that abstracts
over constraints. E.g. classes might need  as instance context. Or
from generics-sop.

Experience has taught us that writing code generators which manipulate open
terms is a lot more convenient than working with only closed terms. We predict
that the same will be true of working with the delayed constraint form as well.
In particular, features such as super classes, instance contexts and type families
can be used naturally with  constraints.
So whilst relaxing the impredicativity restriction will have some positive
consequences to the users of Typed Template Haskell, it does not supersede our
design but rather acts as a supplement.

Would be good to show an example of this specifically here

§.§.§ Dependent Haskell

Our treatment of type variables is inspired by the in-built phase distinction
of System F. As Haskell barrels at an impressive rate to a dependently
typed language <cit.>,
the guarantees of the phase distinction will be lost in some
cases. At this point it will be necessary to revise the specification in order
to account for the richer phase structure.

The specification for Dependent Haskell <cit.> introduces
the so-called relevance quantifier in order to distinguish between relevant and
irrelevant variables. The irrelevant quantifier is intended to model a form
of parametric polymorphism like the $\forall$ in System F, the relevant quantifier
is written as $\Pi$ after the dependent quantifier from dependent type theory.

Perhaps it is sound to modify their system in order to enforce the stage discipline
for relevant type variables not irrelevant ones. It may be that the
concept of relevance should be framed in terms of stages,
where the irrelevant stage
proceeds all relevant and computation stages – in which case it might be
desirable to separate the irrelevant stage itself into multiple stages
which can be evaluated in turn.
The exact nature of this interaction is left as a question for future work.

§ RELATED WORK

Multi-stage languages with explicit staging annotations were first suggested
by <cit.>. Since then there has been a reasonable amount of theoretical
interest in the topic which has renewed in recent years. There are several practical
implementations of multi-stage constructs in mainstream programming languages
such as BER MetaOCaml <cit.>, Typed Template Haskell and
Dotty <cit.>.

reference other formalisms of MetaML? <cit.> <cit.>

At a first glance there is surprisingly little work which attempts to reconcile
multi-stage programming with language features which include polymorphism. Most
presented multi-staged calculi are simply typed despite the fact that
all the languages which practically implement these features support polymorphism.
The closest formalism is by <cit.> who consider
a language with polymorphism and control effects. Their calculus is presented
without explicit type abstraction and application. There
is no discussion about cross-stage type variable references or qualified types
and their primary concern, similar to <cit.> is the interaction of the
value restriction and staging. Our calculus in contrast, as it models
Haskell, does not contain any effects so we have concentrated on qualified types.
<cit.> present a similar ML-like language with

Combining together dependent types and multi-stage features is a more common
combination. The phase distinction is lost in most dependently typed languages
as the typechecking phase involves evaluating expressions. Therefore in order
to ensure a staged evaluation, type variables must also obey the same
stage discipline as value variables. This is the approach taken by <cit.>.
<cit.> defines the dependently-typed multi-stage language Meta-D
but doesn't consider constraints or parametric polymorphism. Concoqtion <cit.> is an
extension to MetaOCaml where Coq terms appear in types. The
languge is based on $\lambda_{H\bigcirc}$ <cit.> which includes
dependent types but is motivated by removing tags in the generated program.
<cit.> observe similarly that it is worthwhile to combine together
depedent types and multi-stage programming to turn a well-typed interpreter
into a verified compiler. The language presented does not consider parametric
polymorphism nor constraints.

We are not aware of any prior work which considers the implications of relevant
implicit arguments formally, although there is an informal characterization by <cit.>.

Formalising Template Haskell
With regards to formalisms of Template Haskell, a brief description of
Untyped Template Haskell is given by <cit.>. The language
is simply-typed and does not account for multiple levels. The language has also
diverged since their formalism as untyped quotations are no longer typechecked
before being converted into their representation. Their formalism does
account for the  monad which provides operations that allow a
programmer to “reify” types, declarations and so on in order to inspect the internal
structure. These are typically used in untyped Template Haskell in order to
generically define instances or other operations.

It is less common to use the reification functions in Typed Template Haskell programs and
so we have avoided their inclusion in our formalism for the sake of simplicity.
In our calculus we wanted to precisely understand the basic interaction between
constraints and quotations, and the existence of the  monad is orthogonal to this.

Code generators are typically effectful in order to support operations such as
let insertion or report errors so it is an important question to define a
calculus with effects. From GHC 8.12, the type of quotations will be generalised <cit.>
from  to a minimal interface  so a user will
have more control over which effects they are allowed to use in their code
generators. We leave formalising this extension open to future work.

Metaprogramming In GHC

GHC implements many different forms of metaprogramming from the principled
to the ad-hoc. At the principled end of the spectrum in a similar vein
as Typed Template Haskell there is Cloud Haskell <cit.>, which
implements a modality for distributed computing. Another popular principled style
is generic programming <cit.> which allows the representation of datatypes to be
inspected and interpreted at runtime. Untyped Template Haskell
is used for untyped code generation in the combinator style. As well as generating
expressions it can be used to generate patterns, declarations and types. Programs
are typechecked after being generated rather than typechecking the generators
as in Typed Template Haskell. Untyped Template Haskell has a limited interface
into the typechecker but Source Plugins <cit.> allow
unfettered access to the internal state and operations of the typechecker and other
compiler phases.

Modal Type Systems

Type systems motivated by modal logics have more commonly
contemplated the interaction of modal operators and polymorphism. In particular
attention has turned recently to investigating dependent modal type
theories and the complex interaction of modal operators in such theories <cit.>. It
seems probable that ideas from this line of research can give a formal account of the interaction
of the code modality <cit.> and the parametric quantification from System F which
can also be regarded as a modality <cit.>.

In recent times, Fitch-Style Modal calculi <cit.> have become a popular way of specifying
a modal type system due to their good computational properties. It would
be interesting future work to attempt to modify our core calculus to a Fitch-Style
system which was not level indexed. In particular the calculus for Simple RaTT <cit.>
looks like a good starting point.

In short, we are sure there is a lot to learn from the vast amount of literature
on modal type systems but we are not experts in this field and the literature
does not deal with our practical concerns regarding implementing and writing
programs in staged programming languages. The goal of this paper was not to uncover a
logically inspired programming language but to give a practical and understandable
practical specification which can be understood by people without extensive
background in modal type theories.

§ CONCLUSION

Now that we have presented the first formalism of Typed Template Haskell,
the way is clear for future researchers to understand and extend the basic system.
We envisage that the system will be useful for two different communities.
Firstly, researchers into extensions such as Linear Haskell <cit.>
and Dependent Haskell <cit.>
now have the possibility to consider how their features interact with stages so that the language
remains sound with respect to staged evaluation.
Secondly, users interested in
multi-stage programming now have a firmer foundation to base further extensions to
the multi-stage features in GHC.

In the long-term our hope is to make multi-stage programming a more popular
and accessible
paradigm for functional programmers. Even with the present implementation of
Typed Template Haskell, <cit.>
have shown how different features implemented in GHC can be used together in
order to express elegant code generators.
We anticipate that a firm foundation for Typed Template Haskell that supports
finer control over the type of qualified constraints will
enable more practitioners to explore this unexplored territory,
and begin to reach for staging as a useful tool in their toolbox of techniques
to enhance the predictability and performance of their code.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Bahr, Graulund, and MøgelbergBahr
et al2019]
authorpersonPatrick Bahr,
personChristian Uldal Graulund, and
personRasmus Ejlers Møgelberg.
Simply RaTT: A Fitch-Style Modal Calculus for
Reactive Programming without Space Leaks.
journalProc. ACM Program. Lang.
volume3, numberICFP, Article articleno109
(dateJuly year2019), numpages27 pages.

[Bernardy, Boespflug, Newton, Peyton Jones, and
SpiwackBernardy et al2017]
authorpersonJean-Philippe Bernardy,
personMathieu Boespflug, personRyan R. Newton,
personSimon Peyton Jones, and personArnaud
Spiwack. year2017.
Linear Haskell: Practical Linearity in a
Higher-Order Polymorphic Language.
journalProc. ACM Program. Lang.
volume2, numberPOPL, Article articleno5
(dateDec. year2017), numpages29 pages.

[Bottu, Karachalias, Schrijvers, Oliveira, and
WadlerBottu et al2017]
authorpersonGert-Jan Bottu, personGeorgios
Karachalias, personTom Schrijvers, personBruno C.
d. S. Oliveira, and personPhilip Wadler.
Quantified Class Constraints. In
booktitleProceedings of the 10th ACM SIGPLAN International
Symposium on Haskell (Oxford, UK) (seriesHaskell 2017).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages148–161.

[Brady and HammondBrady and Hammond2006]
authorpersonEdwin Brady and personKevin
Hammond. year2006.
A Verified Staged Interpreter is a Verified
Compiler. In booktitleProceedings of the 5th International
Conference on Generative Programming and Component Engineering (Portland,
Oregon, USA) (seriesGPCE ’06).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages111–120.

[Brady, McBride, and McKinnaBrady
et al2003]
authorpersonEdwin Brady, personConor
McBride, and personJames McKinna.
Inductive families need not store their indices.
In booktitleInternational Workshop on Types for Proofs and
Programs. Springer, pages115–129.

[Calcagno, Taha, Huang, and LeroyCalcagno
et al2003]
authorpersonCristiano Calcagno, personWalid
Taha, personLiwen Huang, and personXavier Leroy.
Implementing multi-stage languages using ASTs,
Gensym, and reflection. In booktitleProceedings of the 2nd
international conference on Generative programming and component
engineering (Erfurt Germany) (seriesGPCE03).
publisherAssociation for Computing Machinery,

authorpersonLuca Cardelli.
titlePhase distinctions in type theory.
Unpublish Manuscript.

[Chakravarty, Keller, and
Peyton JonesChakravarty et al2005]
authorpersonManuel M. T. Chakravarty,
personGabriele Keller, and personSimon
Peyton Jones. year2005.
Associated Type Synonyms.
journalSIGPLAN Not. volume40,
number9 (dateSept. year2005),

authorpersonRanald Clouston.
Fitch-style modal lambda calculi. In
booktitleInternational Conference on Foundations of Software
Science and Computation Structures. Springer, pages258–275.

[Davies and PfenningDavies and
authorpersonRowan Davies and personFrank
Pfenning. year2001.
A Modal Analysis of Staged Computation.
journalJ. ACM volume48,
number3 (dateMay year2001),

authorpersonRichard A Eisenberg.
booktitleDependent types in Haskell: Theory and
publisherUniversity of Pennsylvania.

[Epstein, Black, and Peyton JonesEpstein
et al2011]
authorpersonJeff Epstein, personAndrew P.
Black, and personSimon Peyton Jones.
Towards Haskell in the Cloud. In
booktitleProceedings of the 4th ACM Symposium on Haskell
(Tokyo, Japan) (seriesHaskell '11).
publisherACM, addressNew York, NY, USA,

[Fogarty, Pasalic, Siek, and TahaFogarty
et al2007]
authorpersonSeth Fogarty, personEmir
Pasalic, personJeremy Siek, and personWalid Taha.
Concoqtion: Indexed Types Now!. In
booktitleProceedings of the 2007 ACM SIGPLAN Symposium on
Partial Evaluation and Semantics-Based Program Manipulation (Nice, France)
(seriesPEPM ’07). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Gratzer, Kavvos, Nuyts, and BirkedalGratzer
et al2020]
authorpersonDaniel Gratzer, personGA
Kavvos, personAndreas Nuyts, and personLars
Birkedal. year2020.
titleMultimodal Dependent Type Theory.
In submission.

[Gratzer, Sterling, and BirkedalGratzer
et al2019]
authorpersonDaniel Gratzer, personJonathan
Sterling, and personLars Birkedal.
Implementing a Modal Dependent Type Theory.
journalProc. ACM Program. Lang.
volume3, numberICFP, Article articleno107
(dateJuly year2019), numpages29 pages.

authorpersonAdam Gundry.
titleType inference, Haskell and dependent types.
thesistypePh.D. Dissertation. schoolUniversity
of Strathclyde.

[Hall, Hammond, Peyton Jones, and
WadlerHall et al1996]
authorpersonCordelia V. Hall, personKevin
Hammond, personSimon L. Peyton Jones, and
personPhilip Wadler. year1996.
Type Classes in Haskell.
journalACM Trans. Program. Lang. Syst.
volume18, number2 (year1996),

[Jay and Peyton JonesJay and
Peyton Jones2008]
authorpersonBarry Jay and personSimon
Peyton Jones. year2008.
Scrap your type applications. In
booktitleInternational Conference on Mathematics of Program
Construction. Springer, pages2–27.

[Jonnalagedda, Coppey, Stucki, Rompf, and
OderskyJonnalagedda et al2014]
authorpersonManohar Jonnalagedda,
personThierry Coppey, personSandro Stucki,
personTiark Rompf, and personMartin Odersky.
Staged Parser Combinators for Efficient Data
Processing. In booktitleProceedings of the 2014 ACM
International Conference on Object Oriented Programming Systems Languages &
Applications (Portland, Oregon, USA) (seriesOOPSLA
’14). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages637–653.

[Kawata and IgarashiKawata and
authorpersonAkira Kawata and personAtsushi
Igarashi. year2019.
A Dependently Typed Multi-stage Calculus. In
booktitleAsian Symposium on Programming Languages and
Systems. Springer, pages53–72.

authorpersonOleg Kiselyov.
The Design and Implementation of BER MetaOCaml. In
booktitleFunctional and Logic Programming,
editorpersonMichael Codish and
personEijiro Sumii (Eds.). publisherSpringer
International Publishing, addressCham, pages86–102.

authorpersonOleg Kiselyov.
Generating Code with Polymorphic let: A Ballad of
Value Restriction, Copying and Sharing.
journalElectronic Proceedings in Theoretical
Computer Science  volume241 (dateFeb
year2017), pages1–22.

authorpersonOleg Kiselyov.
Reconciling Abstraction with High Performance: A
MetaOCaml approach.
journalFoundations and Trends in Programming
Languages volume5, number1 (year2018),

[Kokaji and KameyamaKokaji and
authorpersonYuichiro Kokaji and
personYukiyoshi Kameyama. year2011.
Polymorphic multi-stage language with control
effects. In booktitleAsian Symposium on Programming
Languages and Systems. Springer, pages105–120.

[Krishnaswami and YallopKrishnaswami and
authorpersonNeelakantan R. Krishnaswami and
personJeremy Yallop. year2019.
A Typed, Algebraic Approach to Parsing. In
booktitleProceedings of the 40th ACM SIGPLAN Conference on
Programming Language Design and Implementation (Phoenix, AZ, USA)
(seriesPLDI 2019). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Magalhães, Dijkstra, Jeuring, and
LöhMagalhães et al2010]
authorpersonJosé Pedro Magalhães,
personAtze Dijkstra, personJohan Jeuring, and
personAndres Löh. year2010.
A Generic Deriving Mechanism for Haskell. In
booktitleProceedings of the Third ACM Haskell Symposium on
Haskell (Baltimore, Maryland, USA) (seriesHaskell
’10). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages37–48.

authorpersonAleksandar Nanevski.
Meta-Programming with Names and Necessity.
(year2002), pages206–217.

[Nuyts and DevrieseNuyts and
authorpersonAndreas Nuyts and
personDominique Devriese. year2018.
Degrees of Relatedness: A Unified Framework for
Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and
Algebra in Dependent Type Theory. In booktitleProceedings
of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Oxford,
United Kingdom) (seriesLICS ’18).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages779–788.

authorpersonEmir Pašalic.
titleThe role of type equality in
thesistypePh.D. Dissertation. schoolOGI School
of Science & Engineering at OHSU.

[Pašalic, Taha, and SheardPašalic
et al2002]
authorpersonEmir Pašalic, personWalid
Taha, and personTim Sheard. year2002.
Tagless Staged Interpreters for Typed Languages.
In booktitleProceedings of the Seventh ACM SIGPLAN
International Conference on Functional Programming (Pittsburgh, PA, USA)
(seriesICFP ’02). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Peyton Jones, Jones, and MeijerPeyton Jones
et al1997]
authorpersonSimon Peyton Jones, personMark
Jones, and personErik Meijer.
Type classes: an exploration of the design space.
In booktitleHaskell Workshop.

[Peyton Jones, Vytiniotis, Weirich, and
ShieldsPeyton Jones et al2007]
authorpersonSimon Peyton Jones,
personDimitrios Vytiniotis, personStephanie Weirich,
and personMark Shields. year2007.
Practical Type Inference for Arbitrary-Rank Types.
journalJ. Funct. Program. volume17,
number1 (dateJan. year2007),

authorpersonFrank Pfenning.
Intensionality, extensionality, and proof
irrelevance in modal type theory. In booktitleProceedings
16th Annual IEEE Symposium on Logic in Computer Science. IEEE,

authorpersonMatthew Pickering.
titleOverloaded Quotations. GHC proposal.

[Pickering, Wu, and KissPickering
et al2019a]
authorpersonMatthew Pickering, personNicolas
Wu, and personCsongor Kiss. year2019a.
Multi-Stage Programs in Context. In
booktitleProceedings of the 12th ACM SIGPLAN International
Symposium on Haskell (Berlin, Germany) (seriesHaskell
2019). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages71–84.

[Pickering, Wu, and NémethPickering
et al2019b]
authorpersonMatthew Pickering, personNicolas
Wu, and personBoldizsár Németh.
Working with Source Plugins. In
booktitleProceedings of the 2019 ACM SIGPLAN Symposium on
Haskell (Berlin, Germany) (seriesHaskell '19).
publisherACM, addressNew York, NY, USA.

[Rodriguez, Jeuring, Jansson, Gerdes, Kiselyov,
and OliveiraRodriguez et al2008]
authorpersonAlexey Rodriguez, personJohan
Jeuring, personPatrik Jansson, personAlex Gerdes,
personOleg Kiselyov, and personBruno C. d. S.
Oliveira. year2008.
Comparing Libraries for Generic Programming in
Haskell. In booktitleProceedings of the First ACM SIGPLAN
Symposium on Haskell (Victoria, BC, Canada) (seriesHaskell
’08). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages111–122.

[Rompf and OderskyRompf and Odersky2010]
authorpersonTiark Rompf and personMartin
Odersky. year2010.
Lightweight Modular Staging: A Pragmatic Approach
to Runtime Code Generation and Compiled DSLs. In
booktitleProceedings of the Ninth International Conference
on Generative Programming and Component Engineering (Eindhoven, The
Netherlands) (seriesGPCE '10). publisherACM,
addressNew York, NY, USA, pages127–136.

authorpersonEvgeny Roubinchtein.
titleIR-MetaOCaml: (re)implementing MetaOCaml.
thesistypeMaster's thesis. schoolUniversity
of British Columbia.

[Schuster, Brachthäuser, and
OstermannSchuster et al2020]
authorpersonPhilipp Schuster,
personJonathan Immanuel Brachthäuser, and
personKlaus Ostermann. year2020.
Zero-cost Effect Handlers by Staging.
In submission.

[Serrano, Hage, Peyton Jones, and
VytiniotisSerrano et al2020]
authorpersonAlejandro Serrano,
personJurriaan Hage, personSimon Peyton Jones, and
personDimitrios Vytiniotis. year2020.
titleA quick look at impredicativity.
(dateJanuary year2020).

In submission.

[Serrano, Hage, Vytiniotis, and
Peyton JonesSerrano et al2018]
authorpersonAlejandro Serrano,
personJurriaan Hage, personDimitrios Vytiniotis,
and personSimon Peyton Jones. year2018.
Guarded Impredicative Polymorphism. In
booktitleProceedings of the 39th ACM SIGPLAN Conference on
Programming Language Design and Implementation (Philadelphia, PA, USA)
(seriesPLDI 2018). publisherACM,
addressNew York, NY, USA, pages783–796.

[Sheard and JonesSheard and Jones2002]
authorpersonTim Sheard and
personSimon Peyton Jones. year2002.
Template Meta-programming for Haskell. In
booktitleProceedings of the 2002 ACM SIGPLAN Workshop on
Haskell (Pittsburgh, Pennsylvania) (seriesHaskell '02).
publisherACM, addressNew York, NY, USA,

[Stucki, Biboudis, and OderskyStucki
et al2018]
authorpersonNicolas Stucki, personAggelos
Biboudis, and personMartin Odersky.
A Practical Unification of Multi-Stage Programming
and Macros. In booktitleProceedings of the 17th ACM SIGPLAN
International Conference on Generative Programming: Concepts and
Experiences (Boston, MA, USA) (seriesGPCE 2018).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages14–27.

authorpersonWalid Taha.
booktitleA Gentle Introduction to Multi-stage
publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, pages30–50.

[Taha and SheardTaha and Sheard1997]
authorpersonWalid Taha and personTim
Sheard. year1997.
Multi-stage Programming with Explicit Annotations.
In booktitleProceedings of the 1997 ACM SIGPLAN Symposium on
Partial Evaluation and Semantics-based Program Manipulation (Amsterdam, The
Netherlands) (seriesPEPM '97). publisherACM,
addressNew York, NY, USA, pages203–217.

[Taha and SheardTaha and Sheard2000]
authorpersonWalid Taha and personTim
Sheard. year2000.
MetaML and multi-stage programming with explicit
journalTheor. Comput. Sci. volume248,
number1-2 (year2000), pages211–242.

[Vytiniotis, Peyton Jones, Schrijvers, and
SulzmannVytiniotis et al2011]
authorpersonDimitrios Vytiniotis,
personSimon Peyton Jones, personTom Schrijvers, and
personMartin Sulzmann. year2011.
OutsideIn(X) Modular Type Inference with Local
journalJ. Funct. Program. volume21,
number4-5 (dateSept. year2011),

[Weirich, Voizard, de Amorim, and
EisenbergWeirich et al2017]
authorpersonStephanie Weirich, personAntoine
Voizard, personPedro Henrique Azevedo de Amorim, and
personRichard A. Eisenberg. year2017.
A Specification for Dependent Types in Haskell.
journalProc. ACM Program. Lang.
volume1, numberICFP, Article articleno31
(dateAug. year2017), numpages29 pages.

[Willis, Wu, and PickeringWillis
et al2020]
authorpersonJamie Willis, personNicolas Wu,
and personMatthew Pickering. year2020.
Staged Selective Parser Combinators.
In submission.

authorpersonJeremy Yallop.
Staged Generic Programming.
journalProc. ACM Program. Lang.
volume1, numberICFP, Article articleno29
(dateAug. year2017), numpages29 pages.

[Yallop, von Glehn, and KammarYallop
et al2018]
authorpersonJeremy Yallop, personTamara von
Glehn, and personOhad Kammar.
Partially-Static Data as Free Extension of
journalProc. ACM Program. Lang.
volume2, numberICFP, Article articleno100
(dateJuly year2018), numpages30 pages.