: A Language for Modular Tierless Web Programming

Gabriel Radanne

University of Freiburg

Jérôme Vouillon

IRIF UMR 8243 CNRS
Univ Paris Diderot, Sorbonne Paris Cité

Vincent Balat

IRIF UMR 8243
Univ Paris Diderot, Sorbonne Paris Cité

This work was partially performed at IRILL, center for
Free Software Research and Innovation in Paris, France,

Tierless Web programming languages allow programmers to combine client-side and server-side programming
in a single program.
Programmers can then define components with both client and server parts
and get flexible, efficient and typesafe client-server communications.
However, the expressive client-server features found in most
tierless languages are not necessarily compatible with
functionalities found in many mainstream languages.
In particular, we would like to benefit from type safety,
an efficient execution, static compilation, modularity and separate compilation.

In this paper, we propose
, an industrial-strength tierless functional Web programming language
which extends with support for rich client/server interactions.

allows to build whole applications as a single distributed program,
in which it is possible to define modular tierless libraries
with both server and client behaviors and combine them effortlessly.

is the only language that
combines type-safe and efficient client/server communications
with a static compilation model that supports separate compilation and
modularity. It also supports excellent integration with
, allowing to transparently leverage its ecosystem.

To achieve all these features, borrows ideas not only from distributed
programming languages, but also from meta-programming and modern module systems.

We present the design of , how it can be used in practice
and its formalization; including its type system, semantics and compilation
scheme. We show that this compilation scheme preserves typing
and semantics, and that it supports separate compilation.

§ INTRODUCTION

Writing websites nowadays requires the use of many different technologies:
HTML and CSS for the content and visuals of the website,
for client interactions,
any of the numerous server languages (PHP, Ruby, C#, …), a database
language such as SQL, etc.
Not only do programmers need to use all these technologies, but they also
need them to cooperate in an harmonious manner by ensuring
that communications between these various components are correct.
Such verification is often done manually by the programmer, which is both
error-prone and time-consuming.

This juggling of many different technologies does not only make programming more
complicated, it also imposes strong constraints on code organization and
prevents modularity. Let us consider the case where we want to add a comment
widget to a website.

This widget
requires code for client interactions, for example a convenient editor.
It also
requires server code that will store and serve the comments and potentially
some associated database queries. This code will thus be split in two codebases and
up to three languages. Furthermore, in order to be properly integrated in the
larger website, the internal communications between the client
and server parts of the widget will be exposed to the rest of the program.
All these
programming constraints, which stem directly from the way Web programming
is done currently, make it impossible to preserve abstraction and
encapsulation for widgets who have both client and server aspects.
This hinders safety and reusability of widgets by
preventing programmers to create self-contained independent libraries that
have both client and server aspects.

provides a comprehensive set of tools and libraries
for developing Web applications in .
is an industrial strenght statically typed functional programming language
with a rich ecosystem.
The project includes the compiler
<cit.>, a Web server, libraries for
concurrency <cit.> and HTML
manipulation <cit.>.
It also contains a complete framework to develop complex Web application
with both client and server components.
It includes modules for, among other things, RPCs,
Web GUIs <cit.>,
functional reactive Web programming and
an advanced service identification mechanism <cit.>.

is already used in production for a wide variety of websites

Based on our experience building such a framework, we realized we needed
additional tools to bridge the gap between client and server components.
Indeed, while provides excellent support for abstraction and modularity
through its module language, it doesn't allow to talk directly about the
relationship between client and server code.
In particular, we needed language constructs that allows us to blur the boundaries
between client and server.
Such language constructs can notably be provided by tierless languages.

§.§ Tierless Web Programming Languages

Tierless languages <cit.> allow programmers to
write in a composable way programs that have both client and server aspects.
They provide language constructs to define on the server functions that create
fragments of a Web page together with their associated client-side behavior.
This is done by allowing to freely intersperse client and
server expressions with seamless communication in a unique programming language.
By grouping together client and server parts, they allow to encapsulate
hybrid libraries and create more modular websites.

To be executed, tierless programs are sliced in two:
a part which runs on the server and a part
which is compiled to and runs on the client.
This slicing can be done either dynamically, by generating code
at runtime, or statically, by cutting the program in two during compilation.

Tierless languages can also leverage static typing to statically ensure that
communications between client and server are always correct.

Such tierless languages can also leverage both functional programming and
static typing.
Functional programming provides increased expressiveness and flexibility while
static typing gives strong guarantees about client-server separation,
in particular ensuring that communications are consistent
across tiers.

To complete the design of , we needed a language that not only
provides such expressive tierless features, but
also provides support for most features already supported by
: type safety, efficiency, static compilation, modularity and separate
Furthermore, Web programming often relies on numerous
external libraries (for encryption, HTML, logging, …). We wanted
to leverage all the existing tools and libraries developed either in the
project or the larger ecosystem.

§.§ The design of a Modular Tierless language

To build such a language with support for both modular and tierless features,
we outline several goals that will guide the design of our language.

Explicit communications.
Manual annotations should determine whether a piece of
code is to be executed server- or
client-side. This design
decision stems from our belief that the programmer must be well aware
of where the code is to be executed, to avoid unnecessary remote
interaction. Explicit annotations also prevent ambiguities in the
semantics, allow for more flexibility, and enable the programmer to
reason about where the program is executed and the resulting
trade-offs. Programmers can thus ensure that some data stays on the
client or on the server, and choose how much communication takes

A simple and efficient execution model.
The language should not incur additional back-and-forth communications
between client and server. Furthermore, the execution model should
be simple and predictable.
Having a predictable execution model is essential in the context of a language which is not purely functional, like .

Leveraging the type system.
The language should leverages the type system to allows composition and
modularity of client-server programs while preserving type-safety and abstraction.
This ensures, via the type-system, that client functions are not called
by mistake inside server code (and conversely) and ensures the correctness of client-server communications.

Integration with the host language.
Programmers must be able to leverage both
the language and the ecosystem of . libraries can be useful
on the server, on the client or on both.
As such, any file, even when compiled with the regular compiler, should be a valid module in our language.
Furthermore, we should be able to specify
if we want to use a given library on the client, on the server, or

Modularity and encapsulation.
Module and type abstractions are very powerful programming tools. By only exposing
part of a library, the programmer can safely hide implementation details
and enforce specific properties.
The language should leverages module abstraction to provide encapsulation
and separation of concern for widgets and libraries.
By combining module abstraction and tierless features, library authors can
provide good APIs that do not expose the fine-grained details of client-server
communication to the users.

§.§ Contributions and Plan

We propose ,
a tierless web programming language that supports static typing,
an efficient compilation scheme that avoids extra communications
and a very powerful form of modularity inspired by -style languages.
In particular, is the only tierless programming language
featuring efficient static separate compilation.
extends and can transparently leverage its complete ecosystem.

This article presents the design of , how it can
be used in practice, and formalizes the underlying core language.
Our contributions are the following:

* We designed , a tierless web programming language that follows the
set of goals presented above.
We demonstrate the practicality of our language through
examples (<ref>).

* We formalized the type system and the semantics of ,
including both the expression and the module layers (<ref>).
This formalization provides an interpreted semantics that is easy to
reason with and can be explained to programmers, but still maintains
's good properties regarding communications and typesafety.
Using this semantics, we show that supports
separate typechecking (<ref>)
and complete integration with (<ref>).

* As highlighted before, is not an interpreted language.
We formalized the compilation model of (<ref>).
This compilation scheme turns one program into two simpler
programs; one for the client and one for the server.
We show that such compilation scheme
supports separate compilation and
preserves both the typing and the semantics of (<ref>).

* We implemented as a patch on the compiler
and a runtime library[<https://github.com/ocsigen/ocaml-eliom> and <https://github.com/ocsigen/eliomlang>].

§ PROGRAMMING WITH

An application is composed of a single program that has both client and
server behaviors.
During compilation, the compiler decomposes the program into two parts.

The first part runs on a Web server, and is able to manage several connections and sessions at the same time.
The second part, compiled
statically to , is sent to each client by the Web server together with
the page, in response to the initial HTTP request.

In this section, we give a tour of the language through various examples.
As a guiding example for our exploration of the language, we consider
the case of a commenting system similar to websites such as Reddit or Hackernews,
A comment is a piece of HTML written by a user and identified by
a unique identifier.
Comments are initially stored on the server. Users can then manipulate
them on the client by voting, hiding or searching them.
Such a library features both server
aspects (storing and rendering the comments) and client
interactions (browsing and searching comments).

We start by giving a reminder of some important concepts on modules
before presenting the various concepts.
though is based on , little knowledge of is required.

We explicitly write some type annotations for
illustration purposes but they are not mandatory.

§.§ Going further

Through these various examples, we demonstrated how we can combine traditional
tierless features
with an advanced module system to create powerful and
expressive APIs. One one hand, tierless languages traditionally allows for complex
interplay of client and server code.
Module systems, on the other hand, allows to manipulate large pieces of code
while preserving abstraction, encapsulation and modularity.
to preserve these abstraction capabilities while enjoying the free-form
tierless programming style.

The ecosystem uses these concepts to provide numerous additional tools
such as advanced communication patterns, shared HTML across tiers
or even distributed Functional Reactive Programming <cit.>.
All these advanced
mechanisms are used in production by users.

§ THE CALCULUS

We now formalize as an extension of with both an expression and a module language.
To emphasize the new elements introduced by , these additional elements will be
colored in blue. This is only for ease of reading and
is not essential for understanding the formalization.

While is an extension of , is an extension of a
simpler calculus, which we present quickly in
We then present the location system in <ref>,
followed by the expression and the module languages
in <ref>.
Finally, we describe its semantics in <ref>.

Syntactic considerations

Let us first define some notations and meta-syntactic variables. As a general rule,
the expression language is in lowercase ($e$) and the module language is in
uppercase ($M$). Module types are in calligraphic letters ($\Mm$).
More precisely: $e$ are expressions, $x$ are variables, $p$ are module paths, $X$ are module variables, $\tau$ are type expressions and $\type{t}$ are type constructors.
$x_i$, $X_i$ and $\type{t_i}$ are identifiers (for values, modules and types).
Identifiers (such as $x_i$) have a name part ($x$) and a stamp part ($i$) that
distinguish identifiers with the same name (following <cit.>):
$\alpha$-conversion should keep the name intact and change only the stamp.

Sequences are noted with a star; for example $\tau^*$ is a sequence of type expressions.
Indexed sequences are noted $(\tau_i)$, with an implicit range.
Substitution of $a$ by $b$ in $e$ is noted $\subst[]{a}{b}{e}$.
Repeated substitution of each $a_i$ by the corresponding $b_i$ is noted

§.§ A crash course in the calculus

There are many variants of the calculus. For the purpose of , we consider
a core calculus with polymorphism, let bindings and parametrized datatypes
in the style of <cit.>,
accompanied by a fully featured module system with separate compilation and
applicative functors in the style of <cit.>.
The goal of this calculus is to closely module the most relevant features of
, while being sufficiently
simple to be extended and reasoned on formally.

In this section, we will simple give a quick overview of the syntax and
an informal reminder of the most distinctive or unusual points.
The complete treatment of the language
is given in <ref>.
Each set of typing or reduction rules can also be obtained by considering
the rules in the next section and ignoring the parts written in blue.

§.§.§ Syntax

The complete syntax is presented in <ref> and follows the syntax
of closely.

The expression language is a fairly simple extension of
the lambda calculus with a fixpoint combinator ($\Y$) and let bindings ($\letin{x}{e_1}{e_2}$).
The language is parametrized by a set of constants $\Const$.
Variables can be qualified by a module path $p$.
Paths can be either module identifiers such as $X_i$,
a submodule access such as $X_i.Y$,
or a path application such as $X_i(Y_j.Z)$.
Note that, as said earlier, that fields of modules are only called by their
name, without stamp.

The module language is composed of functors, module application
type constraints ($\constraint{\mm}{\Mm}$).
and structures containing a list of value, types
or module definitions ($\struct{\letm[]{x_i}{2}}$).
Programs are lists of definitions.

Module types can be either functor types ($\functor{X_i}{\Mm_1}{\Mm_2}$)
or a signature ($\signature{\valm[]{x_i}{\intty}}$), which contains a list
of value, types and module descriptions. Type descriptions can expose their definition
or can be left abstract.
Typing environments are simply module signatures. We note them $\Env$ for convenience.

§.§.§ Type system

As a general rule, judgements are denoted with the symbol $\iswt$ for
expressions and $\iswtm$ for modules.
More precisely:

$\wt[]{\Env}{e}{\tau}$    Expression $e$ has type $\tau$ in $\Env$

$\equivty[]{\Env}{\tau_1}{\tau_2}$    $\tau_1$ and $\tau_2$ are equivalent in $\Env$

$\wtm[]{\Env}{\mm}{\Mm}$    module $\mm$ has type $\Mm$ in $\Env$

$\submod[]{\Env}{\Mm}{\Mm'}$    Module type $\Mm$ is a subtype of $\Mm'$ in $\Env$

$\wf[]{\Env}{\tau}$ and $\wfm[]{\Env}{\Mm}$    The type $\tau$ (resp. module type $\Mm$) is well formed.

The type system for expression is the standard Hindley-Milner type system
with polymorphism, generalization and parametrized datatype.
The module system, which follows <cit.>, is less usual. We will focus on three specific features:
qualified accesses, applicative functors and strengthening.

Qualified accesses

Let us consider the module $X$ with the module type
$\renewcommand\added\addedhide(\signature{\typeabsm{t};\ \valm{a}{t}})$. $X$ contains
a type $t$ and a value $a$ of that type.
We wish to typecheck $X.a$. One expected type for this expression is $X.t$.
However, the binding of $v$ in $X$ gives the type $t$, with no mention of
$X$. In order to make the type of $X.a$ expressible in the current scope,
we prefix the type variable $t$ by the access path $X$.
This is done in the rule QualModVar by the substitution
$\substs[]{n_i}{p.n}{\bv[]{\Sm_1}}{\Mm}$ which prefixes all the bound variables of $\Sm_1$, noted $\bv[]{\Sm_1}$, by the path $p$.
We thus obtain the following type derivation

*[Left=QualVar, Right=with $X.t = \subst[]{t}{p.t}{t}$]
Xt; at

Applicative functors

In <ref>, we used the Map.Make functor
to create a new dictionary data-structure using the provided type
as keys. One might wonder what happens if Map.Make is applied
to the same module twice. Are the dictionaries thus produced compatible?
More formally, Does $\mm_1 = \mm_2$ implies $F(\mm_1) = F(\mm_2)$?
When this holds, we say that functors are “applicatives”. Otherwise, we
say they are “generatives”. functors are applicatives by default.
In our simple calculus, all functors are applicatives.
This is implemented by enriching type constructors with types
of the form $F(M).t$. If we consider the modules $N_i = \text{Map.Make}(\mm_i)$,
then we have
$N_1.t = \text{Map.Make}(\mm_1).t = \text{Map.Make}(\mm_2).t = N_2.t$.

Let us consider a module $X$ answering the signature shown
<ref>. We want to pass this module to the functor $F$
shown in <ref>. This functor application
is expected to succeed, since $X.t = t$, where $t$ comes from $X$.
However, the definition of $t$ in $X$ is abstract, and does not have
a definition allowing us to check that $X$ is indeed compatible with the proposed
For this purpose, we strengthen the type of the module $X$ with
additional type equalities. If $\mathcal X$ is the type of $X$, we note
$\strengthen{\mathcal X}{X}$ the strengthened signature.
The result is the signature
$\renewcommand\added\addedhide(\signature{\typem[]{t}{X.t};\ \valm[]{v}{t}})$.
This signature is now trivially included in the argument type of $F$.

\begin{align*}
\end{align*}

Typing environment

\begin{align*}
&\mathtt{module}\ F\ (E:\signature{\typem[]{t}{X.t}\ \valm[]{v}{t}}) = \mathtt{struct}\\
\end{align*}

Application of multi-argument functor using manifests

Program using functors and manifest types

§.§.§ Semantics

We use a rule-based big-step semantics with traces. Big-step semantics
are more amenable to reasoning with modules, as they allow to easily introduced
local bindings. We record traces in order to reason about
execution order.

We note $v$ for values in the expression language and $\vm$ for values
in the module language.
Values in the expression language can be either constants or lambdas.
Module values are either structures, which are list of bindings of
values, or functors.

Execution environments, noted $\envr$,
are a list of value bindings. We
note the concatenation of environment $+$. Environment access is noted
$\bdrin{x}{v}{\envr}$ where $x$ has value $v$ in $\envr$.
The same notation is also used for structures.

Traces are lists of messages.
The empty trace is noted $\niltr$. Concatenation of traces is noted $\ctr$.

Given an expression $e$ (resp. a module $\mm$), an execution
environment $\envr$, a value $v$ (resp. $\vm$) and a trace $\trace$,

\[\renewcommand\added\addedhide
\redto{\envr}{e}{v}{\trace}
\]

means that $e$ reduces to $v$ in $\envr$ and prints $\trace$.
The rules are composed of traditional call-by-value lambda-calculus
with a fixed execution order that is represented by the traces.

§.§.§ Formal results

The calculus considered here has been shown to support
for separate compilation (<ref>) and
representation independence <cit.>.
It doesn't have a proof of soundness, which discussed in <ref>.

§.§ Locations

Before introducing the language constructs, we consider
the notation for locations annotations
which indicate “where the code runs”.
The grammar of locations is given in <ref>.
There are three core locations:
server, client or base.
The base side represents expressions that are “location-less”, that is,
which can be used everywhere. We use the meta-variable $\loc$
for an unspecified core location.
There is a fourth location that is only available for modules: mixed.
A mixed module can have client, server and base components.
We use the meta-variable $\mloc$ for locations that are either m or
one of the core locations. In most contexts, locations are annotated
with subscripts.

\begin{align*}
\loc ::=&\ s\ |\ c\ |\ \base&
\mloc ::=&\ \sideX\ |\ \loc
\end{align*}

Grammar of locations – $\loc$ and $\mloc$

“can be used in” relations on locations – $\canuseloc{\mloc}{\mloc'}$

“can contain” relation on locations – $\canbedefloc{\mloc}{\mloc'}$

We also introduce two relations:

$\canuseloc{\mloc}{\mloc'}$ defined in <ref>, means that
a variable (either values, types or modules) defined on location $\mloc$ can
be used on a location $\mloc'$. For example, a base type can be used in a client context.
Base declarations are usable everywhere. Mixed declarations are not usable in base code.

$\canbedefloc{\mloc}{\mloc'}$ defined in <ref>, means that
a module defined on location $\mloc$ can contain component on location $\mloc'$.
In particular, the mixed location $\sideX$ can contain any component, while other
location can contain only component declared on the same location.

Both relations are reflexive: For instance,
it is always possible to use client declarations when you are on the client.

§ COMPILATION OF PROGRAMS

In <ref>, we gave a tour of the language
from a formal perspective, providing a type system and an interpreted semantics.

, however, is not an interpreted language. The interpreted semantics
is here both as a formal tool and to make the semantics of the language more
approachable to users, as demonstrated in <ref>.

In the implementation, programs are compiled to two programs: one server program
(which is linked and executed on the server) and a client program (which is
compiled to and executed in a browser). The resulting programs are efficient
and avoid unnecessary back-and-forth communications between the client and the server.

Description of the complete compilation toolchain, including emission of
code, is out of scope of this article (see <cit.>).

Instead, we describe
the compilation process in term of emission of client and server
programs in an -like language equipped with additional primitives.
Hence, we present
the typing and execution of compiled programs, in <ref>
and the compilation process, in <ref>.
We then show that our compilation process preserves both the typing
and the semantics in <ref>.

§ STATE OF THE ART AND COMPARISON

takes inspiration from many sources.
The two main influences are, naturally,
the extremely diverse ecosystem of web programming
languages and frameworks, which we explore in <ref>,
and the long lineage of programming languages

One of the important contributions of is the use of a programming
model similar to languages for distributed systems (<ref>)
while using an execution model inspired by staged
meta-programming (<ref>).

§.§ Web programming

Various directions have been explored to simplify Web
development and to adapt it to current needs.
places itself in one of these directions,
which is to use the same language on the server and the client.

Several unified client-server languages have been proposed. They
can be split in two categories depending on their usage of .
can either be used on the server, with Node.js,
or as a compilation target, for example with Google Web Toolkit for Java
or Emscripten for C.

The approach of compiling to was also used to develop new client
languages aiming to address the shortcomings of . Some of them are new languages, such as
Haxe, Elm or Dart. Others are only extensions, such as
TypeScript or CoffeeScript.
[A fairly exhaustive list of languages compiling to can be found
in <https://github.com/jashkenas/coffeescript/wiki/List-of-languages-that-compile-to-JS>]

However, these proposals only address the fact that is an inadequate language for
Web programming. They do not address the fact that the model of Web programming itself –
server and client aspects of web applications are split in two
distinct programs with untyped communication – raises usability, correctness
and efficiency issues.
A first attempt at tackling these concerns is to specify the communication between
client and server. Such examples includes SOAP[<https://en.wikipedia.org/wiki/SOAP>]
(mostly used for RPCs) and REST[<https://en.wikipedia.org/wiki/Representational_state_transfer>]
(for Web APIs).
A more recent attempt is the GraphQL <cit.> query language
which attempts to describe, with a type system, the communications
between the client and server parts of the application.

These proposals are very powerful and convenient ways to check and
document Web-based APIs. However, while making the contract between
the client and the server more explicit, they further separate
web applications into distinct tiers.

Tierless languages attempt to go in the opposite direction: by removing
tiers and allowing web applications to be expressed in one single program,
they make the development process easier and restore the possibility
of encapsulation and abstraction without compromising correctness.
In the remainder of this section, we attempt to give a
fairly exhaustive taxonomy of tierless programming languages. We first
give a high-level overview of the various trade-offs involved, then
we give a detailed description of each language.

§.§.§ Code and data location

In , code and data locations are specified through syntactic annotations.
Other approaches for determining locations have been proposed.

The first approach
is to infer locations based on known elements through a
control flow analysis (Stip.js, , ):
database access is on the server, dynamic DOM interaction is done on the client, etc.

Another approach is to extend the type system with
locations information (, 5).
Locations can then be determined by relying on simple type inference and

These various approaches present a different set of compromises:

* We believe that the semantics of a language should be easy to
predict by looking at the code,
which is why uses syntactic annotations to specify locations.
This fits well within the language,
which is specifically designed to have a predictable behavior.
On the other end of the spectrum, languages with inferred location
sacrifice predictability for a very light-weight syntax which provides
very little disruption over the rest of the program.
Typed based approaches sit somewhere in the middle: locations
are not visible in the code but are still accessible through types.
Such approaches benefit greatly from IDEs allowing exploring
inferred types interactively.

* Naturally, explicit approaches are usually more expressive than implicit
approaches. Specifying locations manually gives programmers greater
control over the performance of their applications.
Furthermore, it allows to express mixed data structures,
data structures that contain both server and client parts as
presented in <ref>.
Such idioms are difficult to express when code locations are inferred.
We demonstrate this with an example in the description.

* Type-directed approaches to infer code location is an extremely
elegant approach.
It can be employed either in an algebraic effect
setting () or as modal logic annotations (5).
By its type-directed nature, error messages can be expressed
in term of the source language and it should lend itself naturally
to separate compilation (although this has not yet been achieved).
However, such novel type systems significantly extend traditional
general purpose type systems (the one, in this case) to the point
where it seems difficult to retrofit them on an existing languages.
One lead
would be to provide a tight integration using a form of Foreign
Function Interface. Such integration has yet to be proposed.

* , as a language based on , is an effectful language.
Marrying inference of locations and a side-effecting semantics is
delicate. The Stip.js library <cit.> attempts to solve this by
automatically providing replication and eventual consistency on shared
references. This might cause many more communications that necessary
if not done carefully.
We believe that such decision is better left in the hands of the programmer.

§.§.§ Slicing

Once code location has been determined, the tierless program must be sliced
in (at least) two components. In , slicing is done statically
at compile time in a modular manner: each module is sliced independently.

Another common approach is to use a static whole-program slicing transformation (, Stip.js). This is most common for languages where code
location is inferred, simply due to the fact that such inference is often
This allows precise analysis of location that can benefit from useful
code transformations such as CPS transformation <cit.>,
inlining and defunctionalization.
However, this can make it difficult for the users to know where each piece of code is executed and hinder error messages,.
It also prevents any form of separate compilation.

Finally, slicing can be done at runtime simply by generating client
code “on the fly” during server execution (, , ).
Such solution has several advantages: it is easier to implement and provides a
very flexible programming
style by allowing programmers to compose the client program in arbitrary ways.
The downside is that it provides less guarantees to the users.
Furthermore, it prevents generating and optimizing a single file
in advance, which is beneficial for caching and execution purposes.

Separate and incremental compilation

Most current mainstream compiled language support some form of incremental compilation. Indeed, incremental compilation avoids recompiling
files of which no dependency has changed. This accelerates the feedback
loop between development and testing greatly and allow very fast
recompilation times. In the case of statically typed languages, it also
allows immediate checking of the modified file thus providing developers
very fast iteration cycles.
The easiest way to implement incremental compilation is through
separate compilation, where each file can be compiled completely independently.
Furthermore, separate compilation is compatible with link-time
optimization and thus does not prevent generation of
heavily optimized code, as demonstrated by nearly every C compiler.

As a consequence, we consider languages that do not support incremental
compilation completely unusable for practical usages.

§.§.§ Communications

uses asymmetric communication between client and server
(see <ref>):
everything needed to execute the client code is sent during the initial communication
that also sends the Web page.
It also exposes a convenient API for
symmetric communications using RPC (<ref>) and broadcasts, which must be used manually.

We thus distinguish several kind of communications.
First, manual communications are exposed through normal APIs and are performed explicitly by programmers. Of course, the convenience and safety of such
functions vary a lot depending on the framework.
Then, we consider automatic communications, that are inserted automatically
by the language at appropriate points, as determined by code locations
and slicing.

We can further decompose automatic communications further
in two categories. In static asymmetric communications,
information is sent from the server to the client automatically,
when sending the page.

In dynamic symmetric communications, information is sent back and forth
between the client and the server dynamically through some
form of channel (AJAX, websockets, Comet, …).

While symmetric communications are very expressive, they impose
a significant efficiency overhead: a permanent connection must be established
each communication imposes a round trip between client and server.
Furthermore, such communication channel must be very reliable.
On the other hand, asymmetric communications are virtually free: data
is sent with the web page (and is usually much smaller). Only a thin
instrumentation is needed.

Of course, the various communication methods can be mixed in arbitrary manner.
, for example, uses both automatic asymmetric and manual communications.

Offline usage

Many web applications are also used on Mobile phones, where connection
is intermittent at best. As such, we must consider the case where
the web application produced by a tierless language is used offline.
In this context, asymmetric communication offer a significant advantage:
given the initially transmitted information by the server, the client
program can run perfectly fine without connection.
This guarantee, however,
does not extend to dynamic manual communications done by the use of RPCs
and channels.
<cit.> explore this question for symmetric communications
through their R5 requirement.

§.§.§ Type systems

Type safety in the context of tierless languages can encompass several notions.
The first notion is the traditional distinction between weakly and strongly
typed languages. In the interest of avoiding a troll war among the jury, we
will not comment further.
A more interesting question is whether communication errors between
client and server are caught by the typechecker. This is, surprisingly,
not the case of since location inference and slicing is done very late
in the compilation process, far after type checking.
One consequence of this is that slicing errors are
fairly difficult to understand
“However, the approach we adopted instead, with ad-hoc static analysis on
whole programs at compile time, leads to error messages that confuse even
experienced Ur/Web programmers.”]
While the formalization is type safe, the implementation
is not, due to the use of wrapping and Marshall,
which will fail at runtime on functional values.

Another remark is the distinction between client and server universes.
[Or, more philosophically:
Is your favorite language platonist or nominalist ?
has separate type universes for client and server types (see <ref>). Most tierless languages do not provide such distinction,
notably for the purpose of convenience. Distributed systems such as
Acute, however, do make such distinction to provide a solution
for API versionning and dynamic reloading of code. In this case, there
are numerous distinct type universes.

Module systems

The notion of module system varies significantly depending
on the language. In we consider an -style module system
composed of a small typed language with structures and functors.
We believe modules are essential for building medium to large sized
programs: this has been demonstrated for general purpose languages but
also holds for web programming languages, as demonstrated by
the size of large modern websites (the web frontend of facebook alone is
over 9 millions lines of code). Even recently obtained
a module system in ES6.

In the context of tierless languages, an interesting question is the
interaction between locations and modules. In particular, can modules contain
elements of different locations and, for statically typed languages,
are locations reflected in signatures?

Types and documentation

Type systems are indisputably very useful for correctness purposes, but they
also serve significant documentation purposes. Indeed, given a function,
its type signature provides many properties. In traditional languages,
this can range from very loose (arguments and return types) to very precise
(with dependent types and parametricity <cit.>).
In the context of tierless languages, important questions we might want
to consider are “Where can I call this function?” and
“Where should this argument come from?”.
The various languages exposes this information in different ways:
does not expose
location in the types, but it is present in the signature. 5 exposes
this information directly in the types. and do not expose that
information at all.

§.§.§ Details on some specific approaches

We now provide an in-depth comparison with the most relevant approaches.
A summary in <ref> classifies each approach according
to the main distinctive features described
in the previous paragraphs. Each language or
framework is also described below.

Locations   Slicing   Communications   Type safe   Host language
Syntactic   Modular   Asymmetric

Type-based*   Dynamic*   Symmetric      -

Inferred   Global   (A)symmetric$\sim$   *   -

Haste   Type-based   Modular   Symmetric      Haskell

Syntactic   Dynamic*   (A)symmetric$\sim$   ×   *

Meteor.js   Syntactic   Dynamic   Manual   ×

Stip.js   Inferred   Global   Symmetric*   ×

5   Type-based   Global*   Symmetric      -

Acute   Syntactic   Modular   Distributed

Summary of the various tierless languages
See previous sections for a description of each headline.
A star * indicates that details are available
in the description of the associated language.
A tilde $\sim$ indicates that we are unsure, either because the information
was not specified, or because we simply missed it.

<cit.> is a new statically typed language especially designed for Web programming.
It features a rich -like type and module system and a fairly original
execution model where programs only execute as part of a web-server
request and do not have any state (the language is completely pure).
While similar in scope to , it follows a very different approach:
Location inference and slicing are done through a whole-program transformation
operated on a fairly low level representation. Notably, this transformation
relies on inlining and removal of high-order functions (which are not supported
by the runtime).
The advantages of this approach are twofold: It makes applications
extremely fast (in particular because it doesn't use a GC: memory
is trashed after each request) and it requires very little syntactic
overheads, allowing programs to be written in a very elegant manner.

The downsides, however, are fairly significant.
's approach is incompatible with any form of separate compilation.
Many constructs are hard-coded into the language, such as RPCs
and reactive signals and it does not seem possible to implement them
as libraries.
The language is clearly
not general and has a limited expressivity, in particular
when trying to use mixed data-structures (see <ref>).
For example, <ref>. presents the server function
which takes a list of labels and client functions and generates a list of
buttons. We show the implementation and a tentative implementation. The version typechecks but slicing fails. We
are unable to write a working version and do not believe it to be possible:
indeed, in the version we use a client fragment to build the
list l as a mixed data-structure. This annotation is essential
to make the desired semantics explicit.
Some examples are expressible only using reactive signals, which present a very
different semantics.

[ ("Click!", [

ul (List.map (fun (name, action) ->
li [button
a:[a_onclick action]
[pcdata name]])

let main () =
body (button_list l)

fun main () : transaction page =
fun handler _ = alert "clicked!"
val l = Cons (("Click!", handler), Nil)

fun button_list lst =
case lst of
Nil => <xml/>
| Cons ((name, action), r) =>
<button value=name
button_list r
return <xml>
<body>button_list l</body>

Tentative version. Typechecks but does not compile.

Programs building a list of buttons from a list of client side actions

<cit.> is a dialect of Scheme for programming Web
applications. Its successor, .js <cit.>, takes the same concepts and brings them to .
The implementation of .js is very complete and allow them to run
both the and the scheme dialect while leveraging the complete
node.js ecosystem.
uses very similar language constructions to the one provided
by : $\sim$-expressions are fragments and $-expressions are
injections. All functions seem to be shared by default.
Communications are asymmetric when possible and use channels otherwise.
However, contrary to , slicing is
done dynamically during server execution <cit.>.

In the tradition of Scheme, only uses a minimal type system for
optimizations and does not have a notion of location. In particular
does not provide static type checking and does not statically enforce the
separation of client and server universes (such as preventing the use of database
code inside the client).

The semantics of has been formalized <cit.>
and does present similarities to the interpreted semantics (<ref>). is however significantly
more dynamic than : it allows dynamic communication patterns
through the use of channels and allows nested fragments in the
style of Lisp quotations which allows to generate client code
inside client code.

For dynamically-typed inclined programmers, currently presents the most
convincing approach to tierless Web programming. In particular given
its solid implementation, great flexibility and support for the ecosystem.

is an experimental functional language for client-server Web programming
with a syntax close to and an -like type system. Its
type system is extended with a notion of effects, allowing
a clean integration of database queries in the language <cit.>.
In <ref>,
we highlight two notable points of : the function adults
takes as argument a list l and returns the name of all the
person over 18. This function has no effect and can thus run on the client,
the server, but can also be transformed into SQL to run in a database query.
On the other hand, the print function has an effect called “wild”
which indicates it can't be run inside a query. Effects are also used
to provide type-safe channel-based concurrency.

also allows
to annotate functions by indicating on which location they should run.
Those annotations, however, are not reflected in the type
system. Communications are symmetric and completely dynamic through
the use of AJAX. Client-server slicing
is dynamic (although some progress has been made towards static
query slicing <cit.>) and can introduce
“code motion”, which can moves closures from the server
to the client. This can be extremely problematic in practice, both from
an efficiency and a security point of view.
The current implementation of is interpreted but a compilation
scheme leveraging the Multicore-efforts has been recently added.

Although is very seducing, the current
implementation presents many shortcomings given its statically typed
nature: slicing is dynamic and produces fairly large
code and the type system does not really track client-server locations.

links> fun adults(l)  for (x <- l) where (x.age >= 18) [(name = x.name)]  ;;
adults = fun : ([(age:Int,name:a|_)]) -> [(name:a)]

links> print ;;
print : (String) wild-> ()

Small pieces of code

Meteor.js<cit.> is a framework where both the
client and the server sides of an application are written in .
It has no built-in mechanism for sections and fragments but relies on conditional $\mathtt{if}$ statements on the  and
constants. It does not perform any slicing. This means that there are no static guarantees over the respective execution of server and client code. Besides, it provides no facilities for client-server communication such as fragments and injections.
Compared to , this solution only provides coarse-grained composition.

Stip.js<cit.> allows to slice tierless programs with a minimal amount of annotations. It emits Meteor.js
programs with explicit communications. Annotations are optionally provided
through the use of comments, which means that Stip.js are actually
perfectly valid programs. Location inference and slicing are
whole-program static transformations. Communications are symmetric, through
the use of fairly elaborate consistency and replication mechanisms for
shared references.
This approach allows the programmer to write code with very little annotations.
As opposed to , manual annotations are possible, which might allow
to express delicate patterns such as mixed data-structures and prevents
security issues.

§.§ Distributed programming

Tierless languages in general are very inspired by distributed programming languages. The
main difference being that distributed programs contain an arbitrary number of locations
while tierless web programs only have two: client and server. Communications
are generally symmetric and dynamic, due to the multi-headed aspect of distributed
systems. There are of course numerous programming languages dedicated to distributed
programming. We present here two relevant approaches that put
greater emphasis on the typing and tierless aspects.

Haste<cit.> is an Haskell EDSL
for distributed programming.
This DSL allows to express complex orchestrations of multiple nodes and external components
(for example databases and IoT components), with handling of distinct type universes when necessary.
Instead of using syntactic annotations, locations are determined through typing.
This approach works particularly well in the context of Haskell,
thanks to the advanced type system and the syntactic support for monads and functors.
Multiple binaries are produced from one program. Slicing relies on type information
and dead code elimination, as provided by the GHC compiler.
Explicit slicing markers similar to 's section annotations are the subject
of future work.
Communications are dynamic and symmetric through the use of websockets.
One notable feature of this DSL is that it offers a client-centric view:
The control flow is decided by the client which pilots the other nodes. This
is the opposite of where the server can assemble pieces of
client code through fragments.

This work also inherits
the Haskell and GHC features in term of modules, data abstraction and
A module language has been developed for Haskell by <cit.>.

An earlier version, Haste.App <cit.>, was limited to only one
client and one server and used a monadic approach
to structure tierless programs.

5<cit.> is an language that introduces new constructs for type-safe communication between distributed actors through the use of location annotations
inside the types called “modal types”.
It is geared towards a situation where all actors have similar capabilities.
It uses dynamic communication, which makes the execution model very different from .
5 provides a very rich type system that allows to precisely export
the capabilities of the various locations. For example, it is possible
to talk about addresses on distant locations and pass them around arbitrary.
only supports such feature through the use of fragments, for client

Unfortunately, 5 does not have a module system.
However, we believe that
5's modal types can play a role similar to 's location
annotations on declarations, including location polymorphism.
5 uses a global transformation for slicing.
Given the rich typing information present
in 5's types, it should lend itself fairly well to a modular
slicing approach, but this has not been done.

Acute<cit.> is an extension of for distributed programming.
It provides typesafe serialization and deserialization and also allows arbitrary loading
of modules at runtime.
Like , it provides a full-blown module system.
However, it takes an opposite stance on the execution model:
each actor runs independent programs and communications
are completely dynamic.

Handling of multiple type universes is done by providing
a description of the type with each message and by versioning APIs.
In particular, great care is taken to provide type safe serialization by
also transmitting the type of messages alongside each message.
This gives Acute very interesting capabilities, such as reloading
only part of the distributed system in a type-safe way.

§.§ Staged meta-programming

An important insight regarding is that, while it is a tierless programming language
and tries to disguise itself as a distributed programming language, corresponds exactly to a staged meta-programming language.
simply provides only two stages: stage 0 is the server, stage 1 is the
's client fragments are the equivalent of stage quotations.

Most approaches to partial evaluation are done implicitly (not unlike tierless
languages with implicit locations).
We take inspiration from several approaches that combine staged meta-programming
with explicit stages annotations that are reflected in the type system.
We only look at the most relevant approaches but a longer description of
the history of staged meta-programming approaches
can be found in <cit.>.

MetaOCaml<cit.> is an extension of for meta programming. It introduces a quotation annotation for staged expressions, whose execution is delayed.
Quotations and antiquotations corresponds exactly to fragments and injections. The
main difference is that MetaOCaml is much more dynamic: quoted code
does not have to be completely closed when produced and well-scopedeness
is checked dynamically, just before running the quoted code. This allows
very dynamic behaviors such as automatic insertion of let-bindings <cit.>
and dynamically determining staged stream pipelines <cit.>.
One difference is the choice of universes: has two universes, client and server, which are distinct. MetaOCaml has a single type universe but a series
of scopes, for each stage, included in one another.

MetaOCaml itself provides no support for modules and
only leverages the module system. Staging annotations
are only on expressions, not on declarations.

Modular macros<cit.> are another extension of .
It uses staging to implement macros. It provides both a quotation-based expression
language along with staging annotations on declarations. It also aims to support modules
and functors.
slicing can be seen as dynamic (since code is executed at compile time to produce
pieces of programs). In particular, this allows to lift most of the restriction imposed on multi-stage functors.
They also use a notion similar to converters, except that the serialization format
here is simply the AST.

The main difference compared to is how the asymmetry between stage 0 and stage 1 is
treated. Only one type universe is used and there is no notion of slicing that would
allow a distant execution.

<cit.> presents a slicing technique for a two-staged simply typed lambda calculus. Their technique is similar to the one used in .
They distinguish their language it three parts: $1\mathcal{G}$, which corresponds
to base code; $1\mathcal{M}$, which corresponds to server code; and $2\mathcal{M}$,
which corresponds to client code.
They also provide a proof of equivalence between the dynamic semantics and the slicing
techniques. This proof has been mechanized in Twelf.
While their work is done in a more general settings, they do not specify how to
transfer rich data types across stages (which is solved in using converters).
They also do not propose a module system.

§ CONCLUSION

We presented , a Modular Tierless Web programming
language that supports static typing, an efficient execution model,
abstraction and modularity.
We showed its design through numerous examples and formalized it.
In our formalization, we first gave a simple interpreted
semantics, that is suitable to explain to programmers. We then gave
a more efficient compilation scheme and showed that it
preserves both typing and semantics. The compilation scheme follows precisely
the current implementation of .

Many design choices of were inspired by practical concerns.
Indeed, in order to be useful, a language must have an ecosystem. The simplest way to have an ecosystem
is to reuse the one of an existing language, in our case the one.
Since separate compilation and modularity are indispensable for any non-trivial programming projects,
we needed to make modularity, abstraction and the tierless annotations interact.
is thus inspired by many different elements
such as languages, tierless
web programming and staged meta-programming.
In particular, aims to combine a semantics inspired by staged meta-programming
and an -style module system.

We believe that such combination can be used in a wider context
than simply Web programming. Indeed, has also been used to create
Mobile applications <cit.>. We would like to extend our language
to be usable to any kind of client-server applications
that requires dynamicity, type safety and modularity.
We also consider extending our model to explicitely support
multiple distinct clients.
Finally, we aim to further explore the programming patterns made
possible by , for instance multi-tiers functional reactive programming.

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

[Amin and RompfAmin and Rompf2017]
authorpersonNada Amin and personTiark
Rompf. year2017.
Type soundness proofs with definitional
interpreters. In booktitleProceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages, POPL 2017,
Paris, France, January 18-20, 2017,
editorpersonGiuseppe Castagna and
personAndrew D. Gordon (Eds.). publisherACM,

[Aydemir, Charguéraud, Pierce, Pollack, and
WeirichAydemir et al2008]
authorpersonBrian E. Aydemir, personArthur
Charguéraud, personBenjamin C. Pierce,
personRandy Pollack, and personStephanie Weirich.
Engineering formal metatheory. In
booktitleProceeding of the 35th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (POPL),
editorpersonGeorge C. Necula and
personPhilip Wadler (Eds.). publisherACM,

authorpersonVincent Balat.
Rethinking Traditional Web Interaction: Theory and
journalInternational Journal on Advances in Internet
Technology (year2014).

Besport year2017.

[Botlan and RémyBotlan and
authorpersonDidier Le Botlan and
personDidier Rémy. year2003.
ML\({}^{\mbox{F}}\): raising ML to the power of
system F. In booktitleICFP.
publisherACM, pages27–38.

[Boudol, Luo, Rezk, and SerranoBoudol
et al2012]
authorpersonGérard Boudol,
personZhengqin Luo, personTamara Rezk, and
personManuel Serrano. year2012.
Reasoning about Web Applications: An Operational
Semantics for HOP.
journalACM Trans. Program. Lang. Syst.
volume34, number2 (year2012),

[Cheney, Lindley, Radanne, and WadlerCheney
et al2014]
authorpersonJames Cheney, personSam
Lindley, personGabriel Radanne, and personPhilip
Wadler. year2014.
Effective quotation: relating approaches to
language-integrated query. In booktitleProceedings of the
ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation,
PEPM 2014, January 20-21, 2014, San Diego, California, USA,
editorpersonWei-Ngan Chin and
personJurriaan Hage (Eds.). publisherACM,

authorpersonAdam Chlipala.
An Optimizing Compiler for a Purely Functional
Web-Application Language. In booktitleICFP.

authorpersonAdam Chlipala.
Ur/Web: A Simple Model for Programming the
Web. In booktitleProceedings of the 42Nd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(seriesPOPL '15). publisherACM,
addressNew York, NY, USA, pages153–165.

[Cooper, Lindley, Wadler, and YallopCooper
et al2006]
authorpersonEzra Cooper, personSam Lindley,
personPhilip Wadler, and personJeremy Yallop.
Links: Web Programming Without Tiers. In
booktitleFMCO. pages266–296.

authorpersonAnton Ekblad.
A meta-EDSL for distributed web applications. In
booktitleProceedings of the 10th ACM SIGPLAN
International Symposium on Haskell, Oxford, United Kingdom, September 7-8,
2017, editorpersonIavor S. Diatchki (Ed.).
publisherACM, pages75–85.

[Ekblad and ClaessenEkblad and
authorpersonAnton Ekblad and personKoen
Claessen. year2014.
A Seamless, Client-centric Programming Model for
Type Safe Web Applications. In booktitleProceedings of the
2014 ACM SIGPLAN Symposium on Haskell (seriesHaskell
'14). publisherACM, addressNew York, NY, USA,

[Feltman, Angiuli, Acar, and
FatahalianFeltman et al2016]
authorpersonNicolas Feltman, personCarlo
Angiuli, personUmut A. Acar, and personKayvon
Fatahalian. year2016.
Automatically Splitting a Two-Stage Lambda
Calculus, See DBLP:conf/esop/2016, pages255–281.

authorpersonJ. Garrigue.
titleA Certified Interpreter for ML with Structural

Gencore year2017.
booktitleNew York University Gencore.

GraphQL year2016.

Hashids year2017.

[Kilpatrick, Dreyer, Peyton Jones, and
MarlowKilpatrick et al2014]
authorpersonScott Kilpatrick, personDerek
Dreyer, personSimon L. Peyton Jones, and
personSimon Marlow. year2014.
Backpack: retrofitting Haskell with interfaces. In
booktitleThe 41st Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '14, San Diego, CA, USA, January
20-21, 2014, editorpersonSuresh Jagannathan and
personPeter Sewell (Eds.). publisherACM,

authorpersonOleg Kiselyov.
The Design and Implementation of BER MetaOCaml -
System Description. In booktitleFunctional and Logic
Programming - 12th International Symposium, FLOPS 2014, Kanazawa, Japan,
June 4-6, 2014. Proceedings (seriesLecture Notes in
Computer Science), editorpersonMichael Codish and
personEijiro Sumii (Eds.), Vol. volume8475.
publisherSpringer, pages86–102.

authorpersonOleg Kiselyov.
Generating Code with Polymorphic let: A Ballad of
Value Restriction, Copying and Sharing. In
booktitleProceedings ML Family / OCaml Users and
Developers workshops, ML Family/OCaml 2015, Vancouver, Canada, 3rd & 4th
September 2015. (seriesEPTCS),
editorpersonJeremy Yallop and
personDamien Doligez (Eds.), Vol. volume241.

[Kiselyov, Biboudis, Palladinos, and
SmaragdakisKiselyov et al2017]
authorpersonOleg Kiselyov, personAggelos
Biboudis, personNick Palladinos, and personYannis
Smaragdakis. year2017.
Stream fusion, to completeness. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium
on Principles of Programming Languages, POPL 2017, Paris, France, January
18-20, 2017, editorpersonGiuseppe Castagna and
personAndrew D. Gordon (Eds.). publisherACM,

[Lee, Crary, and HarperLee
et al2007]
authorpersonDaniel K. Lee, personKarl
Crary, and personRobert Harper.
Towards a mechanized metatheory of standard ML.
In booktitleProceedings of the 34th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2007, Nice, France,
January 17-19, 2007, editorpersonMartin Hofmann
and personMatthias Felleisen (Eds.).
publisherACM, pages173–184.

authorpersonXavier Leroy.
Manifest Types, Modules, and Separate Compilation.
In booktitleConference Record of POPL'94: 21st ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland,
Oregon, USA, January 17-21, 1994,
editorpersonHans-Juergen Boehm,
personBernard Lang, and personDaniel M. Yellin
(Eds.). publisherACM Press, pages109–122.

authorpersonXavier Leroy.
Applicative Functors and Fully Transparent
Higher-Order Modules. In booktitleConference Record of
POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, San Francisco, California, USA, January 23-25, 1995,
editorpersonRon K. Cytron and
personPeter Lee (Eds.). publisherACM Press,

authorpersonXavier Leroy.
A Syntactic Theory of Type Generativity and
journalJ. Funct. Program. volume6,
number5 (year1996), pages667–698.

[Lindley and CheneyLindley and
authorpersonSam Lindley and personJames
Cheney. year2012.
Row-based effect types for database integration.
In booktitleProceedings of TLDI 2012: The Seventh ACM
SIGPLAN Workshop on Types in Languages Design and Implementation,
Philadelphia, PA, USA, Saturday, January 28, 2012,
editorpersonBenjamin C. Pierce (Ed.).
publisherACM, pages91–102.

[Loitsch and SerranoLoitsch and
authorpersonFlorian Loitsch and
personManuel Serrano. year2007.
Hop Client-Side Compilation. In
booktitleProceedings of the Eighth Symposium on Trends in
Functional Programming, TFP 2007, New York City, New York, USA, April 2-4.
2007. (seriesTrends in Functional Programming),
editorpersonMarco T. Morazán (Ed.),
Vol. volume8. publisherIntellect,

Meteor.js year2017.

[Murphy VII, Crary, and HarperMurphy VII
et al2007]
authorpersonTom Murphy VII, personKarl
Crary, and personRobert Harper.
Type-Safe Distributed Programming with ML5. In
booktitleTGC (seriesLecture Notes in
Computer Science), editorpersonGilles Barthe and
personCédric Fournet (Eds.), Vol. volume4912.
publisherSpringer, pages108–123.

authorpersonOlivier Nicole.
titleBringing typed, modular macros to OCaml.

[Ocsigen ToolkitOcsigen Toolkit2017]
Ocsigen Toolkit year2017.
booktitleOcsigen Toolkit.

authorpersonScott Owens.
A Sound Semantics for OCamllight. In
booktitleProgramming Languages and Systems, 17th European
Symposium on Programming, ESOP 2008, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2008, Budapest,
Hungary, March 29-April 6, 2008. Proceedings
(seriesLecture Notes in Computer Science),
editorpersonSophia Drossopoulou (Ed.),
Vol. volume4960. publisherSpringer,

[Owens, Myreen, Kumar, and TanOwens
et al2016]
authorpersonScott Owens, personMagnus O.
Myreen, personRamana Kumar, and personYong Kiam
Tan. year2016.
Functional Big-Step Semantics, See
DBLP:conf/esop/2016, pages589–615.

[Philips, De Roover, Van Cutsem, and
De MeuterPhilips et al2014]
authorpersonLaure Philips, personCoen
De Roover, personTom Van Cutsem, and personWolfgang
De Meuter. year2014.
Towards Tierless Web Development Without Tierless
Languages. In booktitleProceedings of the 2014 ACM
International Symposium on New Ideas, New Paradigms, and Reflections on
Programming & Software (seriesOnward! 2014).
publisherACM, addressNew York, NY, USA,

[Philips, Koster, Meuter, and RooverPhilips
et al2016]
authorpersonLaure Philips, personJoeri De
Koster, personWolfgang De Meuter, and personCoen De
Roover. year2016.
Dependence-driven delimited CPS transformation
for JavaScript. In booktitleProceedings of the 2016 ACM
SIGPLAN International Conference on Generative Programming: Concepts and
Experiences, GPCE 2016, Amsterdam, The Netherlands, October 31 - November
1, 2016, editorpersonBernd Fischer and
personIna Schaefer (Eds.). publisherACM,

Pumgrana year2017.

[Radanne, Papavasileiou, Vouillon, and
BalatRadanne et al2016a]
authorpersonGabriel Radanne, personVasilis
Papavasileiou, personJérôme Vouillon, and
personVincent Balat. year2016a.
Eliom: tierless Web programming from the ground
up. In booktitleIFL 2016, Leuven, Belgium, August 31 -
September 2, 2016, editorpersonTom Schrijvers
(Ed.). publisherACM, pages8:1–8:12.

[Radanne and VouillonRadanne and
authorpersonGabriel Radanne and
personJérôme Vouillon.
Tierless Web programming in the large. In
booktitleWWW 2018, Lyon, Paris.

[Radanne, Vouillon, and BalatRadanne
et al2016b]
authorpersonGabriel Radanne,
personJérôme Vouillon, and personVincent
Balat. year2016b.
Eliom: A Core ML Language for Tierless Web
Programming. In booktitleAPLAS 2016, Hanoi, Vietnam,
November 21-23, 2016, Proceedings (seriesLecture Notes in
Computer Science), editorpersonAtsushi Igarashi
(Ed.), Vol. volume10017. pages377–397.

[Rossberg, Russo, and DreyerRossberg
et al2014]
authorpersonAndreas Rossberg,
personClaudio V. Russo, and personDerek Dreyer.
F-ing modules.
journalJ. Funct. Program. volume24,
number5 (year2014), pages529–607.

[Serrano, Gallesio, and LoitschSerrano
et al2006]
authorpersonManuel Serrano, personErick
Gallesio, and personFlorian Loitsch.
Hop: a language for programming the Web 2.0.
In booktitleOOPSLA Companion. pages975–985.

[Serrano and PrunetSerrano and
authorpersonManuel Serrano and
personVincent Prunet. year2016.
A glimpse of Hopjs. In
booktitleProceedings of the 21st ACM SIGPLAN
International Conference on Functional Programming, ICFP 2016, Nara, Japan,
September 18-22, 2016, editorpersonJacques
Garrigue, personGabriele Keller, and personEijiro
Sumii (Eds.). publisherACM, pages180–192.

[Serrano and QueinnecSerrano and
authorpersonManuel Serrano and
personChristian Queinnec. year2010.
A multi-tier semantics for Hop.
journalHigher-Order and Symbolic Computation
volume23, number4 (year2010),

[Sewell, Leifer, Wansbrough, Nardelli,
Allen-Williams, Habouzit, and VafeiadisSewell et al2007]
authorpersonPeter Sewell, personJames J.
Leifer, personKeith Wansbrough, personFrancesco Zappa
Nardelli, personMair Allen-Williams, personPierre
Habouzit, and personViktor Vafeiadis.
Acute: High-level programming language design for
distributed computation.
journalJ. Funct. Program. volume17,
number4-5 (year2007), pages547–612.

authorpersonWalid Taha.
titleMulti-stage Programming: Its Theory and
thesistypePh.D. Dissertation. schoolOregon
Graduate Institute of Science and Technology.

editorpersonPeter Thiemann (Ed.).
booktitleProgramming Languages and Systems - 25th
European Symposium on Programming, ESOP 2016, Held as Part of the European
Joint Conferences on Theory and Practice of Software, ETAPS 2016,
Eindhoven, The Netherlands, April 2-8, 2016, Proceedings.
seriesLecture Notes in Computer Science,
Vol. volume9632. publisherSpringer.

authorpersonMads Tofte.
titleOperational Semantics and Polymorphic Type
thesistypePh.D. Dissertation. schoolUniversity
of Edinburgh.

Tutorial year2017.
booktitleOcsigen Tutorial.

TyXML year2017.

authorpersonJérôme Vouillon.
Lwt: a cooperative thread library. In
booktitleProceedings of the ACM Workshop on ML, 2008,
Victoria, BC, Canada, September 21, 2008,
editorpersonEijiro Sumii (Ed.).
publisherACM, pages3–12.

[Vouillon and BalatVouillon and
authorpersonJérôme Vouillon and
personVincent Balat. year2014.
From bytecode to JavaScript: the Js_of_ocaml
journalSoftware: Practice and Experience
volume44, number8 (year2014),

authorpersonPhilip Wadler.
Theorems for Free!. In
booktitleProceedings of the fourth international conference
on Functional programming languages and computer architecture, FPCA 1989,
London, UK, September 11-13, 1989,
editorpersonJoseph E. Stoy (Ed.).
publisherACM, pages347–359.

[Wright and FelleisenWright and
authorpersonAndrew K Wright and
personMatthias Felleisen. year1994.
A syntactic approach to type soundness.
journalInformation and computation
volume115, number1 (year1994),

[Yallop and WhiteYallop and White2015]
authorpersonJeremy Yallop and personLeo
White. year2015.
Modular macros.
journalOCaml Workshop (year2015).

§ THE CALCULUS

This section describes our version of the calculus, which contains the
minimal amount of ingredients that allows us to describe the extensions:
a core calculus with polymorphism, let bindings and parametrized datatypes
in the style of <cit.>,
accompanied by a fully featured module system with separate compilation
and applicative functors in the style of <cit.>.

We first present the syntax of the language in <ref> and
its type system in <ref>.
We then present the semantics of this language in
The description in this appendix is self-contained, and thus restate the
basic description found in <ref>.

§.§ Syntax

Let us first define some notations and meta-syntactic variables. As a general rule,
the expression language is in lowercase ($e$) and the module language is in
uppercase ($M$). Module types are in calligraphic letters ($\Mm$).
More precisely: $x$ are variables, $p$ are module paths, $X$ are module variables, $\tau$ are type expressions and $\type{t}$ are type constructors.
$x_i$, $X_i$ and $\type{t_i}$ are identifiers (for values, modules and types).
Identifiers (such as $x_i$) have a name part ($x$) and a stamp part ($i$) that
distinguish identifiers with the same name. Only the name part of
identifiers is exposed in module signature.
$\alpha$-conversion should keep the name intact and change only the stamp,
which allow to preserve module signatures.
Sequences are noted with a star; for example $\tau^*$ is a sequence of type expressions.
Indexed sequences are noted $(\tau_i)$, with an implicit range.
Substitution of $a$ by $b$ in $e$ is noted $\subst[]{a}{b}{e}$.
Repeated substitution of each $a_i$ by the corresponding $b_i$ is noted
The syntax is presented in <ref>.

The expression language is a fairly simple extension of
the lambda calculus with a fixpoint combinator $\Y$ and let bindings $\letin{x}{e_1}{e_2}$.
The language is parametrized by a set of constants $\Const$.
Variables can be qualified by a module path $p$.
Paths can be either module identifiers such as $X_i$,
a submodule access such as $X_i.Y$,
or a path application such as $X_i(Y_j.Z)$.
Note that, as said earlier, that fields of modules are only called by their
name, without stamp.

Types are composed of type variables $\alpha$, function types $\lamtype{\tau_1}{\tau_2}$ and
parametrized type constructors $\appty{\tau_1,\tau_2,\dots,\tau_k}{t_i}$. Type constructors
can have an arbitrary number of parameters, including zero.
Type constructors can be qualified by a module path $p$.
Type schemes, noted $\sigma$, are type expressions that are universally
quantified by a list of type variables. Type schemes can also have
free variables.
For example: $\forall\alpha. \appty{\alpha, \beta}{t_i}$.

The module language is quite similar to a simple lambda calculus: Functors are functions
over module (except that arguments are annotated with their types). Module application
is noted $\appm{\mm_1}{\mm_2}$.
Modules can also be constrained by a module type: $\constraint{\mm}{\Mm}$.
Finally, a module can be a structure which contains a list of value, types
or module definitions: $\struct{\letm[]{x_i}{2}}$.
Programs are lists of definitions.

Module types
Module types can be either the type of a functor or a signature, which contains a list
of value, types and module descriptions. Type descriptions can expose their definition
or can be left abstract.
Typing environments are simply module signatures. We note them $\Env$ for convenience.

§.§ Type system

We now present the type system. For ease of presentation, we proceed
in two steps: we will first forget that the module language exists, and
present a self-contained type system for the expression language.
We then extend the typing relation to handle modules.

§.§.§ The expression language

We introduce the following judgments:

$\wt[]{\Env}{e}{\tau}$    The expression $e$ has type $\tau$ in the environment $\Env$. See <ref>.

$\equivty[]{\Env}{\tau_1}{\tau_2}$   Types $\tau_1$ and $\tau_2$ are equivalent in environment $\Env$. See <ref>.

$\wf[]{\Env}{\tau}$    The type $\tau$ is well formed in the environment $\Env$. See <ref>.

We note $\Typeof(c)$ the type scheme of a given constant $c$.
The instanciation relation is noted $\instanceof{\tau}{\sigma}$
for a type scheme $\sigma$ and a type $\tau$.
The converse operation which closes a type according to an environment is
noted $\Close{\tau}{\Env}$.
We use $(D)\in\Env$ to test if a given type or value is declared in the environment $\Env$. Note that for types,
$(\typeabsm[]{\appty{\alpha_i}{t}})\in\Env$ holds also if $t$ is not abstract
in $\Env$.

One of the main benefit of programming language of
the family is the ability to easily define and use functions
that operate on values of various types. For example, the map function
can applies to all lists, regardless of the type of their content.
Indeed, the type of map is polymorphic:

\[\text{\ocamlc{map}}: \forall\alpha\beta.\ %
\lamtype{(\lamtype{\alpha}{\beta})}{
\lamtype{\appty{\alpha}{list}}{
\appty{\beta}{list}}}
\]

From a type checking point of view, this is possible thanks to two operations:
instanciation and abstraction.
Instanciation takes a type scheme, which is a type where some variables
have been universally quantified, and replace all the quantified type variables
by some type. It is used when looking up a variable (rule Var) or
typechecking a constant (rule Const).
For example, the type of map can be instantiated to the following type.

\[\lamtype{(\lamtype{int}{bool})}{
\lamtype{\appty{int}{list}}{
\appty{bool}{list}}}
\]

Once instantiated, the map function can be applied on
a list with concretes types.

Naturally, we also need the converse operation: constructing a type scheme given a type
containing some type variables. Closing a type depends on the current
typing environments, we only abstract type variables that have not been
introduced by previous binders. $\Close{\tau}{\Env}$ returns the type scheme
$\forall\alpha_1\dots\alpha_n.\tau$ where the $\alpha_i$ are free variables of $\tau$
that are not present in $\Env$.
While it is possible to apply the closing operation at any step of
a typing derivation, it is only useful at the introduction point of type
variables, in let bindings (rule LetIn).
In the following example, we derive a polymorphic type for a function that
constructs a pair with an element from the environment.
We first use the close operation to obtain a type scheme for $f$. Note
that since $\alpha$ is present in the environment, it is not universally
quantified. We then use the instance operation to apply $f$ to an integer

*⋮(;)(a,b)α* β
()b(a,b)βα* β

intα* int
∀β. βα* β

fintα* int

(;f∀β. βα* β)
f 3(α* int)

()fb(a,b)f 3(α* int)

Parametric datatypes

Parametric polymorphism introduces type variables in type expressions.
In the presence of type definitions, it is natural to expect
the ability to write type definitions which can contain type
variables. This leads us to parametric datatypes: datatypes
which are parametrized by a set of variables.
$\appty{\alpha}{list}$ is of course an example of such datatype.
Note that care must be taken when deciding the equivalence of types.
It the type is not abstract, its definition is available, we can
always unfold the definition, as shown in rule DefTypeEq.
However, when considering an abstract type, we cannot unfold the type
definition. Instead, we check that head symbols are compatible and
that parameters are equivalent pairwise
[This is similar to the handling of free symbols in the unification literature.]
This is done in rule AbsTypeEq.

Type validity rules – $\wf[]{\Env}{\tau}$

expression typing rules – $\wt[]{\Env}{e}{\tau}$

Type equivalence rules – $\equivty[]{\Env}{\tau}{\tau'}$

§.§.§ The module language

We introduce the following judgments:

The module $\mm$ is of type $\Mm$ in $\Env$.
See <ref>.

The module type $\Mm$ is a subtype of $\Mm'$ in $\Env$.
See <ref>.

The module type $\Mm$ is well-formed in $\Env$.
See <ref>.

The typing rules for -style modules are quite complex. In particular, the
inner details of the rules are not well known,
even by programmers. Before presenting the typing rules
in details, we will attempt to give
insight on why some features are present in the languages and what are their
advantages. For this purpose, we present two examples illustrating
the need for applicative functors and strengthening, respectively.
We assume that readers are familiar with simpler usages
of modules.

Applicative Functors
Let us consider the following scenario: we are given a module $G$
implementing a graph data-structure and would like to implement a simple
graph algorithm
which takes a vertex and returns all the accessible vertices.
We would like the returned module to contain
a function of type
How to implement $\type{set\_of\_vertices}$? An easy but inefficient way
would be to use lists.
A better way is to use proper sets (implemented with balanced binary tree,
for example).
In , this is provided in the standard library
by the functor $Set.Make$, presented in <ref>,
which takes a module
implementing comparison functions for the given type.
We would obtain a signature similar to the one below.

\begin{align*}
\end{align*}

However, this means we need to expose a complete module implementing
set of vertices that is independent from any other set module. This prevents
modularity, since any usage of our new function must use this specific
set implementation. Furthermore, this make the signature bigger than strictly
necessary. What we really want to expose is that the return type comes
from an application of $Set.Make$. Fortunately, we can do so by
using the following signature.

\begin{align*}
\end{align*}

Here, we export the fact that the set type must be the result of a functor
application on a module that is compatible with $\type{G.Vertex}$.
The type system guarantees that any such functor application
will produces types that are equivalent. In particular, if multiple libraries
uses the $Access$ functor, their sets will be of the same types, which
make composition of libraries easier. This behavior of functors is usually
called applicative.

Let us now consider the program presented in <ref>.
We assume the existence of two modules, presented in
The module $Showable$ exposes the abstract type $\type{t}$, along with
a $show$ function that turns it into a string.
The module $Elt$ exposes a type $\type{t}$ equal to
$\type{Showable.t}$ and a value that inhabits this type.

The program is presented in <ref>.
We define a functor $F$ taking two arguments $E$ and $S$ whose signature
are similar to $Elt$ and $Showable$, respectively.
The main difference is that $E$ comes first and $\type{S.t}$ is defined as an
alias of $\type{E.t}$. The functor uses the $show$ function on the element
in $E$ to create a string.

It is natural to expect the functor application $F(Elt)(Showable)$ to
type check, since $\type{Elt.t} = \type{Showable.t}$. We must, however,
check for module inclusion. While $Elt$ is clearly included in the
signature of the argument $E$, the same is not clear for $Showable$.
We first need to enrich its type signature with additional type equalities.
We give $Showable$
the type $\signature{\typem[]{t}{Showable.t}\ \dots}$. It makes sense to enrich
the signature in such a manner since $Showable$ is already in the environment.
Given this enriched signature, we can now deduce that
$\submod[]{}{(\typem[]{t}{Showable.t})}{(\typem[]{t}{E.t})}$ since
$\type{E.t} = \type{Elt.t} = \type{Showable.t}$.

\begin{align*}
\end{align*}

Typing environment

\begin{align*}
&\mathtt{module}\ F\\
&\quad(E:\signature{\typeabsm[]{t}\ \valm[]{v}{t}})\\
\ \valm[]{show}{\lamtype{t}{string}}})\\
& = \mathtt{struct}\\
\end{align*}

Application of multi-argument functor using manifests

Program using functors and manifest types

The operation that consists in enriching type signatures of module identifiers
with new equalities by using elements in the environment is called
strengthening <cit.>.

§.§.§ Typing rules

In the previous two examples, we showcased some delicate interactions
between functor, type equalities and modularity in the context of an
module system. We now see in details how the rules
presented in <ref>
produce these behaviors.

Qualified access
Unqualified module variables are typechecked in a similar manner than
regular variables in the expression language, with the ModVar
typing rule. Qualified access (of the form $X.a$), both for the core and the module language,
need more work.

As with the expression language, the typing environment is simply
a list of declaration. In particular, typing environments do not store paths.
This means that in order to prove $\wt[]{\Env}{p.a}{\tau}$, we must
first verify that the module $p$ typechecks in $\Env$: $\wtm[]{\Env}{p}{\Mm}$.
We then need to verify that the module type $\Mm$ contains a declaration

This is done in the QualModVar rule for the module language.
The rules for the expression language are given
in <ref>.

Let us now try to apply these rules to the module $X$ with the following
module type. $X$ contains
a type $t$ and a value $a$ of that type. We note that module type $\Xm$.

X: t; at

We wish to typecheck $X.a$. One expected type for this expression is $X.t$.
However, the binding of $v$ in $\Xm$ gives the type $t$, with no mention of
$X$. We need to prefix the type variable $t$ by the access path $X$.
This is done in the rule QualModVar by the substitution
$\substs[]{n_i}{p.n}{\bv[]{\Sm_1}}{\Mm}$ which prefixes all the bound variables of $\Sm_1$, noted $\bv[]{\Sm_1}$, by the path $p$. Note here that we substitute
only by the names declared before the variable $a$. Indeed, a variable
or a type can only reference names declared previously in .
To prove that $X.a$ has the type $X.t$,
we can write the following type derivation.

*[Left=QualVar, Right=with $X.t = \subst[]{t}{p.t}{t}$]
Xt; at

The strengthening operation, noted $\strengthen{\Mm}{p}$, is defined in
<ref> and is used in the Strength rule.
It takes a module type $\Mm$ and a path $p$ and returns a module type $\Mm'$
where all the type declarations, abstract or not, have been replaced by
type aliases pointing to the path $p$.
These type aliases are usually called “manifest types”.

This operator relies on the following idea:
if $p$ is of type $\Mm$, then $p$ is available in the
environment. In order to expose as many type equalities as possible,
it suffices to give $p$ a type where all the type definition point to
definitions available in the environment. This way, we preserve type
equalities even for abstract types. This also mean that type equalities
can be deduced by only looking at the path and the module type. In
particular, we do not need to look at the implementation of $p$,
which is important for the purpose of separate compilation.

Applicative functors

Let us consider a functor $F$ with the following type. It takes
a module containing a single type $t$ and return a module containing
an abstract type $t'$ and a conversion function.

F: X

If we consider two modules $X_1$ and $X_2$, does $X_1 = X_2$ imply
$F(X_1).t = F(X_2).t$ ? If that is the case, we say that functors are
applicative. Otherwise, they are generative
[SML only supports generative functors. originally
only supported applicative functors, but also supports the generative
behavior since version 4.03.].
Here, we consider the applicative behavior of functors.
This is implemented with the last strengthening
rule which ensures that the body of functors is also strengthened.
For example, if $\Mm$ is the type of the functor above, $\Mm/F$ is the following
module type:

This justifies the presence of application inside paths. Otherwise, such
type manifests inside functors could not be represented.
A more type-theoretic description of generative and applicative functors can be found in <cit.>.

Separate compilation

Separate compilation is an important properties of programming languages.
In fact, almost all so-called “mainstream” languages support it.
We can distinguish two aspects of this property:
separate typechecking and separate code generation.
In both cases, it means that in order to process the file
(either to type check it or to transform it into another representation),
we only need to look at the type of its dependencies, not their

It turns out that the module system with manifest types lends itself
very well to separate typechecking <cit.>. Indeed, let us consider
a program as a list of modules. Each module represents a compilation
unit (a file). Since module bindings in the typing environment only
contains module types, and not the actual module, typechecking a file only
needs the module type of the previous files, which ensure that we can
typecheck each file separately, as long as all its dependencies
have been typechecked before. This is expressed more formally
in <ref>.

Given a list of module declarations that form a typed program, there exists
an order such that each module can be typechecked with only knowledge
of the type of the previous modules.

More formally,
given a list of $n$ declarations $\dm_i$ and a signature $\Sm$ such that

\[\renewcommand\added\addedhide
\wtm{}{(\dm_1;\dots;\dm_n)}{\Sm}
\]

then there exists $n$ definitions $\Dm_i$ and a permutation $\pi$ such that

\begin{align*}
\forall i < n,\ &
\wtm[]{\Dm_{1};\dots;\Dm_{i}}{\dm_{i+1}}{\Dm_{i+1}}&
\submod[]{}{\Dm_{\pi(1)};\dots;\Dm_{\pi(n)}}{\Sm}
\end{align*}

It is always possible to reorder declarations in a signature using the
SubStruct rule. This means we can choose the appropriate permutation of
definitions that matches the order of declarations. The rest follows by definition
of the typing relation.

Module typing rules – $\wtm[]{\Env}{m}{\Mm}$

Module subtyping rules – $\submod[]{\Env}{\Mm}{\Mm'}$

Module type validity rules – $\wfm[]{\Env}{\Mm}$

Additional typing rules for the expression language

Module strengthening operation – $\strengthen{\Mm}{p}$

§.§ Semantics

We now define the semantics of our language. We use a rule-based
big step semantics with traces. Traces allows us to reason
about execution order in a way that is compatible with modules, as
we will see in <ref>.

We note $v$ for values in the expression language and $\vm$ for values
in the module language. Values are defined in <ref>.
Values in the expression language can be either constants or lambdas.
Module values are either structures, which are list of bindings of
values, or functors.

We note $\envr$ the execution environment. Execution environments
are a list of value bindings. Note here that the execution environment
is not mutable, since reference cells are not in the language. We
note the concatenation of environment $+$. Environment access is noted
$\bdrin{x}{v}{\envr}$ where $x$ has value $v$ in $\envr$.
The same notation is also used for structures.

Traces are lists of messages. For now, we consider messages
that are values and are emitted with a $\print$ operation.
The empty trace is noted $\niltr$. Concatenation of traces is noted $\ctr$.

Given an expression $e$ (resp. a module $m$), an execution
environment $\envr$, a value $v$ (resp. $\vm$) and a trace $\trace$,

\[\renewcommand\added\addedhide
\redto{\envr}{e}{v}{\trace}
\]

means that $e$ reduces to $v$ in $\envr$ and prints $\trace$.
The reduction rules are given in <ref>.

The rules for the expression language are fairly traditional.
Variables and paths must be resolved using the Var and QualVar
rules. Applications are done in two steps: first, we reduce both
the function and the argument with the App rule,
then we apply the appropriate reduction
rule for the application: Beta for lambda expressions, Y for
fixpoints and Delta for constants.
The $\delta$ operation gives meaning to application of a constant
to a value. $\appconst[]{c}{v} = v', \trace$ means that $c$ applied to $v$
returns $v'$ and emits the trace $\trace$. Let bindings
are treated in a similar manner than lambda expressions: the left
hand side is executed, added to the environment, then the right hand side
is executed.

The module language has similar rules for identifiers and application.
In this case, the Beta and App rule have been combined in
ModBeta. Additional rules for declarations are also present.
Type declarations are ignored (TypeDecl). Values and module
declarations (ValDecl and ModDecl) are treated similarly
to let bindings: the body of the binding is executed, added to the environment
and then the rest of the structure is executed.

§.§.§ Traces and Printing

Traces allow us to visualize the execution order of programs. In
particular, if we prove that code transformation preserves traces,
it ensures that the execution order is preserved.
Traces allow us to reason about execution without introducing
references and other side-effecting operations in our language, which
would make the presentation significantly more complex.

One example of operation using traces is the $\print$ constant.
Typing and semantics of $\print$ are provided in <ref>.
$\print$ accepts any value, prints it, and returns it. From a typing
point of view, $\print$ has the same type as the identity: a polymorphic function
which returns its input. We make use of the fact
that the Const typing rule also uses the instanciation for type schemes.
The semantics of $\print$ is provided via the Delta rule: it returns its argument
directly but also emits a trace containing the given argument.

() = ∀α.(αα)

v = v, v

Typing and execution rules for $\print$

We now present an example using $\print$.
We assume the existence of the type
$\intty$, a set of constant corresponding to the integers
and an associated operation $+$.
We wish to type and execute the expression $e$ defined as $\mye$

Let us first show that $e$ is of type $\intty$. The type derivation is provided
in <ref>. The typing derivation is fairly direct:
we use the Const rule to type $\print$ as $\lamtype{\intty}{\intty}$
and apply it to integers with the rule App.

We can now look at the execution of $e$, which returns $4$
with a trace $\singltr{3;4}$. The execution derivation is shown in
<ref>. The first step is to decompose the let-binding.
We first reduce $\app{\print}{3}$, which can be directly done with
the Delta rule. This gives us $3$ with a trace $\singltr{3}$.
We then reduce $\app{\print}{(x+1)}$ in
the environment where $x$ is associated to $3$.
Before resolving the application of $\print$ with the Delta rule,
we need to reduce its argument with the $\mysc{App}$ rule.
We obtain $4$ with a trace $\singltr{4}$.
We return the result of the right hand side of the left and the concatenation
of both traces by usage of the LetIn rule,
which gives us $4$ with a trace $\singltr{3;4}$.

*[Left=LetIn, Right=LetIn]

*⋮ x+1

Typing derivation for $e$ – $\wt{}{e}{\intty}$

*[Left=Let, Right=Let]
3 = 3, 3

4 = 4, 4

Execution derivation for $e$ – $\redto{}{e}{4}{\singltr{3;4}}$

§.§.§ Modules

We now present an example of reduction involving modules. Our example
program $\Pm$ is presented in <ref>. It consists of
two declarations: a module declaration $X$ which contains a single
declaration $a$, and the return value of the program, which is equal to
$X.a$. It is fairly easy to see that the program $\Pm$ return a value
of type $\intty$, hence we focus on the execution of $\Pm$, which
is presented in <ref>.

The derivation is slightly simplified for clarity. In particular, rules
such as EmptyStruct are elided.
The first step is to apply the Program and ModuleDecl
rules in order to execute the content of each declaration.
The declaration of $X$, on the left side, can be reduced by
first applying the Struct rule in order to extract the
content of the module structure, then ValDecl, to reduce
the declaration of $a$. These reductions give us the structure
value $\bdr{a}{3}$.
We now execute the declaration of $\ret$. According to the ModuleDecl
rule, we must do so in a new environment containing $X$: $\bdr{X}{\bdr{a}{3}}$.
In order to reduce $X.a$, we must use the QualModVar rule, which reduces
qualified variables. This means we first reduce $X$, which according
to the environment gives us $\bdr{a}{3}$, noted $V$.
We then look up $a$ in $V$, which returns $3$.
To return, we first compose the resulting structure value from both
declaration: $\bdr{X}{\bdr{a}{3}}+\bdr{\ret}{3}$.
We then lookup $\ret$ in this structure, which gives us $3$.

\begin{align*}
\end{align*}

The program $\Pm$

Execution of $\Pm$

Example of execution with modules

Big step semantics – $\redto{\envr}{e}{v}{\trace}$

§.§.§ Notes on Soundness

Soundness properties, which correspond to the often misquoted
“Well typed programs cannot go wrong.”, have been proven for many variants
of the language.
Unfortunately, stating and proving the soundness property for big step semantics
and modules requires a fairly large amount of machinery which
we do not attempt to provide here.
Instead, we give pointers to various relevant work containing such proofs.

Soundness for a small step semantics of our expression language is
provided by <cit.>.
At a larger scale, <cit.> proves
the soundness of a small step semantics for a very large portion of the
expression language using the Locally Nameless Coq framework
Soundness of a big step semantics has been proved and mechanized for several
richer languages

Unfortunately, as far as we are aware, soundness of Leroy's module language
with higher order applicative functors has not be proved directly and is a fairly
delicate subject.
The most recent work of interest is <cit.>, which presents
an elaboration scheme from modules, including applicative -style
modules, into System $F_\omega$. Soundness then relies on soundness of
the elaboration (provided in the article) and soundness of System $F_\omega$.
In this work, the applicative/generative behavior of functors is decided
depending on its purity, which is much more precise than what
is done in .

§ SEMANTICS PRESERVATION

We now prove <ref> which states that
given an program $\Pm$, the trace of its execution is the same
as the concatenation of the traces of $\compile{s}{\Pm}$ and
$\compile{c}{\Pm}$. More formally:

Given sets of constants where converters are well-behaved,
given an program $\Pm$ respecting the slicability hypothesis and
such that
$ \redp{\emptyr}{\Pm}{v}{\trace} $

\begin{align*}
\redmls{\emptyr}{\compile{s}{\Pm}}{()}{\envfrag}{\envinj}{\trace_s}&&
\redmlc{\emptyr}{\compile{c}{\Pm}}{v}{\envfrag}{\envfrag'}{\envinj}{\envg}{\trace_c}&&
\trace = \trace_s\ctr\trace_c
\end{align*}

§.§ Hoisting

In <ref>, we mentioned that a useful property
of injections and fragments is that they can be partially lifted
outside sections.
This property can be used to simplify the simulation proofs.
We consider the code transformation that hoists the content of injections
out of fragments, client declarations and mixed functors in a way
that preserve semantics. This transformation can be decomposed
in two parts.

We decompose injections inside fragments and client declarations into simpler
For example, the piece of code presented in <ref>
is decomposed in <ref> by moving out the application
of the converter and leaving only a call to the $\serial$ converter.
All injections using a converter than is not $\serial$ nor $\fragment$
can be decomposed in such a way.

Since injections
can only be used on variables or constants and that no server bindings can be
introduced inside a fragment, scoping is preserved.
Furthermore, by definition of converters and their client and server
components, this transformation preserves typing.

It also preserves the dynamic semantics as long as the order
of hoisting correspond to the order of evaluation. This can be
seen by inspecting the reduction relation for server code under client
contexts $\pred{}_{c/s}$.

Finally, it trivially preserves the semantics of the compiled program since
it corresponds exactly to how converters are decomposed during compilation.

\begin{align*}
&\letin{a}{1 + 2}{}\\
&\cv{3 + \injf{a}{\intty}}
\end{align*}

Fragment with injections

\begin{align*}
&\letin{a}{1 + 2}{}\\
&\cv{3 + \app{\intty^c}{\injf{a'}{\serial}}}
\end{align*}

Fragment with hoisted injections

Hoisting on fragments

This allows us to assume that reduction of server code in client context
only uses variable lookup and never leads to any evaluation.
In particular, this will avoid having to deal with the case
of fragments being executed inside the reduction of another fragment (to
see why this could happen, consider the case of a converter
of type

In the rest of this section, we assume that reductions of the rule
Fragment are always of the following shape:

e = []x_if_i_s(x_i)e
and  f_i∈{,}

and that reductions of the rule ClientDecl
are always of the following shape:

_c = []x_if_i_s(x_i)_c
and  f_i∈{,}

Injections inside mixed modules

We also hoist injections completely out of mixed contexts to the outer
englobing scope.
For example in the functor presented in <ref>,
we can lift the injection out of the functor, as show in
This is valid since injections can only reference
content outside of the functor, by typing.
Semantics is similarly preserved since injections inside functors
are reduced immediately when encountering a functor, as per rule
ModClosure in <ref>.

This allows us to assume that the reduction of a mixed module
will never lead to the reduction of an injection.

\begin{align*}
\end{align*}

Mixed functor with injections

\begin{align*}
\end{align*}

Mixed functor with hoisted injections

Hoisting on mixed modules

§.§ Preliminaries

Let us start with some naming conventions.
Identifiers with a hat, such
as $\co\envg$, are related to the compiled semantics. For example,
while the server environment for the interpreted semantics
is noted $\envr_s$, the environment for the execution of the target
language is noted $\co\envr_s$.
This naming convention is only for ease of reading and does not apply
a formal relation between the objects with and without hats, unless
indicated explicitly.

§.§.§ Remarks about global environments

Let us make some preliminary remarks about global environments in the client generated programs and in .

Given a global environment $\envg$ resulting of $\pred{}_c$,
it contains only two kinds of references:

* Closure fragments, noted $\rf{f}$, which come from the
execution of $\pbind\ \mathtt{env}$.
The associated value is always a environment (a signature).

* Fragment values, noted $\rf{r}$, which come from the execution of
$\pbind\ \mathtt{with}$.

In the rest of this section, we consider that we can always
decompose global environments $\envg$ in two parts:
a fragment value environment $\envg_r$ containing all the references
$\rf{r}$ that were produced by $\pbind\ \mathtt{with}$ and
a fragment closure environment $\envg_f$ containing
only binding of the form $\bdr{\rf{f}}{\envr}$ that were produced by
$\pbind\ \mathtt{env}$.

Similarly, given a global environment $\co\envg$ used in .
There are only three kind of references:

* Closure fragments, noted $\rf{f}$, which come from the slicing of syntactic
fragments in the source program.
The associated value is always a closure.

* Fragment values, noted $\rf{r}$ come from the execution of
fragments in the fragment queue.

* Injections, noted $\rf{x}$. The associated values
must be serializable, and hence
can only be references or constants in $\Const_\base$.

In the rest of this section, we consider that we can always decompose global
compiled environment $\co\envg$ into
a fragment closure environment $\co\envg_f$, a fragment value environment
$\co\envg_r$ and an injection environment $\envinj$.

§.§.§ Client equivalence

Given $v$ an client value, $v'$ an value
and $\envinj$ an environment of references,
$v$ and $v'$ are equivalent under $\envinj$,
noted $v \equivc{\envinj} v'$, if and only if they are equals after
substitution by $\envinj$: $\substenv{\envinj}{v} = \substenv{\envinj}{v'}$.

We extend this notation to environments and traces.

We say that an global environment
$\envg = \envg_f\cup\envg_r$
and an global environment
$\co\envg = \co\envg_f\cup\co\envg_r\cup\envinj$
are synchronized if and only if the following conditions hold.

* The reference environments are equivalent:

* The domains of $\envg_f$ and $\co\envg_f$ coincides, and:

* For each $\rf{f}$ in these environments such that
$\bdrin{\rf{f}}{\envr}{\envg_f}$ and that
$\bdrin{\rf{f}}{\closure{x_0\dots x_n}{\co{\envr}}{e}}{\co\envg_f}$, then
the following property must hold.

We must have that $\envr\equivc{\envinj}\co\envr$ and that
for all $v_0,\dots,v_n$, $\co v_0,\dots,\co v_n$ such that
for all $i$, $v_i\equivc{\envinj}\co{v}_i$;

\begin{align*}
\redc{\envr}{\subst[]{x_i}{v_i}{e}_i}{v}
\implies
\redmlce{}
{\app{\closure{\overline{x}_i}{\co{\envr}}{e}}{\co{v}_0\dots \co{v}_n}}
\end{align*}

with $v\equivc{\envinj}\co{v}$ and $\trace\equivc{\envinj}\co{\trace}$

* For each $\rf{F}$ in these environments such that
$\bdrin{\rf{F}}{\envr}{\envg_f}$ and that
{\co\envg_f}$, we have $\envr\equivc{\envinj}\co\envr$.

We consider that $\co\envg_f$ is a fragment closure environment for
the server expression $e_s$, noted $FCE(\co\envg_f,e_s)$, if
for each $\bdr{\rf{f}}{\closure{\overline{x}_i}{\co\envr}{e'}}$ in
$\co\envg_f$, for each $\cv{e}_{\rf{f}}$ in $\frags{e_s}$
we have $e' = \subst[]{\injf{x_i}{f_i}}{x_i}{e}_i$.

We consider that $\co\envg_f$ is a functor closure environment for
the module expression $\mm$, noted $FCE(\co\envg_f,\mm)$, if
for each $\bdr{\rf{F}}{\functorenvi{\co\envr}{Y}{\Mm}{\co\sm}}$ in
$\co\envg_f$, for each $(\struct{\sm}_{\rf{F}})$ in $\mm_s$
we have $\co\sm = \compile{c}{\sm}$. Additionally, we require
that $\co\envg_f$ be a fragment closure environment
for each expression contained in $\sm$.

In the rest of this section, we use the same notation for both properties.
We extend this notation to server declarations, server values
(by looking under closures) and server environments.

Given $\envr$, $\co\envr$,
$\envg = \envg_f\cup\envg_r$,
$\co\envg = \co\envg_f\cup\co\envg_r\cup\envinj$,
$e$ and $\co e$
such that:

\begin{align*}
\envr&\equivc{\envinj}\co\envr
&e[\envinj] &= \co e[\envinj]
\end{align*}

Then we have:

\begin{align*}
&v&\equivc{\envinj}\co v
\end{align*}

The only difference between client expressions and
expressions are the presence of extra references for injections
in . Indeed, syntactic injections have been removed either
by the server execution or by compilation and $\bindg$ constructs
are only accessible at the module level. Since we assume
that the original expression $e$ and the compiled expression $\co e$
are the same up to the injection environment $\envinj$, we can
trivially mimic the execution of $e$ in $\co e$ by induction.

§.§.§ Server equivalence

Given $v$ an server value, $\co v$ an value.
We say they are equivalent, noted $v\equivs{}\co v$ if
and only if

\begin{align*}
\substfrag{v} &= \co v
&\text{ where $\overline{x_{i,j}} = \injs{e_i}$}
\end{align*}

We extend this notation to environments and traces.

§.§ Server expressions and structures

We first look at server expressions and structures.
By definition of the server reduction relation for ,
the emitted program is a series of binds.

We consider an server expression $e$;
the environments $\envr_s$, $\envr_c$ and
$\envg = \envg_f\cup\envg_r$;
the target environment $\co\envr_s$, $\co\envr_c$ and
$\co\envg = \co\envg_f\cup\co\envg_r\cup\envinj$.

If the expression $e$ has valid server and client executions:

\begin{align*}
\redel[s]{\envr_s}{e}{v}{\clientprog}{\trace_s}
\end{align*}

and the following invariants hold:

\begin{align*}
\co\envr_c &\equivc{\envinj}\envr_c&
\co\envr_s &\equivs{}\envr_s&
\co\envg &\equivc{}\envg&
\end{align*}

Then $\co e = \substfrag{e}$ has an equivalent execution.

with the following invariants:

\begin{align*}
\co\envg'&\equivc{}\envg'&
% \co\envg&\subset\co\envg'&
\co v&\equivs{} v&
\co\trace_s&\equivs{}\trace_s&
\co\trace_c&\equivc{\envinj}\trace_c
\end{align*}

We consider an expression $e$;
the environments $\envr_s$, $\envr_c$ and
$\envg = \envg_f\cup\envg_r$;
the target environment $\co\envr_s$, $\co\envr_c$ and
$\co\envg = \co\envg_f\cup\co\envg_r\cup\envinj$.
such that

\begin{align*}
\co\envg&\equivc{}\envg&
\co\envr_c &\equivc{\envinj}\envr_c&
\co\envr_s &\equivs{}\envr_s&
\end{align*}

We will proceed by induction over the executions of $e$ and $\clientprog$.
The only case of interest is when the server expression is a fragment.

[Case $\cv{e}_{\rf{f}}$]
* We assume that the following executions hold:

$\noinj{e} =
\substi[]{\injf{x_i}{f_i}}{\injval{v_i}}{e}$ and
$\envg' = \envg\cup\bdr{\rf{r}}{v_c}$.
We have $\co e$ equal to $\pfragment{\rf{f}}{x_1\dots x_n}$.

We first consider the execution of $\co e$.
We can easily
construct the following execution.

f v_1…v_n

By hypothesis, for each $i$, $v_i\equivs{\co\envg}\co{v}_i$.
This gives us that
We trivially have that

Let us now look at the client execution.
By client execution of $\clientprog$, $\bdrin{\rf{f}}{\envr}{\envg}$.
Since $\envg\equivc{\envinj}\co\envg$, we have
$\bdr{\rf{f}}{\closure{x_0\dots x_n}{\co{\envr}}{e'}}\in\co\envg$
and $\envr\equivc{\co\envg}\co\envr$.
Furthermore, since $\fragenv{\co\envg_f,\cv{e}_{\rf{f}}}$, we
know that that $e' = \substi[]{\injf{x_i}{f_i}}{x_i}{e}$.
We have by hypothesis that
Since $\noinj{e} = \subst[]{x_i}{\injval{v_i}}{e'}$
and since for all $i$, $\injval{v}_i\equivc{\co\envg}\injval{\co{v}}_i$,
we can use <ref> to build the following reduction:

f v_1…v_n

f v_1…v_n

Where $\co\envg' = \co\envg\cup\bdr{\rf{r}}{\co{v}}$.
By <ref>, we have
that $v\equivc{\co\envg}\co{v}$ and
The only part that is changed in $\envg'$ and $\co\envg'$ is
the fragment reference environment, hence we easily have that
$\co\envg'\equivc{}\envg'$, which concludes.

[Other cases]
* In other cases, we first note that references manipulated
inside server code can only fragment references $\rf{r}$.
By hypothesis, the same references are considered before and
after compilation. Since the fragment closure environment
hypothesis ranges over all server expressions, including the one
in closures, it is easy to preserve it during execution.
The rest is a very simple induction.

We consider an server declaration $\dm_s$;
the environments $\envr_s$, $\envr_c$ and
$\envg = \envg_f\cup\envg_r$;
the target environment $\co\envr_s$, $\co\envr_c$ and
$\co\envg = \co\envg_f\cup\co\envg_r\cup\envinj$.

If the expression $e$ has valid server and client executions:

\begin{align*}
\redel[s]{\envr_s}{\dm}{\vm}{\clientprog}{\trace_s}
\end{align*}

and the following invariants hold:

\begin{align*}
\co\envr_c &\equivc{\envinj}\envr_c&
\co\envr_s &\equivs{}\envr_s&
\co\envg &\equivc{}\envg&
\end{align*}

Then $\co\dm = \substfrag\dm$ have an equivalent execution.

with the following invariants:

\begin{align*}
\co\envg'&\equivc{}\envg'&
% \co\envg&\subset\co\envg'&
\co\vm&\equivs{}\vm&
\co\trace_s&\equivs{}\trace_s&
\co\trace_c&\equivc{\envinj'}\trace_c
\end{align*}

§.§ Mixed structures

We consider a slicable structure $\sm$;
the environments $\envr_s$, $\envr_c$ and
$\envg = \envg_f\cup\envg_r$;
the target environment $\co\envr_s$, $\co\envr_c$ and
$\co\envg = \co\envg_f\cup\co\envg_r\cup\envinj$.

If the structure has valid server and client executions:

\begin{align*}
\redx{\envr_s}{\sm}{\vm_s}{\clientprog}{\trace_s}
\end{align*}

and the following invariants hold:

\begin{align*}
\co\envr_c &\equivc{\envinj}\envr_c&
\co\envr_s &\equivs{}\envr_s&
\co\envg &\equivc{}\envg&
\end{align*}

then for any $\envfrag$,
the compiled structures have equivalent executions

\begin{align*}
\redmls{\co\envr_s}{\compile{s}{\sm}}{\co\vm_s}
\end{align*}

with the following invariants:

\begin{align*}
\co\envg' &\equivc{}\envg'&
\co\vm_s&\equivs{}\vm_s&
\co\trace_s&\equivs{}\trace_s\\
\fragenv{&\co\envg_f',\vm_s}&
\co\vm_c&\equivc{\co\envg'}\vm_c&
\co\trace_c&\equivc{\co\envg'}\trace_c
\end{align*}

We consider a slicable structure $\sm$;
the environments $\envr_s$, $\envr_c$ and
$\envg = \envg_f\cup\envg_r$;
the target environment $\co\envr_s$, $\co\envr_c$ and and
$\co\envg = \co\envg_f\cup\co\envg_r\cup\envinj$.
such that

\begin{align*}
\co\envr_c &\equivc{\co\envg}\envr_c&
\co\envr_s &\equivs{}\envr_s&
\co\envg &\equivc{}\envg&
\end{align*}

We will now proceed by induction over the execution of $\sm$.

[Case $\sm = \dm_b;\sm'$ – Base declaration]
* We assume that the following executions hold:

Let us consider the executions of $\dm_\base$.
By definition of base, it contains neither injections nor fragments.
By <ref>,
and $\redc{\envr_c}{\dm_b}{\vm_b}{\trace_c}{\envg}{\envg}$ both
correspond to $\redel[]{\envr_s}{\dm_\base}{\vm_s}{\emptym}{\trace_s}$
and $\redel[]{\envr_c}{\dm_\base}{\vm_c}{\emptym}{\trace_c}$ respectively.
By definition, base fragments can't be present, hence
we also have $\fragenv{\co\envg_f,\vm_s}$

Additionally, the compilation functions are the identity on base, which mean
that $\compile{s}{\dm_b}$ and $\compile{c}{\dm_b}$ contains only constructs.
The reduction relation over and coincide with the one on the
fragment of the language. Hence, for any $\envfrag$, we have

\begin{align*}
\co\vm_s&\equivs{}\vm_s&
\co\vm_c&\equivc{\co\envg}\vm_c&
\co\trace_s&\equivs{}\trace_s&
\co\trace_c&\equivc{\co\envg}\trace_c
\end{align*}

Let us consider the execution of $\sm'$ and $\clientprog$.
We easily have the following properties:

\begin{align*}
\co\envr_c+\co\vm_c &\equivc{\envinj}\envr_c+\vm_c&
\co\envr_s+\co\vm_s &\equivs{}\envr_s+\vm_s&
\co\envg &\equivc{}\envg&
\end{align*}

hence, by induction on the execution of $\sm'$ and $\clientprog'$, we have
{\envfrag_\bullet \cfrag \envfrag}{\envfrag}
for any $\envfrag$,

\begin{align*}
\co\envg' &\equivc{}\envg'&
\co\vm'_s&\equivs{}\vm'_s&
\co\trace_s&\equivs{}\trace_s\\
\fragenv{&\co\envg_f',\vm'_s}&
\co\vm'_c&\equivc{\co\envg'}\vm'_c&
\co\trace'_c&\equivc{\co\envg'}\trace'_c
\end{align*}

We can then build the following derivations:

_c   _c+_cc''_c

and the following invariants are easily verified:

\begin{align*}
\co\envg' &\equivc{}\envg'&
\co\vm_s+\co\vm'_s&\equivs{}\vm_s+\vm'_s&
\co\trace_s\ctr\co\trace'_s&\equivs{}\trace_s\ctr\trace'_s\\
\fragenv{&\co\envg_f',\vm_s+\vm'_s}&
\co\vm_c+\co\vm'_c&\equivc{\co\envg'}\vm_s+\vm'_c&
\co\trace_c\ctr\co\trace'_c&\equivc{\co\envg'}\trace_c\ctr\trace'_c
\qedhere
\end{align*}

[Case $\sm = \dm_s;\sm'$ – Server declaration]
* We assume that the following executions hold:

Let us note $\cv{e_i}_{\rf{f_i}}$ the fragments syntactically present
in $\dm_s$.
let us note $\cv{e_j}_{\rf{f_j}}$ the fragments executed during the reduction of
$\dm_s$ and $\rf{r_j}$ the associated fresh variables.

We have the following compilations:

\begin{align*}
\compile{s}{\dm_s;\sm'}
&= \substi[]{\cv{e_i}_{\rf{f_i}}}{\pfragment{\rf{f}_i}
\pend;\compile{s}{\sm'}\\
\compile{c}{\dm_s;\sm'}
&=\left( \bindg \rf{f}_i =
\lam{\overline{x_{i,k}}}
\right)_i;
\pexec;\compile{c}{\sm'}
\end{align*}

After hoisting, converters can only be the $\serial$ or $\fragment$. Its
server and client parts are the identity, hence we simply omit them.
We also note that $\compile{s}{\dm_s}$ differs with $\dm_s$ only
on type annotations and type declarations which are ignored by reduction
relations. We note
$\co\dm_s = \substi[]{\cv{e_i}}{\pfragment{\rf{f}_i}

Let us consider the reduction of
Let us note $e'_i = \subst[]{\injf{x_{i,j}}{f_{i,j}}}{x_{i,j}}{e_i}$.
For any queue $\envfrag$, we have the following reduction:

where $\co\envg_1 = \co\envg$ and
$\co\envg_{i+1} = \co\envg_i\cup
\bdr{\rf{f_i}}{\closure{x_1\dots x_m}{\co{\envr_c}}{e'_i}}$.
Let $\envg_{bind}$ be
$\bdr{\rf{f_i}}{\closure{x_1\dots x_m}{\co{\envr_c}}{e'_i}}_i$.
We note $\co\envg' = \co\envg_{n+1} = \co\envg \cup \envg_{bind}$
$\co\envg'_f = \co\envg_f\cup \envg_{bind}$.

we have $\envg' = \envg\cup\bdr{\rf{f_i}}{\envr_c}_i$.
and $\envr_c\equivc{}\co\envr_c$, we have that
Furthermore, given one of the $\rf{f_i}$ in $\envg_{bind}$, each fragment
annotated with this $\rf{f_i}$ syntactically appear in $\dm_s$ by
uniqueness of the annotation function.
This also holds inside functors, since
each $\rf{f_i}$ will be prefixed by a unique module reference.
Hence $\fragenv{\co\envg'_f,\dm_s}$
and $\fragenv{\co\envg'_f,\envr_s}$.

We now have all the ingredients to uses <ref> on
the execution of $\dm_s$ and $\clientprog$.
This gives us the following reductions:

with the following invariants:

\begin{align*}
\co\envg''&\equivc{}\envg''&
% \co\envg&\subset\co\envg'&
\co\vm&\equivs{}\vm&
\co\trace_s&\equivs{}\trace_s&
\co\trace_c&\equivc{\envinj}\trace_c
\end{align*}

We remark that $\envinj'' = \envinj$ since no injection
took place during a server section and that $\co\envg_f'' = \co\envg_f'$,
by definition of the reduction for $\dexec$.

We now consider the execution of $\sm'$.
The following invariants holds:

\begin{align*}
\co\envr_c &\equivc{\envinj}\envr_c&
\co\envr_s+\co\vm_s &\equivs{}\envr_s+\vm_s&
\co\envg'' &\equivc{}\envg''&
\end{align*}

By induction on the execution of $\sm'$ and $\clientprog'$, we have
{\envfrag'_\bullet \cfrag \envfrag'}{\envfrag'}

\begin{align*}
\co\envg''' &\equivc{}\envg'''&
\co\vm'_s&\equivs{}\vm'_s&
\co\trace'_s&\equivs{}\trace'_s\\
\fragenv{&\co\envg_f''',\vm'_s}&
\co\vm'_c&\equivc{\co\envg'}\vm'_c&
\co\trace'_c&\equivc{\co\envg'}\trace'_c
\end{align*}

Finally, we can construct the following executions:

$\envfrag = \envfrag_\bullet\cfrag\dend\cfrag
\envfrag'_\bullet\cfrag\envfrag'$ and
$\co\clientprog = (\bind{\rf{f}_i}{\lam{\overline{x}_i}{e'_i}})_i$.
We verify the following invariants:

\begin{align*}
\co\envg''' &\equivc{}\envg'''&
\co\vm_s+\co\vm'_s&\equivs{}\vm_s+\vm'_s&
\co\trace_s+\co\trace'_s&\equivs{}\trace_s+\trace'_s\\
\fragenv{&\co\envg_f''',\vm_s+\vm'_s}&
\co\vm'_c&\equivc{\co\envg'''}\vm'_c&
\co\trace_c+\co\trace'_c&\equivc{\co\envg'''}\trace_c+\trace'_c
\qedhere
\end{align*}

[Case $\sm = \dm_c;\sm'$ – Client declaration]

We assume that the following executions hold:

Let us note  $\injf{x_i}{f_i}$ the injections in $\dm_c$ and
$\rf{x}_i$ the associated fresh variables.
Since hoisting has been applied, all the $f_i$ are either $\serial$
or $\fragment$. Furthermore, no fragments are executed due to the
execution of injections and
$\noinj{\dm_c} = \substi[]{\injf{x_i}{f_i}}{\envr_s(x_i)}{\dm_c}$.

We have the following compilations:

\begin{align*}
\compile{s}{\dm_c;\sm}
\pend;
\compile{s}{\sm}\\
\compile{c}{\dm_c;\sm}
\subst[]{\injf{x_i}{f_i}}{\rf{x}_i}{\dm_c}_i;
\compile{c}{\sm}
\end{align*}

In the rest of this proof, we note $\compdmc =
\subst[]{\injf{x_i}{f_i}}{\rf{x}_i}{\dm_c}_i$.

We consider the server reduction $\dm_c\pred{}_{c/s}\noinj{\dm_c}$.
We know that
$\noinj{\dm_c} = \substi[]{\injf{x_i}{f_i}}{\injval{\envr_s(x_i)}}{\dm_c}$.
Let us note $v_i = \envr_s(x_i)$.
We can build the following $\ocsis$ reduction:

Since $\co\envr_s\equivs{}\envr_s$, we also have
that $\co v_i\equivs{}v_i$ and
$\injval{\co v_i}\equivc{\envinj}\injval{v_i}$ for each $i$.
We note $\envinj_\bullet = \bdr{\rf{x_i}}{\injval{\co v_i}}_i$.
By definition of the slicing relation, the $\rf{x_i}$ are fresh, hence
they are not bound in $\co\envg$. We can thus construct
the global environment $\co\envg' = \co\envg\cup\envinj_\bullet$.
Since we only extend the part with injection references, we
still have that $\envg\equivc{}\co\envg'$.

We now consider the client reduction

We know that
$\noinj{\dm_c}$ is equal to
hence the reduction tree contains for each $i$ a reduction

To obtain a reduction of
$\compdmc = \subst[]{\injf{x_i}{f_i}}{\rf{x_i}}{\dm_c}_i$,
we simply substitute each of these subreduction by
one of the form
$\redmlc{}{\rf{x_i}}{\injval{\co v_c}}

for any queue $\envfrag$.
By <ref>, we can build the following reduction:

where $\co\vm_c\equivc{\envinj'}\vm_c$ and
$\co\trace_c\equivc{\envinj'}\trace_c$, for any queue $\envfrag$.

We now consider the execution of $\sm'$.
We have the following properties:

\begin{align*}
\co\envr_c+\co\vm_c &\equivc{\envinj'}\envr_c+\vm_c&
\co\envr_s &\equivs{}\envr_s&
\co\envg' &\equivc{}\envg&
\end{align*}

By induction on the execution of $\sm'$ and $\clientprog'$, we have
{\envfrag'_\bullet \cfrag \envfrag'}{\envfrag'}

\begin{align*}
\co\envg'' &\equivc{}\envg'&
\co\vm'_s&\equivs{\envinj''}\vm'_s&
\co\trace'_s&\equivs{\envinj''}\trace'_s\\
\fragenv{&\co\envg_f'',\vm'_s}&
\co\vm'_c&\equivc{\envinj''}\vm'_c&
\co\trace'_c&\equivc{\envinj''}\trace'_c
\end{align*}

Finally, we can build the following derivations:

We verify the following invariants:

\begin{align*}
\co\envg'' &\equivc{}\envg'&
\co\vm_s&\equivs{}\vm_s&
\co\trace_s&\equivs{}\trace_s\\
\fragenv{&\co\envg_f'',\vm_s+\vm'_s}&
\co\vm_c+\co\vm'_c&\equivc{\co\envg''}\vm_c+\vm'_c&
\co\trace_c+\co\trace'_c&\equivc{\co\envg''}\trace_c+\trace'_c&
\qedhere
\end{align*}

[Case $\modulem[\sideX]{X}{\mm};\sm'$ – Declaration of a mixed module]
* We assume that the following executions hold:

Let us assumes that we can build the following reductions

for any $\envfrag$, and that the following invariants hold:

\begin{align*}
\co\envg' &\equivc{}\envg''&
\co\vm_s&\equivs{}\vm_s&
\co\trace_s&\equivs{}\trace_s\\
\fragenv{&\co\envg_f',\vm_s}&
\co\vm_c&\equivc{\co\envg''}\vm_c&
\co\trace_c&\equivc{\co\envg'}\trace_c+\trace'_c
\end{align*}

By induction on the execution of $\sm'$ and $\clientprog'$,
we can build the following reduction:
which allows us to conclude.

To build the compiled reduction,
we will operate by case analysis over $\mm$.

[Subcase $\mm = \struct{\sm}_{\rf{X}}$ – Declaration of a mixed structure]
* We have $\clientprog = \bind{X}{(\struct{\clientprog_0})}$ and
$\mm^c = \rf{X}$
with the following reductions:

_c(X_0; []XX)

$\envg'' = \envg'\cup\bdr{\rf{X}}{\vm_c}$.

We have the following compilations:

\begin{align*}
\compile{s}{\modulem[\sideX]{X}{\struct{\sm}}_{\rf{X}}}
&= \begin{aligned}
\end{aligned}\\[2mm]
\compile{c}{\modulem[\sideX]{X}{\struct{\sm}}_{\rf{X}}}
&= \begin{aligned}
\end{aligned}
\end{align*}

By induction on the execution of $\sm$ and $\clientprog$,
we have
{\envfrag_\bullet \cfrag \envfrag}{\envfrag}
with the following invariants:

\begin{align*}
\co\envg' &\equivc{}\envg'&
\co\vm_s&\equivs{}\vm_s&
\co\trace_s&\equivs{}\trace_s\\
\fragenv{&\co\envg_f',\vm_s}&
\co\vm_c&\equivc{\co\envg'}\vm_c&
\co\trace_c&\equivc{\co\envg'}\trace_c
\end{align*}

We can then build the following executions:

Where $\co\envg'' = \co\envg'\cup\bdr{\rf{X}}{\co\vm_c}$.
We verify the following invariants:

\begin{align*}
\co\envg'' &\equivc{}\envg'&
\co\vm_s+\bdr{\dyn}{\rf{X}}&\equivs{}\vm_s+\bdr{\dyn}{\rf{X}}&
\co\trace_s&\equivs{}\trace_s\\
\fragenv{&\co\envg_f'',\vm_s}&
\co\vm_c&\equivc{\co\envg'}\vm_c&
\co\trace_c&\equivc{\co\envg'}\trace_c
\end{align*}

which concludes.

$\mm = \functori{X}{\Mm}{\struct{\sm}_{\rf{F}}}$ – Declaration of a mixed functor]
* In this case, we have
the client program $\clientprog = \bindenv{F}$ and
the module expression
$\mm^c = \functori{X}{\Mm}{\struct{\restrict{c}{\sm}}}$.
The following reductions hold:

Where $\envg' = \envg \cup\bdr{\rf{F}}{\envr_c}$ and the following values:

\begin{align*}
\vm_s &= \functorenvi{\envr_s}{X}{\Mm}{\struct{\sm}}\\
\vm_c &= \functorenvi{\envr_c}{X}{\Mm}{\struct{\restrict{c}{\sm}}}
\end{align*}

We recall that by hoisting, the body of the functors contains
no injection, hence we don't need to evaluate server code in the client

We have the following compilations:

\begin{align*}
\compile{s}{
\begin{aligned}
\end{aligned}}
\begin{aligned}
\modulem[]{\dyn}{\fragm{\rf{F}}{(\getdyn{X_i})_i}};\\
\end{aligned}\\[2mm]
\compile{c}{
\begin{aligned}
\end{aligned}}
\begin{aligned}
\end{aligned}\\[2mm]
\end{align*}

We trivially have the following execution:

Where $\envg' = \envg \cup\bdr{\rf{F}}{\co\vm_{\rf{F}}}$ with the following values:

\begin{align*}
\co\vm_s &= \functorenvi{\co\envr_s}{X}{\Mm}{\struct{\compile{s}{\sm}}}\\
\co\vm_c &= \functorenvi{\co\envr_c}{X}{\Mm}{\struct{\restrict{c}{\sm}}}\\
\co\vm_{\rf{F}}
&= \functorenvi{\co\envr_c}{X}{\Mm}{\struct{\compile{c}{\sm}}}\\
\end{align*}

We now need to show that the invariants still hold. We easily
have that $\co\vm_c\equivc{\co\envg}\vm_c$.
By definition of equivalence over mixed functors, we have
$\co\vm_s\equivs{}\vm_s$. Indeed, the body of the functor in $\co\vm_s$
is the server compilation of the body of the mixed
functor $\vm_s$ and the captured environments corresponds.
Finally, we have that the body of $\co\vm_{\rf{F}}$ is the
client compilation of the body of the mixed functors and that the
capture environment corresponds to $\envg'(\rf{F})$. Thus
we get that $\fragenv{\co\envg_f',\vm_s}$.
By definition of the annotation function, the reference $\rf{F}$ could not
have appeared on a previously executed structure,
hence we still have that $\fragenv{\co\envg_f',\co\rho_s}$.

Hence, all the following invariants are respected, which concludes.

\begin{align*}
\co\envg' &\equivc{}\envg'&
\co\vm_s&\equivs{}\vm_s\\
\fragenv{&\co\envg_f',\vm_s}&
\co\vm_c&\equivc{\co\envg''}\vm_c&&\qedhere
\end{align*}

Otherwise, $\mm$ is a module expression. By definition of slicability,
$\mm$ does not syntactically contain any structure. In the general
case, we should proceed by induction over module expressions. We
will simply present the case of a mixed functor application
where the functor returns a mixed structure.

We consider $\mm = F(X_1)\dots(X_n)$.
We have $\mm^c = F(X_1)\dots(X_n)$
with the following executions:

R fresh

= (

𝚠𝚒𝚝𝚑 F

𝚠𝚒𝚝𝚑 F

We note $\vm_F$ the value of $F$ in $\envg_s$, which is

We have the following compilations:

\begin{align*}
\compile{s}{\modulem[\sideX]{X}{F(X_1)\dots(X_n)}}
&= \begin{aligned}
\end{aligned}\\[2mm]
\compile{c}{\modulem[\sideX]{X}{F(X_1)\dots(X_n)}}
&= \begin{aligned}
\end{aligned}
\end{align*}

Let us now look at the execution of the server application
By hypothesis, $\vm_F$ is a mixed functor. By equivalence, we know
that $\co\envr_s(F) = \co\vm_F$ where $\co\vm_F\equivs{}\vm_F$.
By definition of the equivalence on server values, $\co\vm_F$
is of the following shape:

\begin{align*}
\co\vm_F
&= \left(\begin{aligned}
\end{aligned}\right)
\end{align*}

where $\co\envr'_s\equivs{\co\envg}\envr'_s$.
For each $i$ we note $\co\vm_i^s = \co\envr_s(X_i)$.
By equivalence, we have $\co\vm_i^s \equivs{} \vm_i^s$.

Furthermore, since $\co\envg\equivc{}\envg$ and by hypothesis, $\rf{F}$ is
also bound in $\co\envg$. We note $\vm_{\rf{F}}$ the corresponding value.
Since $\fragenv{\co\envg, \vm_c}$ (via $\envr_s$), then $\co\vm_{\rf{F}}$
is of the following shape:

\begin{align*}
\co\vm_{\rf{F}}
&= \left(\begin{aligned}
\end{aligned}\right)
\end{align*}

where $\co\envr_{\rf{F}}\equivc{\co\envg}\envr_{\rf{F}} = \envg(\rf{F})$.
Additionally, for each $i$ we note $\vm_i^c = \co\envg(\rf{R_i})$.
By equivalence, we have $\co\vm_i^c \equivs{} \vm_i^c$.

We can now proceed by induction on $\sm$ and $\clientprog_0$ in the
environment $\co\envg$,
$\co\envr_c\cup\bdr{Y_i}{\rf{R_i}}$ and
We obtain the following reductions:

with the usual invariants.

We can now build the following executions:

where $\envfrag_{\rf{R}} = \tokfrag{\rf{R}}{\rf{F}(\rf{R_1})\dots(\rf{R_n})}$.
We respect the following invariants:

\begin{align*}
\co\envg' &\equivc{}\envg'&
\co\vm_s&\equivs{}\vm_s&
\co\trace_s&\equivs{}\trace_s\\
\fragenv{&\co\envg_f',\vm_s}&
\co\vm_c&\equivc{\co\envg'}\vm_c&
\co\trace_c&\equivc{\co\envg'}\trace_c
\end{align*}

Let us now consider the client application.
Since $\envr_c\equivc{\co\envg}\co\envr_c$, we
have that the body of the functor $F$ is equivalent.
We can thus build the following reduction:

By equivalence of $F$ and $X_i$ in $\envr_c$ and $\co\envr_c$, we have
that $\co\envg'\equivc{}\envg'$, $\co\vm'_c\equivc{\co\envg'}\vm'_c$
and $\co\trace_c\equivc{\co\envg'}\trace_c$.

We already built the reduction for the compiled server program. We
can now build the compiled client program:

where the invariants still hold. This concludes.

§.§ Proof of the main theorem

Finally, we prove <ref>. This is a direct consequence of

We have that $ \redp{\emptyr}{\Pm}{v}{\trace} $. By definition of an
program execution, we can decompose this rule as following:

We trivially have the following invariants:

\begin{align*}
\emptyr &\equivc{\emptyr}\emptyr&
\emptyr &\equivs{}\emptyr&
\co\envg &\equivc{}\envg&
\end{align*}

which allow us to apply <ref> and conclude.