<figure><img src="image_1.png" /></figure>

HAL
open science

# Retrofitting OCaml modules

Clément Blaudeau, Didier Rémy, Gabriel Radanne

► To cite this version:

Clément Blaudeau, Didier Rémy, Gabriel Radanne. Retrofitting OCaml modules: Fixing signature avoidance in the generative case. JFLA 2023 - 34èmes Journées Francophones des Langages Appliquatifs, Jan 2023, Praz-sur-Arly, France. pp.59-100. hal-03936636v2

HAL Id: hal-03936636

https://inria.hal.science/hal-03936636v2

Submitted on 24 Jan 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
Retrofitting OCAML modules
Fixing signature avoidance in the generative case

Clément Blaudeau¹, Didier Remy¹, and Gabriel Radanne²

¹ Cambium, Inria, France

² CASH, Inria, EnsL, UCBL, CNRS, LIP, France

Abstract

ML modules are offer large-scale notions of composition and modularity. Provided as
an additional layer on top of the core language, they have proven both vital to the working
OCaml and SML programmers, and inspiring to other use-cases and languages. Unfor-
tunately, their meta-theory remains difficult to comprehend, requiring heavy machinery
to prove their soundness. Building on a previous translation from ML modules to Fω,
we propose a new comprehensive description of a generative subset of OCAML modules,
embarking on a journey right from the source OCAML module system, up to Fω, and back.
We pause in the middle to uncover a system, called canonical that combines the best of
both worlds. On the way, we obtain type soundness, but also and more importantly, a
deeper insight into the signature avoidance problem, along with ways to improve both the
OCAML language and its typechecking algorithm.

# 1 A powerful but imperfect module system

Modularity is a key technique to break down a complex program into parts at different levels of abstraction. Instead of dealing with technical details and complex invariants at all times, programmers can split the code-base into manageable parts, called *modules*, and structure the relationship between those modules by specifying their interfaces and interactions. Code might be packed into a module to make a component, such as the implementation of a data-structure, reusable and often polymorphic—effectively factorizing development. Controlling the interactions between modules through a cautious choice of interfaces is not only a tool for correctness; using abstraction, it is also a way to enforce invariants and to allow for several teams of developers to work independently on different parts of the same program while enjoying a language-level guarantee that they respect the invariants of other parts.

A wide variety of techniques can be used to apply modularity concepts to software develop-
ment: simple compilation units, classes, packages, crates, etc. In languages of the ML-family,
modularity is provided by *modules*, which form a language layer built on top of the core lan-
guage. The interactions between modules are controlled statically by a strict type system,
making modularity work in practice and with little run-time overhead. A module is described
by its interface, called a *signature*, which serves as both a light specification and an API.

The OCAML module system is especially rich and still under development for new features. It provides both developer-side and user-side abstraction mechanisms: developers can control the outside view of a module by explicitly restricting its interface, while users can abstract over a module with a given interface using a *functor*. The signature language allows to both *restrict* and *control* the interface of a module, specifically by *hiding* fields (which corresponds to the distinction between *public* and *private* fields in Object-Oriented Programming), or by abstracting type components—keeping types accessible while hiding their definitions.

The OCAML module system is renowned for its expressiveness, ease of use, and the properties it can statically enforce. All sizable OCAML projects use modules to access libraries or define
<figure><img src="image_2.png" /><figcaption>Figure 1: A representation of the mismatch between the *reachable space* of module expressions (outer-most circle) and the *describable space* of signatures (inner ellipse). The common use-cases of OCAML are mainly within the area where the type-checker behaves correctly. In some cases, the current OCAML typechecker can lose type-equalities while still being in the describable space. This may lead to (1) producing a signature where some type fields are unnecessarily made abstract (over-abstraction) or (2) failing at inferring the signature (incorrect avoidance).</figcaption></figure>

parametric instances of data structures (sets, hashtables, streams, etc.). Several successful projects have made heavy use of modules, as in MirageOS [Madhavapeddy et al., 2013] where modules and functors are even assembled on demand using a DSL [Radanne et al., 2019]. Despite the successes and the interest of the community regarding ML modules, giving it a formal type-theoretic definition and establishing its properties has proven to be a difficult task.

Besides the academic interest, having a formal semantics is made even more necessary to envision extensions such as modular implicits [White et al., 2014] where new modules could be built automatically from their signatures by applications of functors to other modules.

## 1.1 The signature avoidance problem

The *signature avoidance* problem is a key issue of ML-module systems. It originates from a mismatch, illustrated in Figure 1, between the expressiveness of the module and signature languages: the *reachable space* of possible module expressions is larger than the *describable space* of signatures: some modules can't be described by a signature. This issue can be solved either by sticking to the describable space and ensuring that the typechecker correctly covers it or by extending signatures to make the reachable and describable spaces coincide.

This mismatch is caused by the interaction of three mechanisms. First, type abstraction, which is key to control access and protect invariants by typing, creates new types that are only compatible with themselves (or aliases of themselves). Second, sharing abstract types between modules, which is essential for module interactions, produces trees of type-alias equalities. Finally, hiding type components (through either explicit projections or implicit subtyping during functor applications) can remove abstract type aliases from scope, while other components (values or types) kept *in scope* may refer to them (for instance, removing an abstract type *t* while keeping a value of type *t list*). In some situations, there is no possible signature to infer for a module; in other situations, there are several incompatible ones.

We illustrate this abstraction mechanism in Example 1. Each source code comes with a representation of the type equalities and aliases as a *tree of type equalities*. The connected components of the tree represent equal, interchangeable types that all belong to the same equivalence class. They can be rooted with base types (*int*, *bool*, *string*, etc.) or constructed over other types (like *int list*, *int* → *int*, *int* × *bool*, etc.) or previously defined *abstract types*. Abstracting a type effectively removes a link in the type-sharing tree, which splits a connected component.

Example 1 precisely illustrates this potential loss of type sharing when using module oper-
<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

<figure><img src="image_6.png" /><figcaption>Example 1: Two examples of modules and associated type-sharing trees.</figcaption></figure>

ations. On the left-hand side, restricting the signature of the module X to the module type S removes the link between X.t and int (grayed out in the type-sharing tree): this becomes hidden to the typechecker outside of the body of the module X. On the right-hand side, the projection on the submodule Y removes X.t and X.u. The types Y.a, Y.b, and Y.c are pointing to *out-of-scope* types: they must be changed or deleted. This shows why expressing membership to an equivalence class through paths is fragile: the removal of type fields can split connected components apart, resulting in a loss of type-sharing or incorrect signatures.

**Strategies for solving signature avoidance** When a type declaration is referring to an out-of-scope type, there are mainly three strategies to correct the signature: (1) abstracting the type (effectively ignoring the previous link in the tree), (2) rewriting the type equalities using in-scope aliases (effectively rewiring the tree to maintain connected components), or (3) extending the signature syntax with existential types. The first strategy can lead to loss of type sharing, but is easy to implement—it is the one currently in use in the OCAML typechecker. The cases where the second strategy succeeds constitute the *solvable* cases of signature avoidance. The OCAML type-checker only tries to follow directed edges of the tree until it finds an accessible type, but does not follow reverse edges and thus does not have a notion of *connected components*. In *Example 1*, it would fail at finding that Y.a, Y.b and Y.c are aliases. Sometimes, no *in-scope* alias is available and signature avoidance cannot be solved without an extended syntax: those are the *general* cases of signature avoidance.

**Signature avoidance in practice** OCAML developers usually get around this limitation by explicitly naming modules before using them, which adds always-accessible root points to the graph. The module syntax of OCAML actually encourages this approach by limiting the places where inlined, unnamed modules and signatures can be used. In particular, projection on an unnamed module (as done in *Example 1*) is forbidden. However, explicit naming is sometimes cumbersome, which can limit the usability of module-based programming patterns such as modular implicits. It also prevents a fine-grained management of types shown in public APIs.

## 1.2 Related work

Previous work has provided solid formal foundations for ML-modules. The link between abstract types in ML-module systems and existential types in $F^\omega$ was already explored by Mitchell
<figure><img src="image_7.png" /><figcaption>Figure 2: The different systems: their links, with theorems and sections.</figcaption></figure>

and Plotkin [1985]. This vision was opposed by MacQueen [1986], who considered existential types to be too weak, and proposed using a restriction of dependent types (strong sums) to describe module systems. Further work, notably on phase separation by Harper et al. [1989], supported the idea that dependent types may actually be too powerful (thus, unnecessarily complex) for module systems. SML modules were first described by Harper et al. [1989]. Two approaches for the formalization and improvement of abstract types in SML were later concomitantly described by Leroy [1994] (through manifest types) and Harper and Lillibridge [1994] (via an adapted $F^\omega$ with translucent sums). The OCAML module system itself was specified by Leroy [1994, 2000], and later with an extension to applicative functors [Leroy, 1995].

The use of existential types to interpret signatures by Russo [2004] opened the door for a simplified link between modules and $F^\omega$. Type generativity is also explored by DREYER [2007], using stamps in place of existential types. A similar, but logically-based approach was later developed by Montagu and Rémy [2009] introducing the concept of open existential types. Pushing Russo's idea further, a closer correspondence between ML-modules and $F^\omega$ was achieved by Rossberg et al. [2014] by elaborating a significant subset of the SML module syntax into $F^\omega$. The type system is safe by construction, inheriting the property from $F^\omega$. A limit of this approach is that, since the definition of modules is only given by translation, the programmer must think in terms of the elaboration and only sees the elaborated types instead of the usual signatures. This makes direct reasoning on the source program more difficult. Their work, called the F-ing approach, also covered some difficult points like applicative functors and first-class modules, and was partially mechanized in Coq. Moving one step further, Rossberg [2018] achieved a unification of the core and module languages (thus, un-stratified) using $F^\omega$ as the underlying programming language and seeing module constructs as syntactic sugar. More recently, Crary [2020] used involved focusing techniques to solve the signature avoidance problem in the singleton-type approach (for SML modules) in a manner that turns out to have some similarities with that of F-ing.

## 1.3 A journey into OCaml modules

Our approach is strongly inspired by previous works, which we re-explore in the context of OCAML modules. Our goal is to provide a simpler and comprehensive type system for OCAML modules, which could first serve as a specification, then help correct and improve the current implementation, and, finally, serve as a basis for future extensions of the module language. Our contributions are summarized in Figure 2.

We start by presenting a (mostly standard) self-contained specification of the OCAML module system in §2, adapted from previous works. Critically, like the current OCAML implementation, this presentation suffers from the signature avoidance problem.

Then, we build on the insights of the F-ing [Rossberg et al., 2014] translation into $F^\omega$ to present a new set of typing rules. However, reasoning only by elaboration in $F^\omega$ is hard, as the elaboration introduces encoding layers and, crucially, uses a very different way of handling
abstract types, making the correspondence between source and $F^ω$ terms and types rather obscure. Instead, as hinted in the work of Russo [2004], we introduce a light extension of the syntax for signatures with $F^ω$-style quantifiers, which we call *canonical signatures*. They act as a middle point between the path-based approach of the source and the quantified approach of $F^ω$, effectively splitting the translation effort in two steps. We introduce in §3 a new type system for OCaml modules, called *canonical*, where the source module expressions are typed with canonical signatures and source signatures translated into canonical ones. This system is simpler than the source one and doesn't suffer from the signature avoidance problem. Using our one-way translation, we revisit and explain the ad-hoc techniques (strengthening, equivalence) of the source presentation. We finally give the main result of this section: all source typing derivations can be translated into canonical typing derivations (Theorem 1).

The reverse translation of signatures (from the canonical system to the source one) is not always possible, as the former is more expressive than the latter. In §4 we explore *when* and *how* we can translate canonical signatures back into OCaml signatures, which uncovers precisely why the signature syntax lacks expressivity. This reverse process, called *anchoring*, is one of our main contributions. We then show that we can restrict the canonical system at one specific point to *mimic* the source system and only produce signatures that are valid regarding the source typing (Theorem 2). Some details are also given in the appendix §A.

The link between the canonical system and $F^ω$ is conceptually easier while presenting some technical challenges. For lack of space, it is only detailed in the appendix §B. We introduce an *hybrid* system that produces both canonical and $F^ω$ objects in correspondence. The hybrid system acts a central justification, as it can yield both the canonical system and the *F-ing* style elaboration by projections. The canonical system was actually designed by erasing the terms from the $F^ω$ encoding which can still be seen as implicit *proof terms* justifying the canonical rules.

In this work, we restricted our system to a generative subset of the language. We believe our approach also extends to applicative functors and other features (first-class modules, module aliases, abstract signatures, etc.), which are left for future work. Our long term goal is to extend OCaml signatures following the canonical system, thus completely solving the signature avoidance problem. The canonical system would then be a standalone *source* system which can be used by programmers to reason about OCaml programs, with the $F^ω$ elaboration ensuring its soundness.

# 2 A generative subset of the OCaml module system

In this section we present a module system that models a generative subset of OCaml. We present its grammar, several auxiliary judgments used, and end with its typing judgment.

## 2.1 Grammar and syntactic choices

Figure 3 gives the grammar for a generative subset of the module language. The language of modules is built on top of a core language of expressions *e* and types *τ* which we leave abstract, except for value identifiers *x* and type identifiers *t*, so that we can extend expressions with qualified variables and types with qualified types.

**Syntactic choices** The language of module expressions and signatures is rather standard, except for a few minor design choices. We consider the following conventions: module related meta-variables use *uppercase letters*, *M*, *X*, etc. while lowercase letters are used for expressions
<figure><img src="image_8.png" /><figcaption>Figure 3: Syntax of the module language</figcaption></figure>

and types of the core language. Lists are written with an overhead bar: $\overline{D}$ is a list of $D$. In order to simplify the treatment of scoping and shadowing, we use self-references, ranged over by letter $A$, in both structures and signatures to refer to the current object; their binding occurrence appears as a subscript to the structure or signature they belong to, so that self-references can freely be renamed. Abstract types are specified as types pointing to themselves, e.g., $type t = A.t$ where $A$ is the self-reference of the current structure. In typing contexts $\Gamma$, identifiers, denoted by $I$, are prefixed by the self-reference $A$ of the structure or signature they are meant to belong to. As an implicit convention, in entries $A.I : D$, the identifier extracted from $D$ is $I$. We introduce prefixes, written with the letter $Q$, to range over either a path $P$ or a self reference $A$. We use a distinct class of variables, written $Y$, for functor parameters, which can be freely renamed. By contrast, and as usual with modules, neither identifiers $X$ and $T$ for module expressions and signatures, nor the identifiers $x$ and $t$ for core language expressions and types can be renamed, as they also play the role of an external name.

**Projections and accesses** Several restrictions are built into the grammar: field accesses inside a module type are forbidden, since prefixes $Q$ may not originate from a module type identifier $T$; and paths cannot contain functor applications, which makes the system fully *generative*. We allow projection on any module expression, but we restrict functor application to paths. Current OCAML does the opposite, mainly to prevent cases prone to trigger signature avoidance. Our choice is more general, as the OCAML one can be encoded, while the converse requires an explicit signature annotation on the functor argument.

**Omitted constructs** In addition to restricting the system to be generative, we omit some constructs for the sake of simplicity: the include operator, explicit constraints $S$ with $type t = \tau$
<figure><img src="image_9.png" /><figcaption>Figure 4: Structure of judgments for the source system</figcaption></figure>

(resp. module $X = P$) and deleting constraints $S$ with type $t := \tau$ (resp. module $X := P$). We believe that they do not impact the overall structure of the system, only adding more cases in the set of rules. We did not include first-class modules.

## 2.2 System structure and judgments

The typing judgment uses several auxiliary judgments whose dependencies are presented in Figure 4. The system we present revolves around two main components: *typing* (for module expressions and signatures) and *subtyping*. The *path-based* representation of type sharing in OCaml modules requires us to define two more judgments: *equivalence* and *strengthening*. Finally, as retrieving signatures in the environment is non trivial, we define a pair of *resolution* helper judgments. We present and explain these judgments in reversed order of dependency in the subsequent subsections.

## 2.3 Resolution

In the OCaml module system, retrieving the signature of a given path (of a module stored in the environment) is not as simple as a lookup. First, objects are stored with multiple levels of indirection (like $X.X' \cdot X''$) which requires to inspect intermediary signatures. Secondly, every signature can be a module type variables, which must also be resolved to its definition before accessing a field. For this purpose, we recursively define a *path resolution* judgment $\Gamma \vdash_P Q \vdash S$ which gives the signature $S$ of a path $P$ and a *signature resolution* judgment $\Gamma \vdash_Q Q.T \Leftrightarrow S$, which retrieves the definition $S$ of a module type $Q.T$ (both in an environment $\Gamma$).

We show below two examples of resolution rules. Rule S-RES-MODTYPE links path resolution and signature resolution: if the path resolution of $P$ returns a module type $Q.T$, the definition of $Q.T$ should be resolved to a signature $S$. Rule S-RES-PROJ-MOD accesses a submodule $X$ of a module path $P$. This rule illustrates the transformation of *local* links in the signature $S$ (that might refer to other components of the module at $P$ via its self-reference $A$) into *absolute* ones by substitution of the self-reference $A$ for the path $P$. The full set of rules is given in §C.1.

$$ \frac{\substack{\text{S-RES-MODTYPE} \\ \Gamma \vdash_P Q.T \qquad \Gamma \vdash_{\text{src}} Q.T \Leftrightarrow S}}{\Gamma \vdash_P S} $$

$$ \frac{\substack{\text{S-RES-PROJ-MOD} \\ \Gamma \vdash_P \text{sig}_A \bar{D} \text{ end} \qquad (\text{module } X : S) \in \bar{D}}}{\Gamma \vdash_P P.X \triangleright S[A \mapsto P]} $$

## 2.4 Equivalence

In the path-based approach of OCaml, several paths can resolve to the same type, as illustrated in §1.1. A type definition can have several *equivalent* expressions, called aliases. This leads us to consider a notion of *type equivalence* based on the existence of a common ancestor when browsing the type sharing tree of aliases. This can be seen in the rules S-EQV-TYPE-RES and
<figure><img src="image_10.png" /></figure>

<figure><img src="image_11.png" /></figure>

<figure><img src="image_12.png" /></figure>

<figure><img src="image_13.png" /><figcaption>Example 2: Two equivalent signatures $S_1$ and $S_2$: they define two different type sharing trees that yet have the same connected components. Specifically, two types are aliases in $S_1$ if and only if they are also aliases in $S_2$.</figcaption></figure>

<figure><img src="image_14.png" /></figure>

<figure><img src="image_15.png" /></figure>

<figure><img src="image_16.png" /><figcaption>Example 3: Strengthening and its graphical interpretation</figcaption></figure>

**S-EQV-TYPE-LOCAL:** a type is equivalent to its definition (and only to itself for abstract types). With transitivity, symmetry, and reflexivity, we get an equivalence relationship on types.

$$ \frac{\Gamma \vdash_P P \triangleright \text{sig}_A \bar{D} \text{ end} \quad (\text{type } t = \tau) \in \bar{D}}{\Gamma \vdash_P P.t \approx \tau [A \mapsto P]} $$

$$ \frac{(A.t : \text{type } t = \tau) \in \Gamma}{\Gamma \vdash_A A.t \approx \tau} $$

Building on this type equivalence, we define *signature equivalence*: two signatures are equivalent if we can go from the first one to the second one by only substituting type aliases. This is illustrated by the two signatures in Example 2. The full set of rules is given in §C.2.

## 2.5 Strengthening

The need for strengthening is illustrated in Example 3. When aliasing the module `M` on line 7, the inferred signature for `N` cannot be straightforwardly obtained by copying the signature of `M` without loss of type-sharing. Indeed, `M` defines an abstract type which is a root of a connected component of the underlying type-sharing tree. Duplicating the signature duplicates the root, effectively creating a separated connected component and thus, a new abstract type. The known solution to this problem is to use a *strengthening* operation $\Gamma \vdash P/S \gg S'$ of a signature `S` by a path `P`, producing `S'`, a *strengthened* version of `S` where each abstract type field has been rewritten into a concrete type field pointing to its original definition in `P`.

Rule S-STR-SIG-SIG shows the case for declarations inside a signature. Our technical choice of having abstract types represented as pointers to themselves ($\text{type } t = A.t$) makes the definition of strengthening easy, as substituting the self-reference for the path suffices to transform local links into absolute ones ($\text{type } t = P.t$). Thus, strengthening does not change declarations, except
for submodules (rule S-STR-DECL-MOD) where the signature is strengthened with the extended path P.X. Factor signatures are not strengthened, as they do not introduce new abstract types. The full set of rules is given in §C.3.

$$ \frac{\text{S-STR-SIG-SIG}}{\Gamma \vdash \overline{D}[A \mapsto P]/P \gg \overline{D}'} \quad \text{S-STR-DECL-MOD} \quad \frac{\text{S-STR-DECL-MOD}}{\Gamma \vdash S/(P.X) \gg S'} $$

$$ \frac{\text{S-STR-DECL-MOD}}{\Gamma \vdash (\text{module } X : S) / P \gg \text{module } X : S'} $$

## 2.6 Subtyping

The subtyping judgment has a fundamental role in the OCAML module system, as it allows the user to define an abstract (polymorphic) interface and assign it to a module that has a richer signature than this interface. In OCaml, some (but not all) subtyping operations have computational content: the removal and reordering of fields implies a runtime copy of the memory representation of the module. We thus distinguish two operations: *Subtyping by abstraction*, written $\Gamma \vdash^{\text{src}} S_1 \triangleleft: S_2$, which has no computational content and *Subtyping*, written $\Gamma \vdash^{\text{src}} S_1 \prec: S_2$, which includes the former and also allows for removal and reordering of fields and therefore has some computational content. Both judgments have the same rules, except for the comparison of structural signatures.

Subtyping on signatures enforces a structural match (up to name resolution): functor signature against functor signature and structural signature against structural signature. The latter case is where the only distinction between the two modes of subtyping appears: in subtyping by abstraction, the two lists of declarations $\overline{D}$ and $\overline{D}'$ are compared directly as shown in rule S-SUB-SIG-SIG. In the general form of subtyping, a subset $\overline{D}_0$ of the declaration list $\overline{D}$ is compared with $\overline{D}'$, allowing for reordering and deletion, as shown in Rule S-SUB-SIG. Using a subset instead of a subsequence allows for reordering.

$$ \frac{\text{S-SUB-EQ-SIG-SIG}}{\Gamma \vdash \overline{A.D}^{\text{src}} \vdash \overline{D} \triangleleft: \overline{D}'} \quad \text{S-SUB-EQ-SIG} \quad \frac{\text{S-SUB-EQ-SIG}}{\Gamma \vdash \text{sig}_A \overline{D} \text{ end} \triangleleft: \text{sig}_A \overline{D}' \text{ end}} $$

$$ \frac{\overline{D}_0 \subseteq \overline{D}}{\Gamma \vdash \overline{A.D}^{\text{src}} \vdash_A \overline{D}_0 \prec: \overline{D}'} \quad \text{S-SUB-EQ-SIG} \quad \frac{\text{S-SUB-EQ-SIG}}{\Gamma \vdash^{\text{src}} \text{sig}_A \overline{D} \text{ end} \prec: \text{sig}_A \overline{D}' \text{ end}} $$

In both rules, the subtyping is done *declaration by declaration* (independently), in an environment that contains all the declarations of the richer (left-hand-side) signature. This approach matches well with our representation choice of abstract types, allowing us to have only one rule for comparing both abstract types and concrete types declarations (rule S-SUB-DECL-TYPE). The other subtyping rules for declarations are straightforward, and depends on signature subtyping. As a module type field can be used in both covariant and contravariant positions (as functor arguments for example), the rule for subtyping a module type declaration checks subtyping in both directions. In §C.4 and in the following, the rules that are similar between abstraction and general subtyping are given with the symbol $\prec$: being either $\prec$ or $\triangleleft$:

$$ \frac{\text{S-SUB-DECL-TYPE}}{\Gamma \vdash^{\text{src}} \tau \prec: \tau'} \quad \text{S-SUB-DECL-MOD-TYPE} \quad \frac{\text{S-SUB-DECL-MOD}}{\Gamma \vdash^{\text{src}} S \prec: S'} \quad \text{S-SUB-DECL-MOD} \quad \frac{\Gamma \vdash^{\text{src}} S' \prec: S}{\Gamma \vdash^{\text{src}} (\text{module type } T = S) \prec: (\text{module type } T = S')} $$

$$ \frac{\text{S-SUB-DECL-MOD-TYPE}}{\Gamma \vdash^{\text{src}} S \prec: S'} \quad \text{S-SUB-DECL-MOD} \quad \frac{\Gamma \vdash^{\text{src}} S' \prec: S}{\Gamma \vdash^{\text{src}} (\text{module type } T = S) \prec: (\text{module type } T = S')} $$

## 2.7 Typing

Once all the auxiliary judgments have been laid out, the typing judgment is mostly straightforward. All rules are given in §C.5. The judgments for signature typing $\Gamma \vdash^{\text{src}} S : \checkmark$ and declarations
typing $\Gamma \vdash_A^{\text{src}} D : \checkmark$ ensure that no shadowing occurs and no free variables are used. We omit the rules here. The judgment for bindings $\Gamma \vdash_B : D$ uses a core-language typing judgment for expressions and typing of signatures, and is mutually recursive with the typing of modules (for submodules). The rules are straightforward and omitted.

**Module typing** The judgment for modules contains both syntax-directed and free-floating rules, making the presentation purposefully logical rather than algorithmic. There is an equivalent algorithmic presentation, but it is more involved and hides the key insights of the separation of operations between resolution, equivalence, strengthening, subtyping, and typing. Besides, the equivalent, canonical model that we propose in the next section is better suited for deriving algorithmic presentations for the source system. Free-floating typing rules must have no computational content. Therefore, general subtyping (which has some computation content), is not free floating: it should only be used at specific program points, namely functor application and signature ascription, where the target signature of the runtime coercion is explicit in the source. While having no computational content, subtyping by abstraction is still not made free-floating to prevent unnecessary abstraction of types (which would lead to loss of type-sharing). The syntax-directed rules are as follows:

S-TYP-MOD-RES

$$ \frac{\Gamma \vdash_P \Delta S}{\Gamma \vdash_P S} $$

S-TYP-MOD-SEALING

$$ \frac{\Gamma \vdash_S \checkmark \quad \Gamma \vdash_P S' \quad \Gamma \vdash_{S'} \Delta : S}{\Gamma \vdash (P : S) : S} $$

S-TYP-MOD-STRUCT

$$ \frac{\Gamma \vdash_A^{\text{src}} \bar{B} : \bar{D} \quad A \notin \Gamma}{\Gamma \vdash \text{struct}_A \bar{B} \text{ end} : \text{sig}_A \bar{D} \text{ end}} $$

S-TYP-MOD-FUNCTOR

$$ \frac{\Gamma \vdash S_a : \checkmark \quad \Gamma ; (Y : S_a) \vdash_M S \quad Y \notin \Gamma}{\Gamma \vdash (Y : S_a) \to M : (Y : S_a) \to S} $$

S-TYP-MOD-APP

$$ \frac{\Gamma \vdash_P P : (Y : S_a) \to S \quad \Gamma \vdash_{P'} S' \quad \Gamma \vdash_{S'} S' < : S_a}{\Gamma \vdash P(P') : S[Y \mapsto P']$$

S-TYP-MOD-PROJ

$$ \frac{\Gamma \vdash_M \mathit{sig}_A (\overline{D_1}, \mathit{module} X : S, \overline{D_2}) \mathit{end}}{\Gamma \vdash_M X : S'} $$

Functor application (Rule S-TYP-MOD-APP) is normally a place where *signature-avoidance* may occur. In our presentation however, the restriction of functor application to paths prevents this issue. Indeed, as all the abstract types of the argument are defined in the context, no type field is hidden by the application, and thus, no escaping of scope can occur. In contrast, as the grammar allows projection on any module expression (which can hide type fields and could trigger signature avoidance), the projection rule S-TYP-MOD-PROJ is designed to tackle the issue. The abstraction subtyping $\Gamma, \overline{D_1} \vdash_S \Delta : S'$ allows for cutting the links to types in $S$ that will become inaccessible *outside* of the signature of $M$, i.e., without the fields declared in $\overline{D_1}$, so that the resulting signature $S'$ is wellformed in $\Gamma$. This rule is however too permissive, as we allow to *implicitly* abstract *more than necessary* and lose some type sharing. Additional conditions to prevent *unnecessary* loss of type sharing could be added to this rule, but they would be complex to write down in this setting. Fortunately, they will be easy to express using the canonical system.

**Free-Floating rules** Before doing a projection $M \times X$, we must allow to *rewire* the type sharing tree so that types used in $X$ point to other aliases (either external ones, i.e., accessible outside
of M, or local ones, accessible inside of X). Similarly, we must allow strengthening to keep sharing information between aliases. This leads to two additional *free-floating* rules:

$$ \frac{\begin{array}{c} \text{S-TYP-STRENGTHEN} \\ \Gamma \vdash P : S \\ \Gamma \vdash P : S' \end{array}}{\Gamma \vdash P : S'} $$

$$ \frac{\begin{array}{c} \text{S-TYP-EQUIV} \\ \Gamma \vdash M : S \\ \Gamma \vdash M : S' \end{array}}{\Gamma \vdash M : S'} $$

**Remarks on the source system** While this declarative presentation of the source system may appear relatively simple, it actually suffers from three main issues. First, it relies on the equivalence judgment to *guess* correct rewritings in signatures. Second, type sharing can be lost when projecting on a submodule via over-abstraction. Thirdly, the strengthening judgment may seem ad-hoc, while being necessary to prevent loss of type-sharing. In current OCaml, these problems are partially solved via *heuristics* which are sufficient in simple cases, but fail for more advanced uses of modules. We now study a canonical presentation of the module system that solves all three issues.

# 3 Canonical signatures and existential types

Some issues of the source presentation come from the ambiguity and weaknesses of the path-based type-sharing. In this section, we present an alternative set of typing rules with an extended syntax for signatures inspired by previous work on representation of modules in $F^\omega$. This system, called *canonical*, has simpler typing judgments and does not suffer from the signature avoidance problem. We show that the canonical system is more expressive than the source one, as every module expression that can be typed in the source system can also be typed in the canonical system with a signature that has at least the same amount of type sharing.

## 3.1 The need for existential types

In the source presentation, maintaining the connected components of the type sharing tree throughout projection —where fields can be deleted— sometimes require rewriting type equalities (through equivalence) or abstracting type fields (through abstraction subtyping). The core issue is that source signatures store type equalities via a type sharing tree that is cumbersome to handle. However, the information we are actually interested in is not the type sharing tree itself, only the connected components. To handle those directly, we introduce an *existential type* that acts as a canonical representative of the equivalence class. In the type sharing tree, it can be seen as an additional point with a special status, and the whole tree is flattened to one level of depth, as illustrated in Example 4. Rooted with an existential type that cannot be deleted, the connected components become insensible to the loss of some type fields. Building on this intuition, we present a new system, called *canonical*, where signatures use quantifiers to handle abstract types.

## 3.2 System structure and judgments

The grammar of the language, given in Figure 5, extends the OCAML grammar of Figure 3. Crucially, the source syntax (for modules and signatures) remains the same, including source signatures, while new syntactical categories are introduced to represent canonical signatures (and canonical types). By convention, we use curvy capitals ($R$, $S$, $D$, ...) for canonical objects.
<figure><img src="image_17.png" /><figcaption>Example 4: Comparison between the source and canonical signatures and their associated type-sharing trees. Canonical signatures are extended with an existential binder that acts as a special anchor point for the tree.</figcaption></figure>

<figure><img src="image_18.png" /><figcaption>Figure 5: Syntax extensions of the *canonical* module language.</figcaption></figure>

We distinguish between *manifest* canonical signatures $\mathcal{R}$ that only refer to abstract types bound in the context and *abstract* canonical signatures $\exists \bar{\alpha}. \mathcal{R}$ (written $S$) that also specify the existential types $\bar{\alpha}$ created by the module. Notice that canonical manifest signatures cannot refer to other signatures (e.g., using paths), as these are always inlined. Signatures of functors are polymorphic in the abstract types provided by the argument: indeed, these should be treated abstractly, while they can also be returned and thus shared in the result. Signatures stored in module type declarations are just parameterized by their abstract types: these will later be existentially or universally quantified, depending on context. We use an $\mathcal{F}^\omega$ style $\lambda$-binding for these. As we will see in the typing rules, the grammar restricts the positions where abstract types are bounded (existentially or universally). For instance, inside a structural signature, all submodules have manifest signatures, while functor bodies may bound new abstract types.

Canonical signatures remove the need for resolution, equivalence, and strengthening, which significantly simplifies the overall presentation. The judgments are thus reduced to typing of modules (and bindings), typing of source signatures, which we enrich to produce a canonical signature, and subtyping.

## 3.3 Signature typing

We start with signature typing $\Gamma \vdash_S : \lambda \bar{\alpha}. \mathcal{R}$ and declaration typing $\Gamma \vdash_A D : \lambda \bar{\alpha}. \mathcal{D}$, as they illustrate the key mechanism of *abstract type lifting*. The positions where abstract types are
bound are crucial to ensure the correct sharing of types. First, abstract types are introduced only by an abstract type declaration (Rule C-TYP-DECL-TYPEABS). Then, they are gathered and lifted from abstract type definitions and submodules to their parent module to ensure sharing between declarations in the same structure (rules C-TYP-DECL-MOD and C-TYP-DECL-SEQ). The lifting does not go through a functor definition (Rule C-TYP-SIG-FUNCTOR): indeed, in the generative case, each application of the functor should create new unrelated abstract types. The full set of rules are in §D.2.

### C-TYP-DECL-TYPEABS

$$A.t \notin \Gamma$$

$$\Gamma \vdash_A^{\text{can}} \text{type } t = A.t : \lambda\alpha. \text{type } t = \alpha$$

### C-TYP-DECL-MOD

$$\Gamma \vdash^{\text{can}} S : \lambda\bar{\alpha}.\mathcal{R}$$

$$A.X \notin \Gamma$$

$$\Gamma \vdash_A^{\text{can}} (\text{module } X : S) : \lambda\bar{\alpha}. (\text{module } X : \mathcal{R})$$

### C-TYP-DECL-SEQ

$$\Gamma \vdash_A^{\text{can}} D_1 : \lambda\bar{\alpha}_1.D_1$$

$$\Gamma, \bar{\alpha}_1, A.I_1 : D_1 \vdash_A^{\text{can}} \bar{D} : \lambda\bar{\alpha}.\bar{D}$$

$$\Gamma \vdash_A^{\text{can}} (D_1, \bar{D}) : \lambda\bar{\alpha}_1 \bar{\alpha}. (D_1, \bar{D})$$

### C-TYP-SIG-FUNCTOR

$$\Gamma \vdash^{\text{can}} S_a : \lambda\bar{\alpha}.\mathcal{R}_a$$

$$\Gamma, \bar{\alpha}, Y : \mathcal{R}_a \vdash^{\text{can}} S : \lambda\bar{\beta}.\mathcal{R}$$

$$Y \notin \Gamma$$

$$\Gamma \vdash^{\text{can}} (Y : S_a) \to S : \forall\bar{\alpha}. (Y : \mathcal{R}_a) \to \exists\bar{\beta}.\mathcal{R}$$

## 3.4 Subtyping

The subtyping between two canonical signatures $\exists\bar{\alpha}.\mathcal{R}$ and $\exists\bar{\alpha}'.\mathcal{R}'$ is similar to the source subtyping, with the addition of the mechanism to deal with quantifiers.

Rule C-SUB-SIG-MATCH allows us to compare abstract signatures, while the other subtyping rules deal with concrete signatures. The types $\bar{\alpha}$ created by the left-hand-side signature are made available (i.e., pushed in the context), while the right-hand-side ones $\bar{\alpha}'$ are instantiated with some types $\bar{\tau}$. If both signatures define the same abstract types (up to $\alpha$-conversion), a simple renaming instantiation $\bar{\alpha} \mapsto \bar{\alpha}'$ is sufficient. Otherwise, the left-hand-side signature $\mathcal{R}$ can be less abstract (i.e., binding fewer abstract types) than the right-hand-side one $\mathcal{R}'$, in which case some right-hand side abstract types are instantiated with concrete types.

For functor signatures (Rule C-SUB-SIG-FUNCTOR), the parameter is in a contravariant position, hence we check subtyping of the argument signatures in reverse order. As with the source presentation, we distinguish between two kinds of subtyping: abstraction-only subtyping $\Gamma \vdash^{\text{can}} S_1 \triangleleft S_2$ and general subtyping $\Gamma \vdash^{\text{can}} S_1 \prec S_2$, which allows both abstraction and deletion of fields. They differ only by the rules C-SUB-SIG-SIG vs. C-SUBEQ-SIG-SIG. In §D.1 and in the following, the rules that are similar between abstraction and general subtyping are given with the symbol $\prec$: being either $\prec$: or $\triangleleft$:

### C-SUB-SIG-MATCH

$$\Gamma, \bar{\alpha} \vdash^{\text{can}} \mathcal{R} \prec: \mathcal{R}'[\bar{\alpha}' \mapsto \bar{\tau}]$$

$$\Gamma \vdash^{\text{can}} \exists\bar{\alpha}.\mathcal{R} \prec: \exists\bar{\alpha}'.\mathcal{R}'$$

### C-SUB-SIG-FUNCTOR

$$\Gamma, \bar{\alpha}' \vdash^{\text{can}} \mathcal{R}' \prec: \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}]$$

$$\Gamma, \bar{\alpha}', (Y : \mathcal{R}') \vdash^{\text{can}} S[\bar{\alpha} \mapsto \bar{\tau}] \prec: S'$$

$$Y \notin \Gamma$$

$$\Gamma \vdash^{\text{can}} \forall\bar{\alpha}. (Y : \mathcal{R}) \to S \prec: \forall\bar{\alpha}'. (Y : \mathcal{R}') \to S'$$

### C-SUB-SIG-SIG

$$\bar{D}_0 \subseteq \bar{D}$$

$$\Gamma \vdash^{\text{can}} \bar{D}_0 \prec: \bar{D}'$$

$$\Gamma \vdash^{\text{can}} \text{sig}_A \bar{D} \text{ end} \prec: \text{sig}_A \bar{D}' \text{ end}$$

### C-SUBEQ-SIG-SIG

$$\Gamma \vdash^{\text{can}} \bar{D} \triangleleft \bar{D}'$$

$$\Gamma \vdash^{\text{can}} \text{sig}_A \bar{D} \text{ end} \triangleleft: \text{sig}_A \bar{D}' \text{ end}$$

## 3.5 Typing

As with subtyping, the use of canonical signatures and existential types makes the typing simpler and syntax directed. The key technical point is the lifting of the existential quantification that
happens during typing, as already explained for the signature typing in §3.3.

**Bindings typing** The rules presented below for typing a binder give a list of canonical declarations *alongside* a list of (created) existential types. The signature typing judgment is used to convert source types and signatures (as in Rule C-TYP-DECL-MODTYPE for instance) into canonical types and signatures.

$$ \begin{array}{l} \text{C-TYP-DECL-MOD} \\ \Gamma \vdash_M : \exists \bar{\alpha}. \mathcal{R} \\ \Gamma \vdash_A^{\text{can}} (\text{module } X = M) : \exists \bar{\alpha}. (\text{module } X : \mathcal{R}) \end{array} $$

$$ \begin{array}{l} \text{C-TYP-DECL-MODTYPE} \\ \Gamma \vdash_S : \lambda \bar{\alpha}. \mathcal{R} \\ \Gamma \vdash_A^{\text{can}} (\text{module type } T = S) : (\text{module type } T = \lambda \bar{\alpha}. \mathcal{R}) \end{array} $$

$$ \begin{array}{l} \text{C-TYP-DECL-SEQ} \\ \Gamma \vdash_A^{\text{can}} B_1 : \exists \bar{\alpha}_1. \mathcal{D}_1 \\ \Gamma \vdash_A^{\text{can}} B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \mathcal{D}_1, \bar{\mathcal{D}} \end{array} $$

The existential types—which are lifted from submodules with Rule C-TYP-DECL-MOD—are merged by Rule C-TYP-DECL-SEQ, to extend their scope to the local enclosing module. For example, if a module *M* has a submodule *X* which defines an abstract type *α*, the existential quantification is lifted from the submodule *X* to the whole module *M*.

**Module expressions typing** Existential types are introduced only by explicit sealing (Rule C-TYP-MOD-SEALING). Applying a functor to its argument (Rule C-TYP-MOD-APP) can share the types of the argument via the substitution $[\bar{\alpha} \mapsto \bar{\tau}]$.

$$ \begin{array}{l} \text{C-TYP-STRUCT} \\ \Gamma \vdash_A^{\text{can}} B : \exists \bar{\alpha}. \bar{\mathcal{D}} \\ \Gamma \vdash^{\text{can}} \mathit{struct}_A B \end{array} \quad \begin{array}{l} A \notin \Gamma \\ \text{end} : \exists \bar{\alpha}. \mathit{sig}_A \bar{\mathcal{D}} \end{array} $$

$$ \begin{array}{l} \text{C-TYP-MOD-SEALING} \\ \Gamma \vdash_S : \lambda \bar{\alpha}. \mathcal{R} \\ \Gamma \vdash_P : \mathcal{R}' \\ \Gamma \vdash^{\text{can}} \mathcal{R}' < : \mathcal{R} [\bar{\alpha} \mapsto \bar{\tau}] \\ \Gamma \vdash (P : S) : \exists \bar{\alpha}. \mathcal{R} \end{array} $$

$$ \begin{array}{l} \text{C-TYP-MOD-FUNCTOR} \\ \Gamma \vdash^{\text{can}} S : \lambda \bar{\alpha}. \mathcal{R} \\ \Gamma, \bar{\alpha}, (Y : \mathcal{R}) \vdash^{\text{can}} M : S \\ \Gamma \vdash^{\text{can}} (Y : S) \rightarrow M : \forall \bar{\alpha}. (Y : \mathcal{R}) \rightarrow S \end{array} $$

$$ \begin{array}{l} \text{C-TYP-MOD-APP} \\ \Gamma \vdash P : \forall \bar{\alpha}. (Y : \mathcal{R}) \rightarrow S \\ \Gamma \vdash P' : \mathcal{R}' \\ \Gamma \vdash^{\text{can}} \mathcal{R}' < : \mathcal{R} [\bar{\alpha} \mapsto \bar{\tau}] \\ \Gamma \vdash^{\text{can}} P(P') : S [\bar{\alpha} \mapsto \bar{\tau}] \end{array} $$

$$ \begin{array}{l} \text{C-TYP-MOD-PROJ} \\ \Gamma \vdash M : \exists \bar{\alpha}. \mathit{sig}_A \bar{\mathcal{D}}_1, \text{module } X : \mathcal{R}, \bar{\mathcal{D}}_2 \end{array} $$

In the source presentation, the projection rule S-TYP-MOD-PROJ is the only place where sig-nature avoidance can arise, by cutting local links in unsolvable ways. We needed to allow for abstraction subtyping. In the canonical presentation (Rule C-TYP-MOD-PROJ), all the local links go through existentially quantified abstract types in front of the signature. By keeping all the existentially quantified types, projecting a component cannot cause signature avoidance: all the abstract types (that could go out of scope and cause signature avoidance issues) that M.X could use are in the list $\bar{\alpha}$ and remain bound in the signature of M.X. The full set of typing rules is given in §D.2.
## 3.6 From the source to the canonical system

Both presentations share the same grammar for module expressions and signatures, and thus have the same input for typing. By extending the typing predicate to environments (to check wellformedness), we can translate source judgments (resolution, equivalence, strengthening) into the canonical presentation. This translation—called canonification—gives insight on how the source mechanisms can be understood in the canonical framework.

**Typing of source environments** We translate environments with source signatures into their canonical counterparts, using signature typing, declaration typing, and the following rules:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \text{C-CF-EMPTY} & \begin{array}{c} \Gamma \vdash \Gamma_s \\ \vdots \\ \Gamma, \bar{\alpha}, (Y : \mathcal{R}) \vdash \Gamma_s \end{array} & \begin{array}{c} \Gamma \vdash \Gamma_s \\ \vdots \\ \Gamma, \bar{\alpha}, (A.I : \mathcal{D}) \vdash \Gamma_s \end{array} \\ \text{C-CF-DECL} & \begin{array}{c} \Gamma \vdash \Gamma_s \\ \vdots \\ \Gamma, \bar{\alpha}, (A.I : \mathcal{D}) \vdash \Gamma_s \end{array} & \begin{array}{c} \Gamma \vdash \Gamma_s \\ \vdots \\ \Gamma, \bar{\alpha}, (A.I : \mathcal{D}) \vdash \Gamma_s \end{array} \end{array} $$

**Canonification of resolution** We now state how the resolution behaves regarding canonification. The main difference between the two systems comes from the fact that abstract types are quantified outside of the signature in the canonical system (the signature is always concrete), while they are introduced anywhere inside source signatures (which may contain abstract type definitions). Thus, the source signature obtained via resolution of *P* and the canonical signature of *P* only differ by the presence of quantifiers.

$$ \Gamma_s \vdash P \triangleright S \wedge \Gamma \vdash \Gamma_s \wedge \Gamma \vdash S : \lambda \bar{\alpha}.\mathcal{R} \Rightarrow \Gamma \vdash P : \mathcal{R} \quad (1) $$

$$ \Gamma_s \vdash Q.T \Leftrightarrow S \wedge \Gamma \vdash \Gamma_s \wedge \Gamma \vdash S : \lambda \bar{\alpha}.\mathcal{R} \Rightarrow \Gamma \vdash Q.T : \lambda \bar{\alpha}.\mathcal{R} \quad (2) $$

**Canonification of strengthening** Via resolution, the introduction of abstract types is re-exposed by the signature. To prevent an actual duplication of abstract types, the source presentation relies on strengthening. While the resolution of a path *P* corresponds to a canonical signature with existential types bound in front, a strengthened signature can be made fully concrete (no quantified types): all types refer to their original definition through the path *P*. In the canonical presentation, this is a *no-op*, as all type definitions already go through the proper quantified existential types in the context:

$$ \Gamma_s \vdash P \triangleright S \wedge \Gamma_s \vdash S/P \gg S' \wedge \Gamma \vdash \Gamma_s \wedge \Gamma \vdash S : \lambda \bar{\alpha}.\mathcal{R} \Rightarrow \Gamma \vdash S' : \mathcal{R} \quad (3) $$

**Canonification of equivalence** As we described in the previous section, two equivalent signatures have the same connected components of their type sharing tree. In the canonical model, all connected components are flattened into a tree of depth 1, with an existentially quantified variable at the root. This means that two equivalent signatures actually have the same canonification, which matches the intuition (and naming) that canonical signatures are indeed *canonical*. We get the following result:

$$ \Gamma_s \vdash S_1 \approx S_2 \wedge \Gamma \vdash \Gamma_s \wedge \Gamma \vdash S_1 : S_1 \wedge \Gamma \vdash S_2 : S_2 \Rightarrow S_1 = S_2 \quad (4) $$

**Canonification of subtyping** As the rules of subtyping in the source and canonical systems are very similar, the two judgments are also very similar. The only difference is that source subtyping can lose type equalities by over-abstraction. However, in the canonical system, with
Rule C-SUB-SIG-MATCH, the correspondence between the abstract types is dealt with at the signature level, with no abstraction done at the declaration level. We get the following result:

$$ \Gamma_s \vdash_{\text{src}} S_1 <: S_2 \wedge \Gamma \vdash_{\text{can}} \Gamma_s \wedge \Gamma \vdash_{\text{can}} S_1 : S_1 \wedge \Gamma \vdash_{\text{can}} S_2 : S_2 \implies \Gamma \vdash_{\text{can}} S_1 <: S_2 \quad (5) $$

**Canonification of typing** Once all canonification results have been laid out, the typing result becomes easy to write. All typing derivations can be translated into canonical ones, with the only difference being that some over-abstraction during projections and resolutions can lead to a source signature having lost some type sharing. This type-sharing loss, can be delayed to the last step of the derivation (combining the losses of all the intermediary signatures), which gives the following result:

**Theorem 1 (Canonification of typing).** Considering any module expression *M* that admits a signature *S* in the source presentation, it also admits a corresponding canonical signature *S* with more type equalities:

$$ \Gamma_s \vdash_{\text{src}} M : S \wedge \Gamma \vdash_{\text{can}} \Gamma_s \wedge \Gamma \vdash_{\text{can}} S : S \implies \Gamma \vdash_{\text{can}} M : S' \wedge \Gamma \vdash_{\text{can}} S' \prec: S $$

This link between the source and canonical system shows the expressiveness of the latter one, but is only half of the story. Exploring at which conditions the canonical derivations can be translated back into the source will uncover a new concept: anchorability.

# 4 Anchoring: back to the source system

In this section we study the process of translating typing derivations from the canonical system back into the source system, which we call *anchoring*. As the canonical system is more expressive than the source one, it is not always possible to translate signatures back into the source syntax. Still, we can precisely exhibit the conditions under which anchoring is possible. This gives a new specification of the source system, which could also be used to improve the way signature avoidance is actually resolved in OCAML.

The canonical system thus provides the intuition, formal guarantees, and algorithmic insights for the design of OCAML's modules mechanisms.

## 4.1 Quantification vs structural information

The key insight is the semantic difference in the source syntax between the declaration of a concrete type (*type* = *τ*) and that of an abstract type (*type*). An abstract type declaration states the *introduction* of both a new type and of a new field that may later be used as a handle to refer to this abstract type, directly or indirectly via a path. For a signature used in a covariant position, an abstract type declaration effectively *creates* a new type (existential quantification) and *adds* a type field (structural information) to the signature. By contrast, a concrete type definition only introduces structural information—adding a field to refer to an existing type but without introducing a new type.

Canonical signatures *separate* the quantification information (existential, universal, or lambda binders) from the structural information (fields). Thus, it makes the scope of abstract types explicit, using the logical notion of binder, which is perfectly suited for that purpose. More importantly, it allows to refer to types that do not yet have a handle, while the source system cannot. This is illustrated in the following code:
1 | module X = (struct
2 |     module X0 = (... : sig type t end)
3 |     module X1 = struct
4 |         type u = X0.t * int
5 |         type v = X0.t * bool
6 |     end
7 | end).X1

10 | (* Canonical signature of X *)
11 | module X : ∃α. sig
12 |     type u = α * int
13 |     type v = α * string
14 | end

Here, a type definition (*t*) is lost when projecting only on the submodule *X1*. The source syntax *cannot* express the existence of a type that is the first component of both *u* and *v* without already having a handle to that type<fnref n="1" />: being forced to merge quantification and structural information limits the expressiveness. However, the module *X* can be given a canonical signature, where the two kinds of information are clearly separated.

This allows us to better describe the solvable and unsolvable cases of signature avoidance for the source presentation. In the *solvable* cases of signature avoidance, each use of an abstract type has an *in-scope* alias (that can serve as a handle) defined before the type is used. In such cases, the quantification and structural information coincide in a way expressible by the source syntax. In other cases, signature avoidance is *unsolvable*.

## 4.2 Anchoring of canonical signatures

Building on the insights of the previous subsection, we can describe the *anchoring* process that translates a canonical signature back into the source system when the quantification and structural information coincide. The main mechanism boils down to identifying the first place where an abstract type $\alpha$ is used. If it is at the top level of a type declaration $type t = \alpha$, we say that the existential type $\alpha$ is *anchorable*. In the corresponding source signature, we can make *t* an abstract type definition, creating a handle to *t* that can then be used instead of $\alpha$ in the canonical signature. The type *t* must be the *first* reference to the abstract type $\alpha$, regardless of whether or not it is the original definition point. If the type $\alpha$ is used earlier, we raise a signature avoidance failure.

**Example 5** illustrates the process of finding the first available position to rewire the type-sharing tree of **Example 1**. We see the change of the defining instance of $\alpha$, from $X.t$ to $Y.a$ after a projection that makes $X.t$ and $X.u$ unreachable.

The anchoring process consists of associating abstract types with their first available aliases, which we gather using an *anchoring map* $\theta : \alpha \mapsto Q.t$. We define a signature anchoring judgment $\Gamma \vdash_S \Sigma \leftrightarrow \Gamma_s; \theta_\Gamma \vdash_S \theta$ that, given an environment $\Gamma$ and a canonical signature $S$, produces a source environment $\Gamma_s$ associated with an anchoring map $\theta_\Gamma$ and a source signature $S$ associated with an anchoring map $\theta$. In a nutshell, the judgment produces the source counterpart of the canonical signature $S$ by gathering the handles of the abstract types, and replacing the uses of abstract types by their handles. The full set of rules is given in §D.3.

Using the anchoring judgment, we define *anchorable typing*, written $\Gamma \upharpoonright^\text{anc} M : S$. The judgment is defined by a copy of the typing rules for the judgment $\Gamma \vdash M : S$ presented in §3.5, except for the projection rule which takes an additional premise checking for anchorability of the resulting signature. All *anchorable* typing derivations can be translated into source typing derivations.

<footnote n="1">¹Adding a type field for *t* would not work, as it would not be an equivalent signature.</footnote>
<figure><img src="image_19.png" /><figcaption>Canonical signature $S_1$ Source signature $S_1$</figcaption></figure>

<figure><img src="image_20.png" /><figcaption>Canonical signature $S_2$ Source signature $S_2$</figcaption></figure>

Example 5: Graphical representation of the anchoring process on the type sharing trees. In the two canonical signatures $S_1$ and $S_2$, the existential type $\alpha$ is anchorable. For $S_1$, we can use $X.t$ for the handle to $\alpha$, as done in $S_1$. For $S_2$, a projection removed $X.t$ and $X.u$. The handle becomes $Y.a$ as shown in $S_2$.

**Theorem 2 (Anchorable typing).** Anchorable typing produces a signature that is valid regarding the source typing rules:

$$ \Gamma \vdash^{anc} M : S \quad \wedge \quad \Gamma \vdash^{anc} S \hookrightarrow \Gamma_s; \theta_{\Gamma} \vdash S : \theta \quad \implies \quad \Gamma_s \vdash^{src} M : S \qquad (6) $$

More explanations and the formal definition of the anchoring process are given in §A. This completes the link between the source and canonical systems: canonical derivations can be translated back into the source when we restrict their expressiveness. The last link, namely the actual encoding in $F^\omega$ that inspired the design of the canonical system, is detailed in §B.

## Conclusion

ML-Module systems are known for being a well-studied but complex topic. The path-based, OCAML approach has proven to be successful in practice, but has some structural issues. While being restricted to a generative subset, our study of the signature avoidance problem in the source presentation exposes the limitations of the current signature syntax. These limitations are at the heart of the need for *ad-hoc* and complex fixes (strengthening, equivalence). Building on previous works, we introduced the canonical system as a more expressive yet simpler language, equipped with the right construction (existential types) to separate quantification and structural information, and solve the main issues of the source system. Using the canonical system, we shined a new light on the ad-hoc techniques of the source presentation and provided a detailed description of the solvable and unsolvable cases of signature avoidance. While still being close to the OCAML source, the canonical presentation can easily be elaborated into $F^\omega$, which provides formal guarantees. As a middle-point between usability and formalism, the canonical system is both a comprehensive description and a framework for building new features and improving the algorithms (specifically for the *solvable* cases of signature avoidance) of the current OCAML typechecker.

## References

K. Crary. A focused solution to the avoidance problem. *Journal of Functional Programming*, 30: e24, 2020. ISSN 0956-7968, 1469-7653. doi: 10.1017/S0956796820000222. URL https://www.cambridge.org/core/product/identifier/S0956796820000222/type/journal_article.
D. DREYER. Recursive type generativity. *Journal of Functional Programming*, 17(4-5): 433-471, 2007. doi: 10.1017/S0956796807006429.

R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In *Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '94, page 123-137, New York, NY, USA, 1994. Association for Computing Machinery. ISBN 0897916360. doi: 10.1145/174675.176927. URL https://doi.org/10.1145/174675.176927.

R. Harper, J. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In *Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '90, page 341-354, New York, NY, USA, 1989. Association for Computing Machinery. ISBN 0897913434. doi: 10.1145/96709.96744. URL https://doi.org/10.1145/96709.96744.

X. Leroy. Manifest types, modules, and separate compilation. In *Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '94, page 109-122, New York, NY, USA, 1994. Association for Computing Machinery. ISBN 0897916360. doi: 10.1145/174675.176926. URL https://doi.org/10.1145/174675.176926.

X. Leroy. Applicative functors and fully transparent higher-order modules. In *Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '95*, pages 142-153, San Francisco, California, United States, 1995. ACM Press. ISBN 978-0-89791-692-9. doi: 10.1145/199448.199476. URL http://portal.acm.org/citation.cfm?doid=199448.199476.

X. Leroy. A modular module system. *J. Funct. Program.*, 10(3):269-303, 2000. URL http://journals.cambridge.org/action/displayAbstract?aid=54525.

D. B. MacQueen. *Using Dependent Types to Express Modular Structure*, page 277-286. Association for Computing Machinery, New York, NY, USA, 1986. ISBN 9781450373470. URL https://doi.org/10.1145/512644.512670.

A. Madhavapeddy, R. Mortier, C. Rotsos, D. J. Scott, B. Singh, T. Gazagnaire, S. Smith, S. Hand, and J. Crowcroft. Unikernels: library operating systems for the cloud. In V. Sarkar and R. Bodík, editors, *Architectural Support for Programming Languages and Operating Systems*, ASPLOS 2013, Houston, TX, USA, March 16-20, 2013, pages 461-472. ACM, 2013. doi: 10.1145/2451116.2451167. URL https://doi.org/10.1145/2451116.2451167.

J. C. Mitchell and G. D. Plotkin. Abstract types have existential types. In *Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages*, POPL '85, page 37-51, New York, NY, USA, 1985. Association for Computing Machinery. ISBN 0897911474. doi: 10.1145/318593.318606. URL https://doi.org/10.1145/318593.318606.

B. Montagu and D. Rémy. Modeling Abstract Types in Modules with Open Existential Types. In *Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL'09)*, pages 354-365, Savannah, GA, USA, Jan. 2009. ISBN 978-1-60558-379-2. doi: http://doi.acm.org/10.1145/1480881.1480926.

G. Radanne, T. Gazagnaire, A. Madhavapeddy, J. Yallop, R. Mortier, H. Mehnert, M. Perston, and D. Scott. Programming unikernels in the large via functor driven development, 2019.
A. Rossberg. 1ML - Core and modules united. *J. Funct. Program.*, 28:e22, 2018. doi: 10.1017/S0956796818000205. URL https://doi.org/10.1017/S0956796818000205.

A. Rossberg, C. Russo, and D. Dreyer. F-ing modules. *Journal of Functional Programming*, 24(5):529-607, Sept. 2014. ISSN 0956-7968, 1469-7653. doi: 10.1017/S0956796814000264. URL https://www.cambridge.org/core/product/identifier/S0956796814000264/type/journal_article.

C. V. Russo. Types for modules. *Electronic Notes in Theoretical Computer Science*, 60:3-421, 2004. ISSN 1571-0661. doi: https://doi.org/10.1016/S1571-0661(05)82621-0. URL https://www.sciencedirect.com/science/article/pii/S1571066105826210.

L. White, F. Bour, and J. Yallop. Modular implicits. In *Proceedings ML Family/OCaml Users and Developers workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014.*, pages 22-63, 2014. doi: 10.4204/EPTCS.198.2. URL https://doi.org/10.4204/EPTCS.198.2.
# A Anchoring

## A.1 Anchoring of signatures

In this section we present in more details the mechanism that, under certain conditions, allows to build one of the source signatures corresponding to a given canonical signature. As mentioned in §4.2, the anchoring judgment, written

$$ \Gamma \vdash_S^{anc} S \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta $$

states that, given a canonical signature $S$ and environment $\Gamma$, we can build a corresponding source signature $S$ and source environment $\Gamma_s$. Both are returned with an *anchoring map* $(\theta$ for the signature and $\theta_\Gamma$ for the environment) that gives a path $Q.t$ for the handle of every abstract type $\alpha$.

The anchoring map is extended when a type declaration with an *un-mapped* existential is encountered, which can be seen in rule C-ACH-DECL-ANCHORPOINT: the anchoring of the type declaration returns a non-empty map $\alpha \mapsto t$. In contrast, if the type field is concrete, an empty anchoring map is produced, as in Rule C-ACH-DECL-TYPE. Maps are merged together with the sequence rule C-ACH-DECL-SEQ, via the merging operator $\oplus$. The map associated with the left-hand-side declaration is *prefixed* with the self-reference. More generally, we write $Q.\theta$ as a shortcut for the map $\alpha \mapsto Q.\theta(\alpha)$.

$$ \begin{array}{c} \text{C-ACH-DECL-ANCHORPOINT} \\ \Gamma \vdash_{\Gamma_A}^{anc} \text{type } t = \alpha \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{type } t = A.t : (\alpha \mapsto t) \end{array} $$

$$ \begin{array}{c} \text{C-ACH-DECL-TYPE} \\ \Gamma \vdash^{anc}_{\Gamma_A} \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset \\ \Gamma \vdash^{anc}_{\Gamma_A} \text{type } t = \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{type } t = \tau' : \emptyset \end{array} $$

$$ \begin{array}{c} \text{C-ACH-DECL-SEQ} \\ \Gamma \vdash^{anc}_{\Gamma_A} \mathcal{D} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \mathcal{D} : \theta \\ \Gamma \vdash^{anc}_{\Gamma_A} \bar{\mathcal{D}} \leftrightarrow (\Gamma_s, A.I : \mathcal{D}) ; (\theta_\Gamma \uplus A.\theta) \vdash \bar{\mathcal{D}} : \theta' \\ \Gamma \vdash^{anc}_{\Gamma_A} \mathcal{D}, \bar{\mathcal{D}} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \mathcal{D}, \bar{\mathcal{D}} : \theta_\Gamma \uplus \theta' \end{array} $$

The judgment is easily extended to signatures and environments. Rule C-ACH-ENV-DECL shows how the anchoring map associated with a single declaration is merged with the environment map.

$$ \begin{array}{c} \text{C-ACH-ENV-DECL} \\ \Gamma \vdash_{\Gamma_s}^{anc} \Gamma_s : \theta_\Gamma \quad \Gamma, \bar{\alpha} \vdash_{\Gamma_A}^{anc} \mathcal{D} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \mathcal{D} : \theta \quad \text{dom}(\theta) = \bar{\alpha} \\ \Gamma, \bar{\alpha}, A.I : \mathcal{D} \leftrightarrow (\Gamma_s, A.I : \mathcal{D}) : \theta_\Gamma \uplus A.\theta \end{array} $$

## A.2 Anchorable typing

As mentioned in §4.2, we can use the anchoring judgment to restrict the canonical typing to anchorable signatures. In our approach, the only place where a *non-anchorable* signature can be introduced is during projection on a submodule. Thus, we reuse all the rules of §3.5, except for the projection rule, which is modified to force the resulting signature to be anchorable:

$$ \begin{array}{c} \text{C-TYPA-MOD-PROJ} \\ \Gamma \vdash^{anc}_{\Gamma_s} M : \exists \bar{\alpha}. \text{sig}_A \quad \bar{\mathcal{D}}_1, \text{module } X : \mathcal{R}, \bar{\mathcal{D}}_2 \text{ end} \\ \Gamma \vdash^{anc}_{\Gamma_s} \exists \bar{\alpha}. \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta \\ \Gamma \vdash^{anc}_{\Gamma_s} M.X : \exists \bar{\alpha}. \mathcal{R} \end{array} $$
As expected, the anchorable typing, as a restriction of the canonical typing to *source-only* mechanisms, respects the source typing. More formally:

**Theorem 3 (Anchorable typing).** Given any environment $\Gamma$, module $M$ and (canonical) signature $S$, the anchored signature $S$ is a valid signature for the source typing:

$$ \left. \begin{array}{l} \Gamma \vdash^{anc} M : S \\ \Gamma \vdash^{anc} S \leftrightarrow \Gamma_s; \theta_{\Gamma} \vdash S : \theta \end{array} \right\} \Rightarrow \Gamma_s \vdash^{src} M : S \qquad (7) $$

The proof of this theorem uses the following lemma:

**Lemma 1 (Anchorability of subtyping).** Given $\Gamma$, $\Gamma_s$, $\sigma_{\Gamma}$, two canonical signatures $S_1$ and $S_2$, two source signatures $S_1$ and $S_2$, and two substitutions $\sigma_1$ and $\sigma_2$, we have:

$$ \left. \begin{array}{l} \Gamma \vdash^{anc} S \leftrightarrow \Gamma_s; \theta_{\Gamma} \vdash S : \theta \\ \Gamma \vdash^{anc} S' \leftrightarrow \Gamma_s; \theta_{\Gamma} \vdash S' : \theta' \\ \Gamma \vdash^{can} S < : S' \end{array} \right\} \Rightarrow \Gamma_s \vdash^{src} S < : S' \qquad (8) $$

This completes the presentation of the link between the source and the canonical systems. As mentioned, the canonical system was designed as a simpler presentation of the mechanisms found in the $F^\omega$ encoding of modules. To complete this presentation, the next section gives in more details the encoding and the main techniques used, especially regarding the sharing of abstract types.

# B $F^\omega$ and elaboration

To properly finish the transition from source to $F^\omega$ via the canonical system, we are missing one final link from the canonical system to $F^\omega$. In this section we give formal foundations and guarantees for the canonical system through *elaboration* into $F^\omega$: the elaboration is defined by *hybrid* judgments that relate module expressions and canonical signatures to terms and types of $F^\omega$. This gives a precise correspondence between the key mechanisms of the canonical system, in particular existential types, and standard mechanisms of $F^\omega$. The canonical system can actually be understood as a *particular mode of use* of $F^\omega$. Thanks to $F^\omega$, elaborated terms enjoy the properties of soundness, progress, and type preservation. In fact, the canonical system has been designed with the elaboration in mind, mainly by erasing proof terms and only retaining $F^\omega$ types. Hence, the elaboration is mostly straightforward.

Although, we use $F^\omega$ as the target language, we do not actually need the power of $F^\omega$ to model generative functors. The reason to pursue the development in $F^\omega$ is to also allow parameterized types in the source language and to be able to extend the encoding to the case of applicative functors in the future.

We start by giving the syntax and rules of the version of $F^\omega$ (extended with existential types and records) that we use for the elaboration and present the $F^\omega$ terms and types that encode modules and signatures. Then, we introduce the hybrid judgments. Finally, we state the correctness theorem for the elaboration and the link between the canonical system and $F^\omega$.

This section is largely inspired by Rossberg et al. [2014]. We only made minor changes to the encoding of module expressions and signatures: the encoding of module types use $\lambda$-abstraction rather than existential quantification; declarations are encoded differently. The main difference is the extension of the judgments to produce both the $F^\omega$ type and the canonical signature, whereas in Rossberg et al. [2014], typing and subtyping are only defined by elaboration.
$$ \kappa := \Omega \mid \kappa \rightarrow \kappa \qquad (\text{kinds}) $$

$$ \rho := \alpha \mid \rho \rightarrow \rho \mid \{\overline{\ell : \rho}\} \mid \forall \alpha : \kappa.\rho \mid \exists \alpha : \kappa.\rho \mid \lambda \alpha : \kappa.\rho \mid \rho \rho \qquad (\text{types}) $$

$$ E := x \mid \lambda x : \rho.E \mid E E \mid \{\overline{\ell = E}\} \mid E.\ell \mid \lambda \alpha : \kappa.E \mid E \rho \\ \mid \mathit{pack} \langle \rho, E \rangle_{\rho} \mid \mathit{unpack} \langle \alpha, x \rangle = E \text{ in } E \qquad (\text{terms}) $$

$$ W := \lambda x : \rho.E \mid \{\overline{\ell = W}\} \mid \lambda \alpha : \kappa.E \mid \mathit{pack} \langle \rho, W \rangle_{\rho} \qquad (\text{values}) $$

$$ \Gamma := \cdot \mid \Gamma, \alpha : \kappa \mid \Gamma, x : \rho \qquad (\text{environments}) $$

<figure><img src="image_21.png" /><figcaption>Figure 7: Syntactic categories and encoding</figcaption></figure>

## B.1 F-omega and encoded signatures

We use a standard variant of explicitly typed $F^\omega$ with primitive records and existential types; We only give its syntax in Figure 6; its typing rules are available in §E. We use letters $\rho$ and $E$ to range over types and expressions so as to distinguish them from the core language types and expressions, $\tau$ and $e$, although these should be seen as a subset of $\rho$ and $E$. While kinds are part of terms, we usually omit them in $F^\omega$ terms for the sake of conciseness and readability.

To help with the elaboration, we assume a collection $\ell_I$ of record labels indexed by identifiers of the canonical (and source) system. The encoding of the canonical system into $F^\omega$ is described in Figure 7. Functors are encoded as functions and structural signatures as records. Declarations are encoded as record entries: we use the category of the identifier to distinguish between the encoding of values, types, modules and module types. We also introduce some syntactic sugar to have the encoding of declarations look similar to the usual canonical and source syntax. We use the following (overloaded) operator to shorten the encoding of type and module-type fields, with the type encoding on the left and the corresponding term on the right:

$$ \langle\!\langle\rho\rangle\!\rangle := \forall (\beta : \kappa \rightarrow \star). \beta \rho \rightarrow \beta \rho \quad (\text{Type}) \qquad \langle\!\langle\rho\rangle\!\rangle := \Lambda(\beta : \kappa \rightarrow \star). \lambda(x : \beta \rho). x \quad (\text{Term}) $$

This allows to represent *type fields* as $F^\omega$ terms, specifically record fields: the term is always the identity and only its type encoding in the annotation matters, namely to enforce typing constraints. Indeed, erasing type fields during elaboration would have been possible, but this would prevent the elaboration from distinguishing canonical terms that would only differ from their type fields. This will ensure that two modules that differ only from their type definitions (i.e., their type fields) will also differ in their signatures. The type is generalized with a type operator $\beta$ to allow the encoding of higher-kinded types.

A representative example of the encoding of a simple module is given in Example 6. The encoded signature is a type of $F^\omega$ that can be read as a canonical signature. Using the syntactic sugar makes the similarity with the source type even more striking. In the evidence term, we can see that the sealing of `int` corresponds to a `pack(int, ...)` term. To share the abstract type between the two fields (`X` and `u`), the abstract type is unpacked and then repacked, using a
pattern of the form unpack<α, ·> = · in pack<α, ·> called a repacking pattern.

1
module M = struct
2
module X = (struct
3
  type t = int
4
  let v = 42
5
  end : sig
6
  type t
7
  val v : t
8
  end)
9
type u = X.t*bool
10
end

### Encoded signature

$$ \Pi = \exists \alpha \left\{ \begin{array}{l} \ell_X : \{ \ell_t : \langle\langle \alpha \rangle\rangle \} \\ \ell_v : \alpha \\ \ell_u : \langle\langle \alpha \times \mathbf{bool} \rangle\rangle \end{array} \right\} \triangleq \exists \alpha \left\{ \begin{array}{l} \mathbf{module} \ X : \left\{ \begin{array}{l} \mathbf{type} \ t = \alpha \\ \mathbf{val} \ v : \alpha \end{array} \right\} \\ \mathbf{type} \ u = \alpha \times \mathbf{bool} \end{array} \right\} $$

### Encoded module

$$ E = \mathbf{unpack}(\alpha_1, y_1) = \mathbf{pack}(\mathbf{int}, \{\ell_X = \{\ell_t = \langle\langle \mathbf{int} \rangle\rangle, \ell_v = 42\}\}) \text{ in} \\ \mathbf{unpack}(\emptyset, y_2) = \{\ell_u = \langle\langle (\alpha_1 \times \mathbf{bool}) \rangle\rangle\} \text{ in} \\ \mathbf{pack}(\alpha_1, \{\ell_X = (y_1.\ell_X), \ell_u = (y_2.\ell_u)\}) $$

Example 6: A simple module with two components (a submodule X and a type definition u). Its signature is encoded into a type Π of $F^ω$. A term E (called an evidence term) represents the module and has type Π.

## B.2 An extension of the canonical system

The *hybrid* system can be seen as an *extension* of the canonical one: the judgments are extended to actually present both the canonical and $F^ω$ parts. We define all judgments over an extended, hybrid environment $\Delta$ that contains both canonical and $F^ω$ terms, defined as follows:

$$ \Delta ::= \emptyset | \Delta, \bar{\alpha} | \Delta, (Y : (\mathcal{R}, \Sigma)) | \Delta, (A.I : (\mathcal{D}, \zeta)) $$

The elaborated judgments rely on a core-language translation into $F^ω$ for terms and types, that is omitted here.

### B.2.1 Subtyping

We define the subtyping judgment $\Delta \vdash^{\text{elab}} S_1 <: S_2 \rightsquigarrow \Pi_1 <: \Pi_2 \Rightarrow f$, which follows closely the canonical one, as the handling of canonical signatures and $F^ω$ types are similar. We use a version of $F^ω$ with explicit subtyping, so the judgment is extended to produce a *subtyping function* $f: \Pi_1 \to \Pi_2$. The nature of this subtyping function gives interesting insights on the compilation of modules. For abstraction-only subtyping, the subtyping function is $\beta\eta$-convertible to the identity as the memory representation of modules (the terms) are the same when stripped of types. For general subtyping (with reordering or deletion of fields), the subtyping function is not *code-free*; correspondingly, it requires a specific action from the compiler (copy, access table, etc.).

The rule for functor subtyping E-SUB-SIG-FUNCTOR illustrates the main mechanisms: building on the subtyping functions (and type matching $\bar{\tau}$) for the parameter and the body, we craft a subtyping function from the left-hand-side functor signature to the right-hand-side one. All
the rules are given in §F.1.

E-SUB-SIG-FUNCTOR

$$ \Delta, \bar{\alpha}' \vdash_{\text{elab}} \mathcal{R}'_a <: \mathcal{R}_a[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma'_a <: \Sigma_a[\bar{\tau} \mapsto \bar{\alpha}] \Rightarrow f_a $$

$$ \Delta, \bar{\alpha}', (Y : (\mathcal{R}'_a, \Sigma'_a)) \vdash_{\text{elab}} S[\bar{\alpha} \mapsto \bar{\tau}] <: S' \rightsquigarrow \Pi[\bar{\alpha} \mapsto \bar{\tau}] <: \Pi' \Rightarrow f \quad Y \notin \Delta $$

$$ \Delta \vdash_{\text{elab}} \forall \bar{\alpha}. (Y : \mathcal{R}_a) \rightarrow S <: \forall \bar{\alpha}'. (Y : \mathcal{R}'_a) \rightarrow S' \rightsquigarrow \forall \bar{\alpha}. \Sigma_a \rightarrow \Pi <: \forall \bar{\alpha}'. \Sigma'_a \rightarrow \Pi' [\lambda (g : (\forall \bar{\alpha}. \Sigma_a \rightarrow \Pi)). \Lambda \bar{\alpha}'. \lambda (x : \Sigma'_a) . f (g \bar{\tau} (f_a x))] $$

## B.2.2 Typing

As for subtyping, the typing rules extend the canonical ones and produce an $F^\omega$ type (and term for module and bindings). When handling signatures and types, the lifting of existentials is just a rewriting. Producing the actual proof terms shows how the extension of scope is made using the repacking pattern. All the rules are given in §F.2.

**Binding typing rules** A binder is encoded with a single-field declaration record. The extrusion of existential types is illustrated in Rule E-TYP-DECL-MOD. In the sequence rule E-TYP-DECL-SEQ, two bindings are merged using a let-binding for renaming. The extension of scope needed to make the abstract types of the first declaration $\bar{\alpha}_1$ available to the rest also uses the repacking pattern.

E-TYP-DECL-MOD

$$ \Delta \vdash_{\text{elab}} M : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow e : \exists \bar{\alpha}. \Sigma \quad A.X \notin \Delta $$

$$ \begin{array}{l} \Delta \vdash_{\text{elab}} A \text{ (module } X = M\text{) : } (\exists \bar{\alpha}. \text{ module } X : \mathcal{R}) \quad \rightsquigarrow \text{ unpack}\langle \bar{\alpha}, y \rangle = e \text{ in } \text{pack}\langle \bar{\alpha}, \{\ell_X = y\} \rangle \\ \phantom{\Delta \vdash_{\text{elab}} A \text{ (module } X = M\text{) : } (\exists \bar{\alpha}. \text{ module } X : \mathcal{R}) \quad \rightsquigarrow \text{ unpack}\langle \bar{\alpha}, y \rangle = e \text{ in } \text{pack}\langle \bar{\alpha}, \{\ell_X = y\} \rangle} \\ \phantom{\Delta \vdash_{\text{elab}} A \text{ (module } X = M\text{) : } (\exists \bar{\alpha}. \text{ module } X : \mathcal{R}) \quad \rightsquigarrow \text{ unpack}\langle \bar{\alpha}, y \rangle = e \text{ in } \text{pack}\langle \bar{\alpha}, \{\ell_X = y\} \rangle} : (\exists \bar{\alpha}. \text{ module } X : \Sigma) \end{array} $$

E-TYP-DECL-SEQ

$$ \Delta \vdash_{\text{elab}} B_1 : \exists \bar{\alpha}_1. \mathcal{D}_1 \rightsquigarrow e_1 : \exists \bar{\alpha}_1. \{\zeta_1\} \quad \Delta, \bar{\alpha}_1, A.I_1 : (\mathcal{D}_1, \zeta_1) \vdash_{\text{elab}} \bar{B} : \exists \bar{\alpha}. \bar{\mathcal{D}} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\zeta}\} $$

$$ \begin{array}{l} \Delta \vdash_{\text{elab}} B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \bar{\mathcal{D}}_1, \bar{\mathcal{D}} \rightsquigarrow \begin{array}{@{}l@{}} \text{unpack}\langle \bar{\alpha}_1, x_1 \rangle = e_1 \text{ in} \\ \text{unpack}\langle \bar{\alpha}, x \rangle = (\text{let } A.I_1 = x_1. \ell_{I_1} \text{ in } e) \text{ in} \\ \text{pack}\langle \bar{\alpha}_1 \bar{\alpha}, \{\ell_I = x_1. \ell_I, \bar{\ell}_I = x. \ell_I\} \rangle \end{array} \\ : \exists \bar{\alpha}_1 \bar{\alpha}. \{\zeta_1, \bar{\zeta}\} \end{array} $$

**Module expressions typing** We only present the key typing rules for module expressions. The introduction of abstract types is done by sealing (E-TYP-MOD-SEALING), and features an explicit isolated packing (as opposed to a repacking). The application of functor (E-TYP-MOD-APP) shows how the polymorphic interface (universally quantified) is instantiated with types (obtained from the matching of the argument's and parameter's signatures). Finally, the projection rule (E-TYP-MOD-PROJ) illustrates another usage of the repacking pattern to collect
abstract types, project on the X submodule, and put back the abstract types.

<figure><img src="image_22.png" /></figure>

## B.3 Correctness and link with the canonical system

We write $\Delta^{\text{can}}$ and $\Delta^{\text{F}}$ for the left and right projections of the hybrid context $\Delta$, defined in the obvious way. We present implications as rules.

**Theorem 4 (Correctness of elaboration).** The elaboration judgment ensures well-typedness on both sides. For subtyping, we have the following result:

$$ \Delta \vdash^{\text{elab}} S <: S' \rightsquigarrow \Pi <: \Pi' \Rightarrow f \implies \left\{ \begin{array}{l} \Delta^{\text{F}} \vdash^{\text{can}} S <: S' \\ \Delta^{\text{F}} \vdash f : \Pi \rightarrow \Pi' \end{array} \right. \qquad (9) $$

For typing, we have the following result:

$$ \Delta \vdash^{\text{elab}} M : S \rightsquigarrow e : \Pi \implies \left\{ \begin{array}{l} \Delta^{\text{can}} \vdash^{\text{can}} M : S \\ \Delta^{\text{F}} \vdash e : \Pi \end{array} \right. \qquad (10) $$

Conversely, we show that well-typedness in the canonical system ensures that elaboration is well-defined. We first observe that there is an isomorphism between canonical and $F^{\omega}$-encoded signatures. This allows us, for a given signature $S$ (resp. $\mathcal{R}$) to consider its encoding in $F^{\omega}$, noted $\Pi_S$ (resp. $\Sigma_{\mathcal{R}}$). Similarly, we may consider the extension of an environment $\Gamma$ into a hybrid enriched environment $\Delta_{\Gamma}$ (we omit the definition.)

**Theorem 5 (Enrichment of canonical judgments).** The $F^{\omega}$ terms $(e, f, \Pi_S)$ corresponding to canonical derivation always exist. More formally, we have:

$$ \Gamma \vdash^{\text{can}} S : S \implies \Delta_{\Gamma} \vdash^{\text{elab}} S : S \rightsquigarrow \Pi_S \qquad (11) $$

$$ \Gamma \vdash^{\text{can}} S_1 <: S_2 \implies \exists f, \Delta_{\Gamma} \vdash^{\text{elab}} S_1 <: S_2 \rightsquigarrow \Pi_{S_1} <: \Pi_{S_2} \Rightarrow f \qquad (12) $$

$$ \Gamma \vdash^{\text{can}} M : S \implies \exists e, \Delta_{\Gamma} \vdash^{\text{elab}} M : S \rightsquigarrow e : \Pi_S \qquad (13) $$

# C Source system – Complete rules

## C.1 Resolution

### C.1.1 $\Gamma \vdash^{\text{src}} P \triangleright S$ – Path resolution
$$ \frac{\text{S-RES-LOCALMOD}}{\Gamma \vdash A.X \triangleright S} \in \Gamma $$

$$ \frac{\text{S-RES-FCTARG}}{\Gamma \vdash Y \triangleright S} \in \Gamma $$

$$ \frac{\text{S-RES-PROJ-MOD}}{\Gamma \vdash P \triangleright \text{sig}_A \bar{D} \text{ end}} \quad (\text{module } X : S) \in \bar{D} $$

$$ \frac{\text{S-RES-MODTYPE}}{\Gamma \vdash P \triangleright S} \quad \frac{\Gamma \vdash P \triangleright Q.T \quad \Gamma \vdash Q.T \triangleleft S}{\Gamma \vdash P \triangleright S} $$

### C.1.2 $\Gamma \vdash S \triangleleft S' - \text{Signature resolution}$

$$ \frac{\text{S-RES-LOCALSIG}}{\Gamma \vdash A.T \triangleleft S} \in \Gamma $$

$$ \frac{\text{S-RES-PROJ-MODTYPE}}{\Gamma \vdash P \triangleright \text{sig}_A \bar{D} \text{ end}} \quad (\text{module type } T = S) \in \bar{D} $$

$$ \frac{\text{S-RES-MODTYPE-REC}}{\Gamma \vdash Q.T \triangleleft Q'.T' \quad \Gamma \vdash Q'.T' \triangleleft S} $$

## C.2 Equivalence

### C.2.1 $\Gamma \vdash \tau \approx \tau' - \text{Type equivalence}$

$$ \frac{\text{S-EQV-TYPE-LOCAL}}{\Gamma \vdash A.t \approx \tau} \in \Gamma $$

$$ \frac{\text{S-EQV-TYPE-RES}}{\Gamma \vdash P \triangleright \text{sig}_A \bar{D} \text{ end}} \quad (\text{type } t = \tau) \in \bar{D} $$

$$ \frac{\text{S-EQV-TYPE-TRANS}}{\Gamma \vdash \tau_1 \approx \tau_2 \quad \Gamma \vdash \tau_2 \approx \tau_3} $$

$$ \frac{\text{S-EQV-TYPE-SYM}}{\Gamma \vdash \tau' \approx \tau} $$

$$ \frac{\text{S-EQV-TYPE-REFL}}{\Gamma \vdash \tau \approx \tau} $$

### C.2.2 $\Gamma \vdash_A D \approx D' - \text{Declaration equivalence}$
S-EQV-DECL-VAL

$$ \frac{\Gamma \vdash^{\text{src}} \tau \approx \tau'}{\Gamma \vdash_A^{\text{src}} (\text{val } x : \tau) \approx (\text{val } x : \tau')} $$

S-EQV-DECL-TYPE

$$ \frac{\Gamma \vdash^{\text{src}} \tau \approx \tau'}{\Gamma \vdash_A^{\text{src}} (\text{type } t = \tau) \approx (\text{type } t = \tau')} $$

S-EQV-DECL-MOD

$$ \frac{\Gamma \vdash^{\text{src}} S \approx S'}{\Gamma \vdash_A^{\text{src}} (\text{module } X : S) \approx (\text{module } X : S')} $$

S-EQV-DECL-MODTYPE

$$ \frac{\Gamma \vdash^{\text{src}} S \approx S'}{\Gamma \vdash_A^{\text{src}} (\text{module type } T = S) \approx (\text{module type } T = S')} $$

S-EQV-DECL-EMPTY

$$ \Gamma \vdash^{\text{src}} \emptyset \approx \emptyset $$

S-EQV-DECL-SEQ

$$ \frac{\Gamma \vdash_A^{\text{src}} D_1 \approx D'_1 \quad \Gamma, A.I_1 : D_1 \vdash_A^{\text{src}} \bar{D} \approx \bar{D'}}{\Gamma \vdash_A^{\text{src}} D_1, \bar{D} \approx D'_1, \bar{D'}} $$

### C.2.3 $\Gamma \vdash^{\text{src}} S \approx S'$ – Signature equivalence

S-EQV-SIG-MODTYPE

$$ \frac{\Gamma \vdash^{\text{src}} Q.T \Leftrightarrow S}{\Gamma \vdash^{\text{src}} Q.T \approx S} $$

S-EQV-SIG-FUNCTOR

$$ \frac{\Gamma \vdash^{\text{src}} S_a \approx S'_a \quad \Gamma, Y : S_a \vdash^{\text{src}} S \approx S'}{\Gamma \vdash^{\text{src}} (Y : S_a) \to S \approx (Y : S'_a) \to S'} $$

S-EQV-SIG-SIG

$$ \frac{\Gamma \vdash_A^{\text{src}} \bar{D} \approx \bar{D'}}{\Gamma \vdash^{\text{src}} \text{sig}_A \bar{D} \text{ end} \approx \text{sig}_A \bar{D'} \text{ end}} $$

S-EQV-SIG-TRANS

$$ \frac{\Gamma \vdash^{\text{src}} S \approx S' \quad \Gamma \vdash^{\text{src}} S' \approx S''}{\Gamma \vdash^{\text{src}} S \approx S''} $$

S-EQV-SIG-REFL

$$ \Gamma \vdash^{\text{src}} S \approx S $$

S-EQV-SIG-SYM

$$ \frac{\Gamma \vdash^{\text{src}} S' \approx S}{\Gamma \vdash^{\text{src}} S \approx S'} $$

## C.3 Strengthening

### C.3.1 $\Gamma \vdash S/P \gg S'$ – Signature strengthening

S-STR-SIG-FUNCTOR

$$ \Gamma \vdash (Y : S_a) \to S/P \gg (Y : S_a) \to S $$

S-STR-SIG-SIG

$$ \frac{\Gamma \vdash \bar{D}[A \mapsto P]/P \gg \bar{D'}}{\Gamma \vdash \text{sig}_A \bar{D} \text{ end}/P \gg \text{sig}_A \bar{D'} \text{ end}} $$

### C.3.2 $\Gamma \vdash D/P \gg D'$ – Declaration strengthening
S-STR-DECL-VAL

$$ \Gamma \vdash \text{val } x : \tau / P \gg \text{val } x : \tau $$

S-STR-DECL-TYPE

$$ \Gamma \vdash \text{type } t = \tau / P \gg \text{type } t = \tau $$

S-STR-DECL-MOD

$$ \Gamma \vdash S / (P \cdot X) \gg S' $$

$$ \Gamma \vdash (\text{module } X : S) / P \gg \text{module } X : S' $$

S-STR-DECL-MODTYPE

$$ \Gamma \vdash \text{module type } T = S / P \gg \text{module type } T = S $$

## C.4 Subtyping

Rules for both general and abstraction subtyping are shown, $<$: being either $<$: or $<>:$.

### C.4.1 $\Gamma \upharpoonright_S S <: S' - \text{Signature subtyping}$

S-SUB-SIG-EQUIV

$$ \Gamma \upharpoonright_S S \approx S' $$

$$ \Gamma \upharpoonright_S S <: S' $$

S-SUB-SIG-TRANS

$$ \Gamma \upharpoonright_S S <: S' \qquad \Gamma \upharpoonright_S S' <: S'' $$

$$ \Gamma \upharpoonright_S S <: S'' $$

S-SUB-SIG-FUNCTOR

$$ \Gamma \upharpoonright_{S_a'} S_a <: S_a \qquad \Gamma, Y : S_a' \upharpoonright_{S_a} S <: S' \qquad Y \notin \Gamma $$

$$ \Gamma \upharpoonright (Y : S_a) \to S <: (Y : S_a') \to S' $$

S-SUB-SIG-SIG

$$ \overline{D_0} \subseteq \overline{D} \qquad \Gamma, \overline{A \cdot D} \upharpoonright_{A}^{\text{src}} \overline{D_0} <: \overline{D'} $$

$$ \Gamma \upharpoonright_{\text{sig}_A}^{\text{src}} \overline{D} \text{ end} <: \text{sig}_A \overline{D'} \text{ end} $$

S-SUB-EQ-SIG-SIG

$$ \Gamma, \overline{A \cdot D} \upharpoonright_{\overline{D}}^{\text{src}} \overline{D} <: \overline{D'} $$

$$ \Gamma \upharpoonright_{\text{sig}_A}^{\text{src}} \overline{D} \text{ end} <: \text{sig}_A \overline{D'} \text{ end} $$

### C.4.2 $\Gamma \upharpoonright_A^S D <: D' - \text{Declaration subtyping}$

S-SUB-DECL-VAL

$$ \Gamma \upharpoonright_{\text{A}}^{\text{src}} \tau \approx \tau' \qquad \Gamma \upharpoonright_{\text{A}}^{\text{src}} (\text{val } x : \tau) <: (\text{val } x : \tau') $$

S-SUB-DECL-TYPE

$$ \Gamma \upharpoonright_{\text{A}}^{\text{src}} \tau \approx \tau' \qquad \Gamma \upharpoonright_{\text{A}}^{\text{src}} (\text{type } t = \tau) <: (\text{type } t = \tau') $$

S-SUB-DECL-MOD

$$ \Gamma \upharpoonright_{\text{A}}^{\text{src}} S <: S' \qquad \Gamma \upharpoonright_{\text{A}}^{\text{src}} (\text{module } X : S) <: (\text{module } X : S') $$

S-SUB-DECL-MODTYPE

$$ \Gamma \upharpoonright_{\text{A}}^{\text{src}} S <: S' \qquad \Gamma \upharpoonright_{\text{A}}^{\text{src}} S' <: S \qquad \Gamma \upharpoonright_{\text{A}}^{\text{src}} (\text{module type } T = S) <: (\text{module type } T = S') $$
## C.5 Typing

### C.5.1 $\Gamma \vdash_S : \checkmark$ – Signature typing

S-TYP-SIG-LOCALMODTYPE

$$ \frac{\Gamma \vdash_P T : \mathit{sig}_A \bar{D} \ \mathit{end}}{\Gamma \vdash_P T : \checkmark} \qquad \text{module type } T = S \in \bar{D} $$

S-TYP-SIG-MODTYPE

$$ \frac{A.T : \text{module type } T = S \in \Gamma}{\Gamma \vdash_A A.T : \checkmark} $$

S-TYP-SIG-FUNCTOR

$$ \frac{\Gamma \vdash S_a : \checkmark \quad \Gamma, Y : S_a \vdash_S : \checkmark \quad Y \notin \Gamma}{\Gamma \vdash (Y : S_a) \to S : \checkmark} $$

S-TYP-SIG-SIG

$$ \frac{\Gamma \vdash_A \bar{D} : \checkmark \quad A \notin \Gamma}{\Gamma \vdash \mathit{sig}_A \bar{D} \ \mathit{end} : \checkmark} $$

### C.5.2 $\Gamma \vdash_A^s D : \checkmark$ – Declarations typing

S-TYP-DECL-VAL

$$ \frac{\Gamma \vdash^s \tau : \checkmark \quad A.x \notin \Gamma}{\Gamma \vdash_A^s (\mathit{val} x : \tau) : \checkmark} $$

S-TYP-DECL-TYPE

$$ \frac{\Gamma \vdash^s \tau : \checkmark \quad A.t \notin \Gamma}{\Gamma \vdash_A^s (\mathit{type} t = \tau) : \checkmark} $$

S-TYP-DECL-TYPEABS

$$ \frac{A.t \notin \Gamma}{\Gamma \vdash_A^s (\mathit{type} t = A.t) : \checkmark} $$

S-TYP-DECL-MOD

$$ \frac{\Gamma \vdash_S : \checkmark \quad A.X \notin \Gamma}{\Gamma \vdash_A^S (\mathit{module} X : S) : \checkmark} $$

S-TYP-DECL-MODTYPE

$$ \frac{\Gamma \vdash_S : \checkmark \quad A.T \notin \Gamma}{\Gamma \vdash_A^S (\mathit{module} \ \mathit{type} \ T = S) : \checkmark} $$

S-TYP-DECL-EMPTY

$$ \Gamma \vdash_A^s \emptyset : \checkmark $$

S-TYP-DECL-SEQ

$$ \frac{\Gamma \vdash_A^s D_1 : \checkmark \quad \Gamma, A.I_1 : D_1 \vdash_A^s \bar{D} : \checkmark}{\Gamma \vdash_A^s (D_1, \bar{D}) : \checkmark} $$

### C.5.3 $\Gamma \vdash^s \tau : \checkmark$ – Type checking

S-TYP-TYPE-LOCALTYPE

$$ \frac{A.t : \mathit{type} t = \tau \in \Gamma}{\Gamma \vdash^s A.t : \checkmark} $$

S-TYP-TYPE-QUALIFIEDPATHTYPE

$$ \frac{\Gamma \vdash_P : \mathit{sig}_A \bar{D} \ \mathit{end}}{\Gamma \vdash_P t : \tau \in \bar{D}} $$

### C.5.4 $\Gamma \vdash_M : S$ – Module typing
### S-TYP-MOD-RES

$$ \frac{\Gamma \vdash_P P \triangleright S}{\Gamma \vdash_P P : S} $$

### S-TYP-MOD-STRENGTHEN

$$ \frac{\Gamma \vdash P : S}{\Gamma \vdash S/P \gg S'} \qquad \frac{\Gamma \vdash P : S'}{\Gamma \vdash P : S} $$

### S-TYP-MOD-EQUIV

$$ \frac{\Gamma \vdash M : S}{\Gamma \vdash M : S} \qquad \frac{\Gamma \vdash S \approx S'}{\Gamma \vdash S : S'} $$

### S-TYP-MOD-SEALING

$$ \frac{\Gamma \vdash S : \checkmark}{\Gamma \vdash P : S'} \qquad \frac{\Gamma \vdash S' < : S}{\Gamma \vdash (P : S) : S} $$

### S-TYP-MOD-FUNCTOR

$$ \frac{\Gamma \vdash S_a : \checkmark}{\Gamma ; (Y : S_a) \vdash M : S} \qquad \frac{}{Y \notin \Gamma} \qquad \frac{\Gamma \vdash (Y : S_a) \rightarrow M : (Y : S_a) \rightarrow S'}{\Gamma \vdash (Y : S_a) \rightarrow M : (Y : S_a) \rightarrow S'} $$

### S-TYP-MOD-FCTAPP

$$ \frac{\Gamma \vdash_P P : (Y : S_a) \rightarrow S}{\Gamma \vdash_P P' : S'_a} \qquad \frac{\Gamma \vdash S'_a < : S_a}{\Gamma \vdash_P P(P') : S[Y \mapsto P']$$

### S-TYP-MOD-STRUCT

$$ \frac{\Gamma \vdash_A \bar{B} : \bar{D}}{\Gamma \vdash \mathit{struct}_A \bar{B} \ \mathit{end} : \mathit{sig}_A \ \bar{D} \ \mathit{end}} \qquad A \notin \Gamma $$

### S-TYP-PROJ

$$ \frac{\Gamma \vdash_M \mathit{sig}_A (\bar{D}_1, \mathit{module} X : S, \bar{D}_2) \ \mathit{end}}{\Gamma \vdash_M X : S'} $$

### C.5.5 $\Gamma \vdash_A B : D$ – Bindings typing

#### S-TYP-BIND-LET

$$ \frac{\Gamma \vdash e : \tau}{\Gamma \vdash_A (\mathit{let} x = e) : (\mathit{val} x : \tau)} \qquad A.x \notin \Gamma $$

#### S-TYP-BIND-TYPE

$$ \frac{\Gamma \vdash \tau : \checkmark}{\Gamma \vdash_A (\mathit{type} t = \tau) : (\mathit{type} t = \tau)} \qquad A.t \notin \Gamma $$

#### S-TYP-BIND-ABSTRACTTYPE

$$ \frac{A.t \notin \Gamma}{\Gamma \vdash_A (\mathit{type} t = A.t) : (\mathit{type} t = A.t)} $$

#### S-TYP-BIND-MOD

$$ \frac{\Gamma \vdash M : S}{\Gamma \vdash_A (\mathit{module} X = M) : (\mathit{module} X : S)} \qquad A.X \notin \Gamma $$

#### S-TYP-BIND-MODTYPE

$$ \frac{\Gamma \vdash_S S : \checkmark}{\Gamma \vdash_A (\mathit{module} \ type \ T = S) : (\mathit{module} \ type \ T = S)} \qquad A.T \notin \Gamma $$

#### S-TYP-BIND-EMPTY

$$ \Gamma \vdash_A \emptyset : \emptyset $$

#### S-TYP-BIND-SEQ

$$ \frac{\Gamma \vdash_A B_1 : D_1}{\Gamma, A.I_1 : D_1 \vdash_A B_2 : D_2} \qquad \frac{}{\Gamma \vdash_A B_1, B_2 : D_1 ++ D_2} $$
# D Canonical system – Complete rules

## D.1 Subtyping

Rules for both general and abstraction subtyping are shown, $<$: being either $<$: or $<>:$.

### D.1.1 $\Gamma \vdash_S S' : S'$ – Signatures subtyping

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\text{C-SUB-SIG-FUNCTOR} & \Gamma, \bar{\alpha}' \vdash_R R' <: R[\bar{\alpha} \mapsto \bar{\tau}] & \Gamma, \bar{\alpha}', (Y : R') \vdash_S S[\bar{\alpha} \mapsto \bar{\tau}] <: S' & Y \notin \Gamma \\[2ex]
& \multicolumn{1}{c}{\Gamma \vdash \forall \bar{\alpha}. (Y : R) \to S <: \forall \bar{\alpha}'. (Y : R') \to S'} & &
\end{array}
$$

$$
\begin{array}{l}
\text{C-SUB-SIG-MATCH} \\
\quad \Gamma, \bar{\alpha} \vdash_R R <: R'[\bar{\alpha}' \mapsto \bar{\tau}] \\
\quad \Gamma \vdash \exists \bar{\alpha}. R <: \exists \bar{\alpha}'. R'
\end{array}
$$

$$
\begin{array}{l}
\text{C-SUB-SIG-SIG} \\
\quad \overline{\mathcal{D}_0 \subseteq \overline{\mathcal{D}} \qquad \Gamma \vdash \overline{\mathcal{D}_0} <: \overline{\mathcal{D}'}} \\
\quad \Gamma \vdash \operatorname{sig}_A \overline{\mathcal{D}} \text{ end} <: \operatorname{sig}_A \overline{\mathcal{D}'} \text{ end}
\end{array}
$$

$$
\begin{array}{l}
\text{C-SUBEQ-SIG-SIG} \\
\quad \Gamma \vdash \overline{\mathcal{D}} <: \overline{\mathcal{D}'} \\
\quad \Gamma \vdash \operatorname{sig}_A \overline{\mathcal{D}} \text{ end} <: \operatorname{sig}_A \overline{\mathcal{D}'} \text{ end}
\end{array}
$$

### D.1.2 $\Gamma \vdash_D D' : D'$ – Declarations subtyping

$$
\begin{array}{l}
\text{C-SUB-DECL-VAL} \\
\quad \Gamma \vdash \tau <: \tau' \\
\quad \Gamma \vdash (\text{val } x : \tau) <: (\text{val } x : \tau')
\end{array}
$$

$$
\begin{array}{l}
\text{C-SUB-DECL-TYPE} \\
\quad \Gamma \vdash \tau <: \tau' \\
\quad \Gamma \vdash (\text{type } t = \tau) <: (\text{type } t = \tau')
\end{array}
$$

$$
\begin{array}{l}
\text{C-SUB-DECL-MOD} \\
\quad \Gamma \vdash_R R <: R' \\
\quad \Gamma \vdash (\text{module } X : R) <: (\text{module } X : R')
\end{array}
$$

$$
\begin{array}{l}
\text{C-SUB-DECL-MODTYPE} \\
\quad \Gamma \vdash_R R <: R' \qquad \Gamma \vdash R' <: R \\
\quad \Gamma \vdash (\text{module type } T = \lambda \bar{\alpha}. R) <: (\text{module type } T = \lambda \bar{\alpha}. R')
\end{array}
$$

## D.2 Typing

### D.2.1 $\Gamma \vdash_{Q.t} \tau$ – Type checking

$$
\begin{array}{l}
\text{C-TYP-TYPE-LOCALTYPE} \\
\quad A.t : \text{type } t = \tau \in \Gamma \\
\quad \Gamma \vdash_{\text{can}} A.t : \tau
\end{array}
$$

$$
\begin{array}{l}
\text{C-TYP-TYPE-PATHTYPE} \\
\quad \Gamma \vdash P : \operatorname{sig}_A \overline{\mathcal{D}} \text{ end} \quad (\text{type } t = \tau) \in \overline{\mathcal{D}} \\
\quad \Gamma \vdash P.t : \tau
\end{array}
$$
### D.2.2 $\Gamma \vdash_A^{\text{can}} D : \lambda \bar{\alpha}.D$ – Declaration typing

**C-TYP-DECL-VAL**

$$ \Gamma \vdash^{\text{can}} \tau : \tau' \qquad A.x \notin \Gamma $$

$$ \Gamma \vdash_A^{\text{can}} val : \tau : val : x : \tau' $$

**C-TYP-DECL-TYPE**

$$ \Gamma \vdash^{\text{can}} \tau : \tau' \qquad A.t \notin \Gamma $$

$$ \Gamma \vdash_A^{\text{can}} type : \tau : type : t = \tau' $$

**C-TYP-DECL-TYPEABS**

$$ A.t \notin \Gamma $$

$$ \Gamma \vdash_A^{\text{can}} type : t = A.t : \lambda \alpha. type : t = \alpha $$

**C-TYP-DECL-MOD**

$$ \Gamma \vdash^{\text{can}} S : \lambda \bar{\alpha}.R \qquad A.X \notin \Gamma $$

$$ \Gamma \vdash_A^{\text{can}} (\text{module } X : S) : \lambda \bar{\alpha}. (\text{module } X : R) $$

**C-TYP-DECL-MODTYPE**

$$ \Gamma \vdash^{\text{can}} S : \lambda \bar{\alpha}.R \qquad A.T \notin \Gamma $$

$$ \Gamma \vdash_A^{\text{can}} (\text{module type } T = S) : (\text{module type } T = \lambda \bar{\alpha}.R) $$

**C-TYP-DECL-EMPTY**

$$ \Gamma \vdash_A^{\text{can}} \emptyset : \emptyset $$

**C-TYP-DECL-SEQ**

$$ \Gamma \vdash_A^{\text{can}} D_1 : \lambda \bar{\alpha}_1.D_1 \qquad \Gamma, \bar{\alpha}_1, A.I_1 : D_1 \vdash_A^{\text{can}} \bar{D} : \lambda \bar{\alpha}.\bar{D} $$

$$ \Gamma \vdash_A^{\text{can}} (D_1, \bar{D}) : \lambda \bar{\alpha}_1 \bar{\alpha}. (D_1, \bar{D}) $$

### D.2.3 $\Gamma \vdash^{\text{can}} S : \lambda \bar{\alpha}.R$ – Signature typing

**C-TYP-SIG-SIG**

$$ \Gamma \vdash_A^{\text{can}} \bar{D} : \lambda \bar{\alpha}.\bar{D} \qquad A \notin \Gamma $$

$$ \Gamma \vdash^{\text{can}} \text{sig}_A \bar{D} \text{ end} : \lambda \bar{\alpha}.\text{sig}_A \bar{D} \text{ end} $$

**C-CF-MODTYPE**

$$ \Gamma \vdash^{\text{can}} P : \text{sig}_A \bar{D} \text{ end} \qquad \text{module type } T = \lambda \bar{\alpha}.R \in \bar{D} $$

$$ \Gamma \vdash^{\text{can}} A.T : \lambda \bar{\alpha}.R $$

**C-TYP-SIG-LOCALMODTYPE**

$$ (A.T : \text{module type } T = \lambda \bar{\alpha}.R) \in \Gamma $$

$$ \Gamma \vdash^{\text{can}} A.T : \lambda \bar{\alpha}.R $$

**C-TYP-SIG-FUNCTOR**

$$ \Gamma \vdash^{\text{can}} S_a : \lambda \bar{\alpha}.R_a \qquad \Gamma, \bar{\alpha}, Y : R_a \vdash^{\text{can}} S : \lambda \bar{\beta}.R \qquad Y \notin \Gamma $$

$$ \Gamma \vdash^{\text{can}} (Y : S_a) \to S : \forall \bar{\alpha}. (Y : R_a) \to \exists \bar{\beta}.R $$

### D.2.4 $\Gamma \vdash^{\text{can}} M : S$ – Module typing
C-TYP-MOD-FCTARG
$(Y : \mathcal{R}) \in \Gamma$
$\Gamma \vdash^{\text{can}} Y : \mathcal{R}$

C-TYP-MOD-LOCAL
$(A.X : \mathcal{R}) \in \Gamma$
$\Gamma \vdash^{\text{can}} A.X : \mathcal{R}$

C-TYP-STRUCT
$\Gamma \vdash_A^{\text{can}} B : \exists \bar{\alpha}. \bar{D}$
$A \notin \Gamma$
$\Gamma \vdash \mathit{struct}_A B \mathit{end} : \exists \bar{\alpha}. \mathit{sig}_A \bar{D} \mathit{end}$

C-TYP-MOD-SEALING
$\Gamma \vdash^{\text{can}} S : \lambda \bar{\alpha}. \mathcal{R}$
$\Gamma \vdash^{\text{can}} P : \mathcal{R}'$
$\Gamma \vdash^{\text{can}} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}]$
$\Gamma \vdash (P : S) : \exists \bar{\alpha}. \mathcal{R}$

C-TYP-MOD-FUNCTOR
$\Gamma \vdash^{\text{can}} S : \lambda \bar{\alpha}. \mathcal{R}$
$\Gamma, \bar{\alpha}, (Y : \mathcal{R}) \vdash^{\text{can}} M : S$
$\Gamma \vdash^{\text{can}} (Y : S) \to M : \forall \bar{\alpha}. (Y : \mathcal{R}) \to S$

C-TYP-MOD-APP
$\Gamma \vdash^{\text{can}} P : \forall \bar{\alpha}. (Y : \mathcal{R}) \to S$
$\Gamma \vdash^{\text{can}} P' : \mathcal{R}'$
$\Gamma \vdash^{\text{can}} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}]$
$\Gamma \vdash^{\text{can}} P(P') : S[\bar{\alpha} \mapsto \bar{\tau}]$

C-TYP-MOD-PROJ
$\Gamma \vdash^{\text{can}} M : \exists \bar{\alpha}. \mathit{sig}_A \bar{D}_1, \mathit{module} X : \mathcal{R}, \bar{D}_2 \mathit{end}$
$\Gamma \vdash^{\text{can}} M.X : \exists \bar{\alpha}. \mathcal{R}$

### D.2.5 $\Gamma \vdash_A^{\text{can}} B : \exists \bar{\alpha}. \mathcal{D}$ – Bindings typing

C-TYP-DECL-LET
$\Gamma \vdash^{\text{can}} e : \tau$
$\Gamma \vdash^{\text{can}} \tau : \tau'$
$A.x \notin \Gamma$
$\Gamma \vdash_A^{\text{can}} (\mathit{let} x = e) : (\mathit{val} x : \tau')$

C-TYP-DECL-TYPE
$\Gamma \vdash^{\text{can}} \tau : \tau'$
$A.t \notin \Gamma$
$\Gamma \vdash_A^{\text{can}} (\mathit{type} t = \tau) : (\mathit{type} t = \tau')$

C-TYP-DECL-MOD
$\Gamma \vdash^{\text{can}} M : \exists \bar{\alpha}. \mathcal{R}$
$A.X \notin \Gamma$
$\Gamma \vdash_A^{\text{can}} (\mathit{module} X = M) : (\exists \bar{\alpha}. \mathit{module} X : \mathcal{R})$

C-TYP-DECL-MODTYPE
$\Gamma \vdash^{\text{can}} S : \lambda \bar{\alpha}. \mathcal{R}$
$A.T \notin \Gamma$
$\Gamma \vdash_A^{\text{can}} (\mathit{module} \ type \ T = S) : (\mathit{module} \ type \ T = \lambda \bar{\alpha}. \mathcal{R})$

C-TYP-DECL-EMPTY
$\Gamma \vdash_A^{\text{can}} \emptyset : \emptyset$

C-TYP-DECL-SEQ
$\Gamma \vdash_A^{\text{can}} B_1 : \exists \bar{\alpha}_1. \mathcal{D}_1$
$\Gamma, \bar{\alpha}_1, A.I_1 : \mathcal{D}_1 \vdash_A^{\text{can}} \bar{B} : \exists \bar{\alpha}. \bar{D}$
$\Gamma \vdash_A^{\text{can}} B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \bar{D}_1, \bar{D}$

## D.3 Anchoring
### D.3.1 $\Gamma \vdash \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' - \text{Type anchoring}$

$$
\begin{array}{c}
\text{C-ACH-TYPE-ANCHOR} \\
\Gamma \leftrightarrow \Gamma_s : \theta_\Gamma \qquad \theta_\Gamma(\alpha) = Q.t \\
\Gamma \vdash \alpha \leftrightarrow \Gamma_s; \theta_\Gamma \vdash Q.t
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-TYPE} \\
\Gamma \vdash \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset \\
\Gamma \vdash_A \text{ type } t = \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = \tau' : \emptyset
\end{array}
$$

### D.3.2 $\Gamma \vdash_A^{anc} D \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta$ - Declaration anchoring

$$
\begin{array}{c}
\text{C-ACH-DECL-VAL} \\
\Gamma \vdash^{anc} \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset \\
\Gamma \vdash^{anc}_A \text{ val } x : \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ val } x : \tau' : \emptyset
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-ANCHORPOINT} \\
\Gamma \leftrightarrow \Gamma_s : \theta_\Gamma \qquad \alpha \notin \text{dom}(\theta_\Gamma) \\
\Gamma \vdash_A^{anc} \text{ type } t = \alpha \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = A.t : (\alpha \mapsto t)
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-TYPE} \\
\Gamma \vdash \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset \\
\Gamma \vdash_A^{anc} \text{ type } t = \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = \tau' : \emptyset
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-MOD} \\
\Gamma \vdash \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta \\
\Gamma \vdash_A^{anc} \text{ module } X : \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ module } X : S : X.\theta
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-SIG} \\
\Gamma, \bar{\alpha} \vdash \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta \qquad \text{dom}(\theta) = \bar{\alpha} \\
\Gamma \vdash_A^{anc} \text{ module } T : \lambda\bar{\alpha}.\mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ module } T : S : \emptyset
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-SEQ} \\
\Gamma \vdash^{anc} D \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta \qquad \Gamma \vdash^{anc} \bar{D} \leftrightarrow (\Gamma_s, A.I : D); (\theta_\Gamma \uplus A.\theta) \vdash \bar{D} : \theta' \\
\Gamma \vdash^{anc}_A D, \bar{D} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D, \bar{D} : \theta_\Gamma \uplus \theta'
\end{array}
$$

### D.3.3 $\Gamma \vdash S : \lambda\bar{\alpha}.\mathcal{R}$ - Signature anchoring

$$
\begin{array}{c}
\text{C-ACH-SIG-FUNCTOR} \\
\Gamma, \bar{\alpha} \vdash \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S_a : \theta_a \\
\text{dom}(\theta_a) = \bar{\alpha} \qquad \Gamma, \bar{\alpha}, Y : \mathcal{R} \vdash S \leftrightarrow (\Gamma_s, Y : S_a); (\theta_\Gamma \uplus Y.\theta) \vdash S : \theta \\
\Gamma \vdash^{anc} \forall \bar{\alpha}. (Y : \mathcal{R}) \to S \leftrightarrow \Gamma_s; \theta_\Gamma \vdash (Y : S_a) \to S : \emptyset
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-SIG-SIG} \\
\Gamma \vdash_A^{anc} \bar{D} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \bar{D} : \theta \\
\Gamma \vdash^{anc} \text{ sig}_A \bar{D} \text{ end} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ sig}_A \bar{D} \text{ end} : \theta
\end{array}
$$
### D.3.4 $\Gamma \hookrightarrow \Gamma_s : \theta_\Gamma$ – Environment anchoring

$$ \begin{array}{c} \text{C-ACH-ENV-EMPTY} \\ \emptyset \hookrightarrow \emptyset : \emptyset \end{array} $$

$$ \begin{array}{c} \text{C-ACH-ENV-FCTARG} \\ \frac{\Gamma \hookrightarrow \Gamma_s : \theta_\Gamma \quad \Gamma, \bar{\alpha} \vdash_R^{anc} \mathcal{R} \hookrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta \quad \text{dom}(\theta) = \bar{\alpha}}{\Gamma, \bar{\alpha}, Y : \mathcal{R} \hookrightarrow (\Gamma_s, Y : S) : \theta_\Gamma \uplus Y.\theta} \end{array} $$

$$ \begin{array}{c} \text{C-ACH-ENV-DECL} \\ \frac{\Gamma \hookrightarrow \Gamma_s : \theta_\Gamma \quad \Gamma, \bar{\alpha} \vdash_A^{anc} D \hookrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta \quad \text{dom}(\theta) = \bar{\alpha}}{\Gamma, \bar{\alpha}, A.I : D \hookrightarrow (\Gamma_s, A.I : D) : \theta_\Gamma \uplus A.\theta} \end{array} $$

### D.3.5 $\Gamma \vdash^{anc} M : S$ – Anchorable typing

$$ \begin{array}{c} \text{C-TYPA-MOD-PROJ} \\ \frac{\Gamma \vdash^{anc} M : \exists \bar{\alpha}. \text{sig}_A \bar{D}_1, \text{module } X : \mathcal{R}, \bar{D}_2 \text{ end} \quad \Gamma \vdash^{anc} \exists \bar{\alpha}. \mathcal{R} \hookrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta}{\Gamma \vdash M.X : \exists \bar{\alpha}. \mathcal{R}} \end{array} $$
# E F<sup>ω</sup> – Complete rules

## E.1 Γ : **wf** – Environment checking

$$ \therefore \text{wf} \qquad \frac{\Gamma : \text{wf} \qquad \alpha \notin \Gamma}{\Gamma, \alpha : \kappa : \text{wf}} \qquad \frac{\Gamma \vdash \tau : \star \qquad x \notin \Gamma}{\Gamma, (x : \tau) : \text{wf}} $$

## E.2 Γ ⊢ τ : κ – Type checking

$$ \frac{\Gamma \vdash \tau_1 : \star \qquad \Gamma \vdash \tau_2 : \star}{\Gamma \vdash \tau_1 \to \tau_2 : \star} \qquad \frac{\Gamma \vdash \tau : \star \qquad \Gamma : \text{wf}}{\Gamma \vdash \{\overline{l_1} : \tau\} : \star} \qquad \frac{\Gamma : \text{wf}}{\Gamma \vdash \alpha : \Gamma(\alpha)} \qquad \frac{\Gamma, \alpha : \kappa \vdash \tau : \star}{\Gamma \vdash \forall \alpha : \kappa. \tau : \star} $$

$$ \frac{\Gamma, \alpha : \kappa \vdash \tau : \star}{\Gamma \vdash \exists \alpha : \kappa. \tau : \star} \qquad \frac{\Gamma, \alpha : \kappa \vdash \tau : \kappa'}{\Gamma \vdash \lambda \alpha : \kappa. \tau : \kappa \to \kappa'} \qquad \frac{\Gamma \vdash \tau_1 : \kappa' \to \kappa}{\Gamma \vdash \tau_1 \tau_2 : \kappa} $$

## E.3 Γ ⊢ e : τ – Term typing

$$ \frac{\Gamma : \text{wf}}{\Gamma \vdash x : \Gamma(x)} \qquad \frac{\Gamma, x : \tau \vdash e : \tau'}{\Gamma \vdash \lambda x : \tau. e : \tau \to \tau'} \qquad \frac{\Gamma \vdash e_1 : \tau' \to \tau}{\Gamma \vdash e_1 e_2 : \tau} $$

$$ \frac{\Gamma \vdash e : \tau}{\Gamma \vdash \{\overline{l} = e\} : \{\overline{l} : \tau\}} \qquad \frac{\Gamma \vdash e : \{l : \tau, \overline{l'} : \tau'\}}{\Gamma \vdash e.l : \tau} \qquad \frac{\Gamma, \alpha : \kappa \vdash e : \tau}{\Gamma \vdash \Lambda(\alpha : \kappa).e : \forall(\alpha : \kappa).\tau} $$

$$ \frac{\Gamma \vdash e : \forall \alpha : \kappa. \tau'}{\Gamma \vdash e \tau : \tau' [\tau \mapsto \alpha]} \qquad \frac{\Gamma \vdash \tau : \kappa}{\Gamma \vdash \text{pack} \langle \tau, e \rangle \text{ as } \exists \alpha : \kappa. \tau' : \star} \qquad \frac{\Gamma \vdash e : \tau' [\tau \mapsto \alpha]}{\Gamma \vdash \exists \alpha : \kappa. \tau' : \star} $$

$$ \frac{\Gamma \vdash e_1 : \exists \alpha : \kappa. \tau'}{\Gamma \vdash \text{unpack} \langle \alpha, x \rangle = e_1 \text{ in } e_2 : \tau} \qquad \frac{\Gamma, \alpha : \kappa, x : \tau' \vdash e_2 : \tau}{\Gamma \vdash \tau : \star} $$

# F Elaborated system – Complete rules

## F.1 Subtyping

### F.1.1 Δ ⊢ S <: S' ⇝ Π <: Π' ⇒ f – Signature subtyping
E-SUB-SIG-FUNCTOR

$$ \Delta, \bar{\alpha}' \vdash_R \mathcal{R}'_a <: \mathcal{R}_a[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma'_a <: \Sigma_a[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f_a $$

$$ \Delta, \bar{\alpha}', (Y : (\mathcal{R}'_a, \Sigma'_a)) \vdash_{\text{elab}} S[\bar{\alpha} \mapsto \bar{\tau}] <: S' \rightsquigarrow \Pi[\bar{\alpha} \mapsto \bar{\tau}] <: \Pi' \Rightarrow f \quad Y \notin \Delta $$

$$ \Delta \vdash \forall \bar{\alpha}. (Y : \mathcal{R}_a) \rightarrow S <: \forall \bar{\alpha}'. (Y : \mathcal{R}'_a) \rightarrow S' \rightsquigarrow \forall \bar{\alpha}. \Sigma_a \rightarrow \Pi <: \forall \bar{\alpha}'. \Sigma'_a \rightarrow \Pi' \\ [\lambda (g : (\forall \bar{\alpha}. \Sigma_a \rightarrow \Pi)). \Lambda \bar{\alpha}'. \lambda (x : \Sigma'_a) . f (g \bar{\tau} (f_a x))] $$

E-SUB-SIG-SIG

$$ \overline{D_0} \subseteq \overline{D} \qquad \Delta \vdash_{\overline{A}}^{\text{elab}} \overline{D_0} <: \overline{D}' \rightsquigarrow \overline{\zeta_0} <: \overline{\zeta} \Rightarrow \overline{f} $$

$$ \Delta \vdash_{\text{sig}_A}^{\text{elab}} \overline{D} \text{ end} <: \text{sig}_A \overline{D}' \text{ end} \rightsquigarrow \{\overline{\ell_I} : \overline{\zeta}\} <: \{\overline{\ell_I} : \overline{\zeta'}\} \Rightarrow \lambda x. \{\overline{\ell_{I_0}} : (f \overline{\zeta})\} $$

E-SUBEQ-SIG-SIG

$$ \Delta \vdash_{\overline{A}}^{\text{elab}} \overline{D} <: \overline{D}' \rightsquigarrow \overline{\zeta} <: \overline{\zeta'} \Rightarrow \overline{f} $$

$$ \Delta \vdash_{\text{sig}_A}^{\text{elab}} \overline{D} \text{ end} <: \text{sig}_A \overline{D}' \text{ end} \rightsquigarrow \{\overline{\ell_I} : \overline{\zeta}\} <: \{\overline{\ell_I} : \overline{\zeta'}\} \Rightarrow \lambda x. \{\overline{\ell_I} : (f \overline{\zeta})\} $$

### F.1.2 $\Delta \vdash_{\overline{A}}^{\text{elab}} \mathcal{D} <: \mathcal{D}' \rightsquigarrow \zeta <: \zeta' \Rightarrow f$ - Declaration subtyping

E-SUB-VAL

$$ \Delta \vdash \tau <: \tau' \uparrow f $$

$$ \Delta \vdash_{\overline{A}}^{\text{elab}} (\text{val } x : \tau) <: (\text{val } x : \tau') \rightsquigarrow [[\tau]] <: [[\tau')] \Rightarrow \lambda x. [[f(x.\text{val})]] $$

E-SUB-TYPE

$$ \Delta \vdash \tau <: \tau' \uparrow f $$

$$ \Delta \vdash_{\overline{A}}^{\text{elab}} (\text{type } t = \tau) <: (\text{type } t = \tau') \rightsquigarrow [[\tau : \kappa]] <: [[\tau' : \kappa]] \Rightarrow \lambda x. [[\tau' : \kappa]] $$

E-SUB-MOD

$$ \Delta \vdash \mathcal{R} <: \mathcal{R}' \rightsquigarrow \Sigma <: \Sigma' \Rightarrow f $$

$$ \Delta \vdash_{\overline{A}}^{\text{elab}} (\text{module } X : \mathcal{R}) <: (\text{module } X : \mathcal{R}') \rightsquigarrow [[\Sigma]] <: [[\Sigma']]) \Rightarrow \lambda x. [[f(x.\text{mod})]] $$

E-SUB-MODTYPE

$$ \Delta, \bar{\alpha} \vdash_{\mathcal{R}}^{\text{elab}} \mathcal{R}' <: \mathcal{R}' \rightsquigarrow \Sigma <: \Sigma' \Rightarrow f \qquad \Delta, \bar{\alpha} \vdash_{\mathcal{R}'}^{\text{elab}} \mathcal{R}' <: \mathcal{R}' \rightsquigarrow \Sigma' <: \Sigma \Rightarrow f' $$

$$ \Delta \vdash_{\overline{A}}^{\text{elab}} (\text{module type } T = \lambda \bar{\alpha}. \mathcal{R}) <: (\text{module type } T = \lambda \bar{\alpha}. \mathcal{R}') \rightsquigarrow [[\lambda \bar{\alpha}. \Sigma]] <: [[\lambda \bar{\alpha}. \Sigma']]) \Rightarrow \lambda x. [[\lambda \bar{\alpha}. \Sigma']]) $$

## F.2 Typing

### F.2.1 $\Delta \vdash Q.t : \tau$ - Type checking
E-TYP-TYPE-LOCALTYPE

$$A.t : (\mathit{type} t = \tau, \mathit{type} t = \tau) \in \Delta$$

$$\Delta \vdash^{\mathit{elab}} A.t : \tau$$

E-TYP-TYPE-PATHTYPE

$$\frac{\Delta \vdash^{\mathit{elab}} P : \mathit{sig}_A \bar{D} \mathit{end} \rightsquigarrow_- : \Sigma \quad (\mathit{type} t = \tau) \in \bar{D} \quad \Sigma.\ell_t : \langle\langle \tau \rangle\rangle}{\Delta \vdash P.t : \tau}$$

$$\Delta \vdash^{\mathit{elab}} P.t : \tau$$

### F.2.2 $\Delta \vdash_A^\mathit{elab} D : \lambda\bar{\alpha}.D \rightsquigarrow \lambda\bar{\alpha}.\zeta$ - Declaration typing

E-TYP-DECL-VAL

$$\Delta \vdash^{\mathit{elab}} \tau : \tau'$$

$$A.x \notin \Delta$$

$$\Delta \vdash^{\mathit{elab}}_A val : \tau : val : \tau' \rightsquigarrow val : \tau'$$

E-TYP-DECL-TYPE

$$\Delta \vdash^{\mathit{elab}} \tau : \tau'$$

$$A.t \notin \Delta$$

$$\Delta \vdash^{\mathit{elab}}_A type : \tau : type : \tau' \rightsquigarrow type : \tau'$$

E-TYP-DECL-TYPEABS

$$A.t \notin \Delta$$

$$\Delta \vdash_A^{\mathit{elab}} type : A.t : \lambda\alpha. type : \alpha \rightsquigarrow \lambda\alpha. type : \alpha$$

E-TYP-DECL-MOD

$$\Delta \vdash^{\mathit{elab}} S : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma$$

$$A.X \notin \Delta$$

$$\Delta \vdash_A^{\mathit{elab}} (\mathit{module} X : S) : \lambda\bar{\alpha}. (\mathit{module} X : \mathcal{R}) \rightsquigarrow \lambda\bar{\alpha}. \mathit{module} X : \Sigma$$

E-TYP-DECL-MODTYPE

$$\Delta \vdash^{\mathit{elab}} S : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma$$

$$A.T \notin \Delta$$

$$\Delta \vdash_A^{\mathit{elab}} (\mathit{module} \ type \ T = S) : (\mathit{module} \ type \ T = \lambda\bar{\alpha}.\mathcal{R}) \rightsquigarrow (\mathit{module} \ type \ T = \lambda\bar{\alpha}.\Sigma)$$

E-TYP-DECL-EMPTY

$$\Delta \vdash_A^{\mathit{elab}} \emptyset : \emptyset \rightsquigarrow \emptyset$$

E-TYP-DECL-SEQ

$$\Delta \vdash_A^{\mathit{elab}} D_1 : \lambda\bar{\alpha}_1.D_1 \rightsquigarrow \lambda\bar{\alpha}_1.\zeta_1$$

$$\Delta, \bar{\alpha}_1, A.I_1 : (D_1, \zeta_1) \vdash_A^{\mathit{elab}} \bar{D} : \lambda\bar{\alpha}.\bar{D} \rightsquigarrow \lambda\bar{\alpha}.\bar{\zeta}$$

$$\Delta \vdash_A^{\mathit{elab}} (D_1, \bar{D}) : \lambda\bar{\alpha}_1 \bar{\alpha}. (D_1, \bar{D}) \rightsquigarrow \lambda\bar{\alpha}_1 \bar{\alpha}. (\zeta_1, \bar{\zeta})$$

### F.2.3 $\Delta \vdash S : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma$ - Signature typing
E-TYP-SIG-SIG

$$ \Delta \vdash_A \bar{D} : \lambda \bar{\alpha}. \bar{D} \rightsquigarrow \lambda \bar{\alpha}. \bar{\zeta} \quad A \notin \Delta $$

$$ \Delta \vdash \mathit{sig}_A \bar{D} \mathit{end} : \lambda \bar{\alpha}. \mathit{sig}_A \bar{D} \mathit{end} \rightsquigarrow \lambda \bar{\alpha}. \{\bar{\zeta}\} $$

E-CF-MODTYPE

$$ \Delta \vdash_P \mathit{sig}_A \bar{D} \mathit{end} \rightsquigarrow \mathit{\Sigma}' \quad \mathit{module type} \ T = \lambda \bar{\alpha}. \mathcal{R} \in \bar{D} \quad \mathit{\Sigma}' . \ell_T : \langle \langle \lambda \bar{\alpha} . \mathcal{\Sigma} \rangle \rangle \rangle $$

$$ \Delta \vdash \mathit{A.T} : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \mathcal{\Sigma} $$

E-TYP-SIG-LOCALMODTYPE

$$ A.I : (\mathit{module type} \ T = \lambda \bar{\alpha}. \mathcal{R}, \mathit{module type} \ T = \lambda \bar{\alpha}. \mathcal{\Sigma}) \in \Delta $$

$$ \Delta \vdash \mathit{A.T} : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \mathcal{\Sigma} $$

E-TYP-SIG-FUNCTOR

$$ \Delta \vdash^{\mathit{elab}} S_a : \lambda \bar{\alpha}. \mathcal{R}_a \rightsquigarrow \lambda \bar{\alpha}. \mathcal{\Sigma}_a \quad \Delta, \bar{\alpha}, Y : (\mathcal{R}_a, \mathcal{\Sigma}_a) \vdash^{\mathit{elab}} S : \lambda \bar{\beta}. \mathcal{R} \rightsquigarrow \lambda \bar{\beta}. \mathcal{\Sigma} \quad Y \notin \Delta $$

$$ \Delta \vdash^{\mathit{elab}} (Y : S_a) \rightarrow S : \forall \bar{\alpha}. (Y : \mathcal{R}_a) \rightarrow \exists \bar{\beta}. \mathcal{R} \rightsquigarrow \forall \bar{\alpha}. \mathcal{\Sigma}_a \rightarrow \exists \bar{\beta}. \mathcal{\Sigma} $$

### F.2.4 $\Delta \vdash M : S \rightsquigarrow e : \Pi$ - Module typing
E-TYP-MOD-FCTARG

$$Y : (\mathcal{R}, \Sigma) \in \Delta$$

$$\Delta \vdash_{\text{elab}} Y : \mathcal{R} \rightsquigarrow Y : \Sigma$$

E-TYP-MOD-LOCAL

$$A.X : (\mathcal{R}, \Sigma) \in \Delta$$

$$\Delta \vdash_{\text{elab}} A.X : \mathcal{R} \rightsquigarrow A.X : \Sigma$$

E-TYP-STRUCT

$$\Delta \vdash_{\text{elab}}^{} B : \exists \bar{\alpha}. \bar{D} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\zeta}\} \quad A \notin \Delta$$

$$\Delta \vdash_{\text{elab}} \mathit{struct}_A B \mathit{end} : \exists \bar{\alpha}. \mathit{sig}_A \bar{D} \mathit{end} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\zeta}\}$$

E-TYP-MOD-SEALING

$$\Delta \vdash_{\text{elab}}^{} S : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \Sigma$$

$$\Delta \vdash_{\text{elab}}^{} P : \mathcal{R}' \rightsquigarrow e : \Sigma'$$

$$\Delta \vdash_{\text{elab}}^{} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma' < : \Sigma[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f$$

$$\Delta \vdash_{\text{elab}}^{} (P : S) : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow \mathit{pack}(\bar{\tau}, (f e)) : \lambda \bar{\alpha}. \Sigma$$

E-TYP-MOD-FUNCTOR

$$\Delta \vdash_{\text{elab}}^{} S : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \Sigma$$

$$\Delta, \bar{\alpha}, Y : (\mathcal{R}, \Sigma) \vdash_{\text{elab}}^{} M : S \rightsquigarrow e : \Pi$$

$$\Delta \vdash_{\text{elab}}^{} (Y : S) \rightarrow M : \forall \bar{\alpha}. (Y : \mathcal{R}) \rightarrow S \rightsquigarrow \forall \bar{\alpha}. \lambda(Y : \mathcal{R}) . e : \forall \bar{\alpha}. \Sigma \rightarrow \Pi$$

E-TYP-MOD-APP

$$\Delta \vdash_{\text{elab}}^{} P : \forall \bar{\alpha}. (Y : \mathcal{R}) \rightarrow S \rightsquigarrow e_P : \forall \bar{\alpha}. \Sigma \rightarrow S$$

$$\Delta \vdash_{\text{elab}}^{} P' : \mathcal{R}' \rightsquigarrow e : \Sigma'$$

$$\Delta \vdash_{\text{elab}}^{} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma' < : \Sigma[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f$$

$$\Delta \vdash_{\text{elab}}^{} P(P') : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow e_P \bar{\tau} (f e) : \Pi[\bar{\alpha} \mapsto \bar{\tau}]$$

E-TYP-MOD-PROJ

$$\Delta \vdash_{\text{elab}}^{} M : \exists \bar{\alpha}. \mathit{sig}_A \bar{D}_1, \mathit{module} X : \mathcal{R}, \bar{D}_2 \mathit{end} \rightsquigarrow e : \{\bar{\zeta}_1, \ell_X : \Sigma, \bar{\zeta}_2\}$$

$$\Delta \vdash_{\text{elab}}^{} M.X : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow \mathit{unpack}(\bar{\alpha}, y) = e \text{ in } \mathit{pack}(\bar{\alpha}, e.\ell_X) : \exists \bar{\alpha}. \Sigma$$

**F.2.5** $\Delta \vdash_{\text{elab}}^{} B : \exists \bar{\alpha}. \mathcal{D} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\ell}_I : \bar{\zeta}\} - \text{Bindings typing}$
E-TYP-DECL-LET

$$
\begin{array}{l}
\Delta \vdash_{\text{elab}} e : \tau \rightsquigarrow e' : \tau' \qquad \Delta \vdash_{\text{elab}} \tau : \tau' \qquad A.x \notin \Delta \\[1em]
\Delta \vdash_{A} (\text{let } x = e) : (\text{val } x : \tau') \rightsquigarrow \{\ell_x = e'\} : (\text{val } x : \tau')
\end{array}
$$

E-TYP-DECL-TYPE

$$
\begin{array}{l}
\Delta \vdash_{\text{elab}} \tau : \tau' \qquad A.t \notin \Delta \\[1em]
\Delta \vdash_{A}^{\text{elab}} (\text{type } t = \tau) : (\text{type } t = \tau') \rightsquigarrow \{\ell_t = \langle\langle \tau' \rangle\rangle\} : (\text{type } t = \tau')
\end{array}
$$

E-TYP-DECL-MOD

$$
\begin{array}{l}
\Delta \vdash_{\text{elab}} M : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow e : \exists \bar{\alpha}. \Sigma \qquad A.X \notin \Delta \\
\\
\Delta \vdash_{A}^{\text{elab}} (\text{module } X = M) : (\exists \bar{\alpha}. \text{module } X : \mathcal{R}) \rightsquigarrow \text{unpack}(\bar{\alpha}, y) = e \text{ in } \text{pack}(\bar{\alpha}, \{\ell_X = y\}) \\
\phantom{\Delta \vdash_{A}^{\text{elab}} (\text{module } X = M) : (\exists \bar{\alpha}. \text{module } X : \mathcal{R}) \rightsquigarrow \text{unpack}(\bar{\alpha}, y) = e \text{ in }} : \exists \bar{\alpha}. \text{module } X : \Sigma
\end{array}
$$

E-TYP-DECL-MODTYPE

$$
\begin{array}{l}
\Delta \vdash_{\text{elab}} S : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \Sigma \qquad A.T \notin \Delta \\
\\
\Delta \vdash_{A}^{\text{elab}} (\text{module type } T = S) : (\text{module type } T = \lambda \bar{\alpha}. \mathcal{R}) \rightsquigarrow \{\ell_T = \langle\langle \lambda \bar{\alpha}. \mathcal{R} \rangle\rangle\} \\
\phantom{\Delta \vdash_{A}^{\text{elab}} (\text{module type } T = S) : (\text{module type } T = \lambda \bar{\alpha}. \mathcal{R}) \rightsquigarrow \{\ell_T = \langle\langle \lambda \bar{\alpha}. \mathcal{R} \rangle\rangle\} : (\text{module type } T = \lambda \bar{\alpha}. \mathcal{R})}
\end{array}
$$

E-TYP-DECL-SEQ

$$
\begin{array}{l}
\Delta \vdash_A^{\text{elab}} B_1 : \exists \bar{\alpha}_1. \mathcal{D}_1 \rightsquigarrow e_1 : \exists \bar{\alpha}_1. \{\zeta_1\} \qquad \Delta, \bar{\alpha}_1, A.I_1 : (\mathcal{D}_1, \zeta_1) \vdash_A^{\text{elab}} \bar{B} : \exists \bar{\alpha}. \bar{\mathcal{D}} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\zeta}\} \\
\\
\Delta \vdash_A^{\text{elab}} B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \overline{\mathcal{D}_1}, \bar{\mathcal{D}} \rightsquigarrow \mathit{unpack}(\bar{\alpha}_1, x_1) = e_1 \text{ in } \quad : \exists \bar{\alpha}_1 \bar{\alpha}. \{\zeta_1, \bar{\zeta}\} \\
\phantom{\Delta \vdash_A^{\text{elab}} B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \overline{\mathcal{D}_1}, \bar{\mathcal{D}} \rightsquigarrow \mathit{unpack}(\bar{\alpha}_1, x_1) = e_1 \text{ in }} \mathit{unpack}(\bar{\alpha}, x) = (\text{let } A.I_1 = x_1. \ell_{I_1} \text{ in } e) \text{ in} \\
\phantom{\Delta \vdash_A^{\text{elab}} B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \overline{\mathcal{D}_1}, \bar{\mathcal{D}} \rightsquigarrow \mathit{unpack}(\bar{\alpha}, x) = (\text{let } A.I_1 = x_1. \ell_{I_1} \text{ in } e) \text{ in }} \mathit{pack}(\bar{\alpha}_1 \bar{\alpha}, \{\ell_I = x_1. \ell_{I_1}, \bar{\ell}_I = x. \ell_{I_1}\})
\end{array}
$$