Clément Blaudeau

Didier Rémy

Gabriel Radanne

Remy Didier

Retrofitting OCaml modules

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 datastructure, 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 development: 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 language. 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

Reachable space

Signature avoidance

Describable space

Incorrect avoidance Over abstraction

Common use-cases 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 typechecker 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 (overabstraction) or (2) failing at inferring the signature (incorrect avoidance). parametric instances of data structures (sets, hashtables, streams, etc.). Several successful projects have made heavy use of modules, as in MirageOS [START_REF] Madhavapeddy | Unikernels: library operating systems for the cloud[END_REF] where modules and functors are even assembled on demand using a DSL [START_REF] Radanne | Programming unikernels in the large via functor driven development[END_REF]. 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 [START_REF] White | Modular implicits[END_REF] where new modules could be built automatically from their signatures by applications of functors to other modules.

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- 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 inscope 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.

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 ω was already explored by Mitchell [START_REF] Mitchell | Abstract types have existential types[END_REF]. This vision was opposed by [START_REF] Macqueen | Using Dependent Types to Express Modular Structure[END_REF], 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 [START_REF] Harper | Higher-order modules and the phase distinction[END_REF], supported the idea that dependent types may actually be too powerful (thus, unnecessarily complex) for module systems. SML modules were first described by [START_REF] Harper | Higher-order modules and the phase distinction[END_REF]. Two approaches for the formalization and improvement of abstract types in SML were later concomitantly described by [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF] (through manifest types) and [START_REF] Harper | A type-theoretic approach to higher-order modules with sharing[END_REF] (via an adapted F ω with translucent sums). The OCaml module system itself was specified by [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF][START_REF] Leroy | A modular module system[END_REF], and later with an extension to applicative functors [START_REF] Leroy | Applicative functors and fully transparent higher-order modules[END_REF]. The use of existential types to interpret signatures by [START_REF] Russo | Types for modules[END_REF] opened the door for a simplified link between modules and F ω . 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 [START_REF] Montagu | Modeling Abstract Types in Modules with Open Existential Types[END_REF] introducing the concept of open existential types. Pushing Russo's idea further, a closer correspondence between ML-modules and F ω was achieved by [START_REF] Rossberg | F-ing modules[END_REF] by elaborating a significant subset of the SML module syntax into F ω . The type system is safe by construction, inheriting the property from F ω . 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, [START_REF] Rossberg | 1ML -Core and modules united[END_REF] achieved a unification of the core and module languages (thus, un-stratified) using F ω as the underlying programming language and seeing module constructs as syntactic sugar. More recently, [START_REF] Crary | A focused solution to the avoidance problem[END_REF] 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.

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 [START_REF] Rossberg | F-ing modules[END_REF] translation into F ω to present a new set of typing rules. However, reasoning only by elaboration in F ω 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 [START_REF] Russo | Types for modules[END_REF], 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.

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.

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 and types of the core language. Lists are written with an overhead bar: 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 selfreferences 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 Γ, 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 = τ (resp. module X = P ) and deleting constraints S with type t := τ (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.

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.

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 .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 Γ src P S which gives the signature S of a path P and a signature resolution judgment Γ src Q.T S, which retrieves the definition S of a module type Q.T (both in an environment Γ).

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.

S-Res-Modtype

Γ src P Q.T Γ src Q.T S Γ src P S S-Res-Proj-Mod Γ src P sig A D end (module X : S) ∈ D Γ src P.X S[A → P ]

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 With transitivity, symmetry, and reflexivity, we get an equivalence relationship on types.

S-Eqv-Type-Res

Γ src P sig A D end (type t = τ ) ∈ D Γ src P.t ≈ τ [A → P ] S-Eqv-Type-Local (A.t : type t = τ ) ∈ Γ Γ src A.t ≈ τ
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.

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 Γ P/S 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 (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 (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. Functor signatures are not strengthened, as they do not introduce new abstract types. The full set of rules is given in §C.3.

S-Str-Sig-Sig Γ D[A → P ] /P D Γ sig A D end/P sig A D end S-Str-Decl-Mod
Γ S/ (P.X) S Γ (module X : S) /P module X : S

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 Γ src S 1 : S 2 , which has no computational content and Subtyping, written Γ src S 1 <: 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 D and D are compared directly as shown in rule S-Sub-Sig-Sig. In the general form of subtyping, a subset D 0 of the declaration list D is compared with D , allowing for reordering and deletion, as shown in Rule S-Sub-Sig. Using a subset instead of a subsequence allows for reordering.

S-SubEq-Sig-Sig Γ, A.D src D : D Γ src sig A D end : sig A D end S-Sub-Sig-Sig D 0 ⊆ D Γ, A.D src A D 0 <: D Γ src sig A D end <: sig A D 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).

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 Γ src S : and declarations typing Γ src A D : ensure that no shadowing occurs and no free variables are used. We omit the rules here. The judgment for bindings Γ src 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. 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 Γ, D 1 src S : 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 D 1 , so that the resulting signature S is wellformed in Γ. 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.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: 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 pathbased 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 ω . 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.

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.

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. We distinguish between manifest canonical signatures R that only refer to abstract types bound in the context and abstract canonical signatures ∃α.R (written S) that also specify the existential types α 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 F ω style λ-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.

Signature typing

We start with signature typing Γ

Γ can A D 1 : λα 1 .D 1 Γ, α 1 , A.I 1 : D 1 can A D : λα.D Γ can A D 1 , D : λα 1 α. D 1 , D C-Typ-Sig-Functor Γ can Sa : λα.Ra Γ, α, Y : Ra can S : λβ.R Y / ∈ Γ Γ can (Y : Sa) → S : ∀α. (Y : Ra) → ∃β.R

Subtyping

The subtyping between two canonical signatures ∃α.R and ∃α .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 α created by the left-hand-side signature are made available (i.e., pushed in the context), while the right-hand-side ones α are instantiated with some types τ . If both signatures define the same abstract types (up to α-conversion), a simple renaming instantiation α → α is sufficient. Otherwise, the left-hand-side signature R can be less abstract (i.e., binding fewer abstract types) than the right-hand-side one 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 Γ can S 1 : S 2 and general subtyping Γ can S 1 <: 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 ≺: being either <: or :.

C-Sub-Sig-Match Γ, α can R ≺: R α → τ Γ can ∃α.R ≺: ∃α .R C-Sub-Sig-Functor Γ, α can R ≺: R[α → τ ] Γ,

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. 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 . In the source presentation, the projection rule S-Typ-Mod-Proj is the only place where signature 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 α and remain bound in the signature of M.X. The full set of typing rules is given in §D.2.

Module expressions typing

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:

Γ can Γ s Γ can A D : λα.D Γ, α, (A.I : D) can Γ s , (A.I : D)
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.

Γ

s src P S ∧ Γ can Γ s ∧ Γ can S : λα.R =⇒ Γ can P : R (1) Γ s src Q.T S ∧ Γ can Γ s ∧ Γ can S : λα.R =⇒ Γ can Q.T : λα.R (2)
Canonification of strengthening Via resolution, the introduction of abstract types is reexposed 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:

Γ s src P S ∧ Γ s S/P S ∧ Γ can Γ s ∧ Γ can S : λα.R =⇒ Γ can S : R (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:

Γ s src S 1 ≈ S 2 ∧ Γ can Γ s ∧ Γ can S 1 : S 1 ∧ Γ can S 2 : S 2 =⇒ S 1 = S 2 (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:

Γ s src S 1 <: S 2 ∧ Γ can Γ s ∧ Γ can S 1 : S 1 ∧ Γ can S 2 : S 2 =⇒ Γ can S 1 <: S 2 (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:

Γ s src M : S ∧ Γ can Γ s ∧ Γ can S : S =⇒ Γ can M : S ∧ Γ can S : 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.

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.

Quantification vs structural information

The key insight is the semantic difference in the source syntax between the declaration of a concrete type (type t = τ ) and that of an abstract type (type t). 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 : 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 type1 : 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.

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 α is used. If it is at the top level of a type declaration type t = α, we say that the existential type α 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 α in the canonical signature. The type t must be the first reference to the abstract type α, regardless of whether or not it is the original definition point. If the type α is used earlier, we raise a signature avoidance failure.

Example 5 illustrates the process of finding the first available position to rewire the typesharing tree of Example 1. We see the change of the defining instance of α, 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 θ : α → Q.t. We define a signature anchoring judgment Γ anc S → Γ s ; θ Γ S : θ that, given an environment Γ and a canonical signature S, produces a source environment Γ s associated with an anchoring map θ Γ and a source signature S associated with an anchoring map θ. 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 Γ anc M : S. The judgment is defined by a copy of the typing rules for the judgment Γ can 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.

X.t X.u Y.a Y.b Y.c α Canonical signature S 1 → X.u Y.a Y.b Y.c X.t Source signature S 1 X.t X.u Y.a Y.b Y.c α Canonical signature S 2 → X.t X.u Y.b Y.c Y.a Source signature S 2
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 α is anchorable. For S 1 , we can use X.t for the handle to α, 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:

Γ anc M : S ∧ Γ anc S → Γ s ; θ Γ S : θ =⇒ Γ s src M : S (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 ω 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 ω , 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.

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 Γ anc S → Γ s ; θ Γ S : θ states that, given a canonical signature S and environment Γ, we can build a corresponding source signature S and source environment Γ s . Both are returned with an anchoring map (θ for the signature and θ Γ for the environment) that gives a path Q.t for the handle of every abstract type α.

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 α → 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 . The map associated with the left-hand-side declaration is prefixed with the self-reference. More generally, we write Q.θ as a shortcut for the map α → Q.θ(α).

C-Ach-Decl-AnchorPoint Γ → Γ s : θ Γ α / ∈ dom(θ Γ ) Γ anc A type t = α → Γ s ; θ Γ type t = A.t : (α → t) C-Ach-Decl-Type Γ anc τ → Γ s ; θ Γ τ : ∅ Γ anc A type t = τ → Γ s ; θ Γ type t = τ : ∅ C-Ach-Decl-Seq Γ anc D → Γ s ; θ Γ D : θ Γ anc D → (Γ s , A.I : D) ; (θ Γ A.θ) D : θ Γ anc A D, D → Γ s ; θ Γ D, D : θ Γ θ
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.

C-Ach-Env-Decl Γ → Γ s : θ Γ Γ, α anc A D → Γ s ; θ Γ D : θ dom(θ) = α Γ, α, A.I : D → (Γ s , A.I : D) : θ Γ A.θ

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:

C-TypA-Mod-Proj Γ anc M : ∃α.sig A D 1 , module X : R, D 2 end Γ anc ∃α.R → Γ s ; θ Γ S : θ Γ anc M.X : ∃α.R
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 Γ, module M and (canonical) signature S, the anchored signature S is a valid signature for the source typing:

Γ anc M : S Γ anc S → Γ s ; θ Γ S : θ    =⇒ Γ s src M : S (7)
The proof of this theorem uses the following lemma :

Lemma 1 (Anchorability of subtyping). Given Γ, Γ s , σ Γ , two canonical signatures S 1 and S 2 , two source signatures S 1 and S 2 , and two substitutions σ 1 and σ 2 , we have:

Γ anc S → Γ s ; θ Γ S : θ Γ anc S → Γ s ; θ Γ S : θ Γ can S <: S        =⇒ Γ s src S <: S (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 ω 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 ω and elaboration

To properly finish the transition from source to F ω via the canonical system, we are missing one final link from the canonical system to F ω . In this section we give formal foundations and guarantees for the canonical system through elaboration into F ω : the elaboration is defined by hybrid judgments that relate module expressions and canonical signatures to terms and types of F ω . This gives a precise correspondence between the key mechanisms of the canonical system, in particular existential types, and standard mechanisms of F ω . The canonical system can actually be understood as a particular mode of use of F ω . Thanks to F ω , 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 ω types. Hence, the elaboration is mostly straightforward.

Although, we use F ω as the target language, we do not actually need the power of F ω to model generative functors. The reason to pursue the development in F ω 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 ω (extended with existential types and records) that we use for the elaboration and present the F ω 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 ω .

This section is largely inspired by [START_REF] Rossberg | F-ing modules[END_REF]. We only made minor changes to the encoding of module expressions and signatures: the encoding of module types use λ-abstraction rather than existential quantification; declarations are encoded differently. The main difference is the extension of the judgments to produce both the F ω type and the canonical signature, whereas in [START_REF] Rossberg | F-ing modules[END_REF], typing and subtyping are only defined by elaboration.

κ := Ω | κ → κ (kinds) ρ := α | ρ → ρ | { : ρ} | ∀α : κ.ρ | ∃α : κ.ρ | λα : κ.ρ | ρ ρ (types) E := x | λx : ρ.E | E E | { = E} | E. | λα : κ.E | E ρ | pack ρ, E ρ | unpack α, x = E in E (terms) W := λx : ρ.E | { = W } | λα : κ.E | pack ρ, W ρ (values) Γ := • | Γ, α : κ | Γ, x : ρ (environments)

B.1 F-omega and encoded signatures

We use a standard variant of explicitly typed F ω with primitive records and existential types;

We only give its syntax in Figure 6; its typing rules are available in §E. We use letters ρ and E to range over types and expressions so as to distinguish them from the core language types and expressions, τ and e, although these should be seen as a subset of ρ and E. While kinds are part of terms, we usually omit them in F ω terms for the sake of conciseness and readability.

To help with the elaboration, we assume a collection I of record labels indexed by identifiers of the canonical (and source) system. The encoding of the canonical system into F ω 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:

ρ := ∀(β : κ → ).β ρ → β ρ (Type) ρ := Λ(β : κ → ).λ(x : β ρ).x (Term)
This allows to represent type fields as F ω 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 β 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 ω 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.

Π = ∃α        X : t : α v : α u : α × bool        ∃α        module X : type t = α val v : α type u = α × bool        Encoded module E = unpack α 1 , y 1 = pack int, { X = { t = int , v = 42}} in unpack ∅, y 2 = { u = (α 1 × bool) } in pack α 1 , { X = (y 1 . X ), u = (y 2 . 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 ∆ that contains both canonical and F ω terms, defined as follows:

∆ ::= ∅ | ∆, α | ∆, (Y : (R, Σ)) | ∆, (A.I : (D, ζ))
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 ∆ elab S 1 <: S 2 Π 1 <: Π 2 ⇒ 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 : Π 1 → Π 2 . The nature of this subtyping function gives interesting insights on the compilation of modules. For abstraction-only subtyping, the subtyping function is βη-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 τ ) 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 ∆, α elab R a <: R a [α → τ ] Σ a <: Σ a [τ → α] ⇒ f a ∆, α , (Y : (R a , Σ a )) elab S[α → τ ] <: S Π[α → τ ] <: Π ⇒ f Y / ∈ ∆ ∆ elab ∀α. (Y : R a ) → S <: ∀α . (Y : R a ) → S ∀α. Σ a → Π <: ∀α . Σ a → Π [λ (g : (∀α. Σ a → Π)) . Λα .λ (x : Σ a ) . f (g τ (f a x))]

B.2.2 Typing

As for subtyping, the typing rules extend the canonical ones and produce an F ω 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 α 1 available to the rest also uses the repacking pattern.

: Σ) E-Typ-Decl-Seq ∆ elab A B 1 : ∃α 1 .D 1 e 1 : ∃α 1 . {ζ 1 } ∆, α 1 , A.I 1 : (D 1 , ζ 1 ) elab A B : ∃α.D e : ∃α. ζ ∆ elab A B 1 , B : ∃α 1 α.D 1 , D unpack α 1 , x 1 = e 1 in unpack α, x = (let A.I 1 = x 1 . I1 in e) in pack α 1 α, I = x 1 . I , I = x. I : ∃α 1 α. ζ 1 , ζ
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.

B.3 Correctness and link with the canonical system

We write ∆ can and ∆ F for the left and right projections of the hybrid context ∆, 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:

∆ elab S <: S Π <: Π ⇒ f =⇒    ∆ F can S <: S ∆ F f : Π → Π (9)
For typing, we have the following result:

∆ elab M : S e : Π =⇒    ∆ can can M : S ∆ F e : Π (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 ω -encoded signatures. This allows us, for a given signature S (resp. R) to consider its encoding in F ω , noted Π S (resp. Σ R ). Similarly, we may consider the extension of an environment Γ into a hybrid enriched environment ∆ Γ (we omit the definition.)

Theorem 5 (Enrichment of canonical judgments). The F ω terms (e, f , Π S ) corresponding to canonical derivation always exist. More formally, we have:

  Two examples of modules and associated type-sharing trees.

SourceFigure 2 :

 2 Figure 2: The different systems: their links, with theorems and sections.

Figure 3 :

 3 Figure 3: Syntax of the module language

Figure 4 :

 4 Figure 4: Structure of judgments for the source system

  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 . o u t s t r e n g t h e n i n g w it h st re ng th en in g Example 3: Strengthening and its graphical interpretation S-Eqv-Type-Local: a type is equivalent to its definition (and only to itself for abstract types).

  type T = S) ≺: (module type T = S )

  Sa) → M : (Y : Sa) → S S-Typ-Mod-App Γ src P : (Y : Sa) → S Γ src P : S a Γ src S a <: Sa Γ src P (P ) : S Y → P S-Typ-Mod-Proj Γ src M : sig A D1, module X : S, D2 end Γ,

Figure 5 :

 5 Figure 5: Syntax extensions of the canonical module language.

AC

  can S : λα.R and declaration typing Γ can A D : λα.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. type t = A.t : λα. type t = α X : S) : λα. (module X : R) C-Typ-Decl-Seq

  end : sig A D end

  X = M ) : ∃α.(module X : R) type T = S) : (module type T = λα.R) C-Typ-Decl-Seq Γ can A B1 : ∃α1.D1 Γ, α1, A.I1 : D1 can A B : ∃α.D Γ can A B1, B : ∃α1α.D1, D

M

  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 [α → τ ]. : ∃α.sig A D1, module X : R, D2 end Γ can M.X : ∃α.R

Figure 6 :

 6 Figure 6: Syntax of F ω

  X = M ) : (∃α. module X : R) unpack α, y = e in pack α, { X = y} : (∃α. module X

  R[α → τ ] Σ <: Σ[α → τ ] ⇒ f ∆ elab (P : S) : ∃α.R pack τ , (f e) : λα.Σ R[α → τ ] Σ <: Σ[α → τ ] ⇒ f∆ elab P (P ) : R[α → τ ] e τ (f e ) : Π[α → τ ] E-Typ-Mod-Proj ∆ elab M : ∃α.sig A D1, module X : R, D2 end e : ζ1, X : Σ, ζ2 ∆ elab M.X : ∃α.R unpack α, y = e in pack α, e. X : ∃α.Σ

PDFFFF

  : S 2 =⇒ ∃f, ∆ Γ elab S 1 <: S 2 Π S1 <: Π S2 ⇒ f x : τ ) ≈ (val x : τ ) t = τ ) ≈ (type t = τ ) X : S) ≈ (module X : S ) type T = S) ≈ (module type T = S )Rules for both general and abstraction subtyping are shown, ≺: being either <: or :. Y : R) → S ≺: ∀α . (Y : R ) → SC-Sub-Sig-Match Γ, α can R ≺: R [α → τ ] Γ can ∃α.R ≺: ∃α .R C-Sub-Sig-Sig D 0 ⊆ D Γ can D 0 <: D Γ can sig A D end <: sig A D end C-SubEq-Sig-Sig x : τ ) ≺: (val x : τ ) t = τ ) ≺: (type t = τ ) : R) ≺: (module X : R ) type T = λα.R) ≺: (module type T = λα.R ) : sig A D end (type t = τ ) ∈ D Γ can P.t : τ D.3.1 Γ anc τ → Γ s ; θ Γ τ -Type anchoring C-Ach-Type-Anchor Γ → Γ s : θ Γ θ Γ (α) = Q.t Γ anc α → Γ s ; θ Γ Q.t C-Ach-Decl-Type Γ anc τ → Γ s ; θ Γ τ : ∅ Γ anc A type t = τ → Γ s ; θ Γ type t = τ : ∅ D.3.2 Γ anc A D → Γ s ; θ Γ D : θ -Declaration anchoring C-Ach-Decl-Val Γ anc τ → Γ s ; θ Γ τ : ∅ Γ anc A val x : τ → Γ s ; θ Γ val x : τ : ∅ C-Ach-Decl-AnchorPoint Γ → Γ s : θ Γ α / ∈ dom(θ Γ ) Γ anc A type t = α → Γ s ; θ Γ type t = A.t : (α → t) C-Ach-Decl-Type Γ anc τ → Γ s ; θ Γ τ : ∅ Γ anc A type t = τ → Γ s ; θ Γ type t = τ : ∅ C-Ach-Decl-Mod Γ anc R → Γ s ; θ Γ S : θ Γ anc A module X : R → Γ s ; θ Γ module X : S : X.θ C-Ach-Decl-Sig Γ, α anc R → Γ s ; θ Γ S : θ dom(θ) = α Γ anc A module T : λα.R → Γ s ; θ Γ module T : S : ∅ C-Ach-Decl-Seq Γ anc D → Γ s ; θ Γ D : θ Γ anc D → (Γ s , A.I : D) ; (θ Γ A.θ) D : θ Γ anc A D, D → Γ s ; θ Γ D, D : θ Γ θ s ; θ Γ S a : θ a dom(θ a ) = α Γ, α, Y : R anc S → (Γ s , Y : S a ) ; (θ Γ Y.θ) S : θ Γ anc ∀α. (Y : R) → S → Γ s ; θ Γ (Y : S a ) → S : ∅ C-Ach-Sig-Sig Γ anc A D → Γ s ; θ Γ D : θ Γ anc sig A D end → Γ s ; θ Γ sig A D end : θ D.3.4 Γ → Γ s : θ Γ -Environment anchoring C-Ach-Env-Empty ∅ → ∅ : ∅ C-Ach-Env-FctArg Γ → Γ s : θ Γ Γ, α anc R → Γ s ; θ Γ S : θ dom(θ) = α Γ, α, Y : R → (Γ s , Y : S) : θ Γ Y.θ C-Ach-Env-Decl Γ → Γ s : θ Γ Γ, α anc A D → Γ s ; θ Γ D : θ dom(θ) = α Γ, α, A.I : D → (Γ s , A.I : D) : θ Γ A.θ D.3.5 Γ anc M : S -Anchorable typing C-TypA-Mod-Proj Γ anc M : ∃α.sig A D 1 , module X : R, D 2 end Γ anc ∃α.R → Γ s ; θ Γ S : θ Γ anc M.X : ∃α.R E F ω -Complete rules E.1 Γ : wf -Environment checking • : wf Γ : wf α / ∈ Γ Γ, α : κ : wf Γ e 1 : ∃α : κ.τ Γ, α : κ, x : τ e 2 : τ Γ τ : Γ unpack α, x = e 1 in e 2 : τ : R a [α → τ ] Σ a <: Σ a [α → τ ] ⇒ f a ∆, α , (Y : (R a , Σ a )) elab S[α → τ ] <: S Π[α → τ ] <: Π ⇒ f Y / ∈ ∆ ∆ elab ∀α. (Y : R a ) → S <: ∀α . (Y : R a ) → S ∀α. Σ a → Π <: ∀α . Σ a → Π [λ (g : (∀α. Σ a → Π)) . Λα .λ (x : Σ a ) . f (g τ (f a x))] E-Sub-Sig-Sig D 0 ⊆ D ∆ elab A D 0 <: D ζ 0 <: ζ ⇒ f ∆ elab sig A Dend <: sig A D end I : ζ <: I : ζ ⇒ λx. I0 : (f ζ) E-SubEq-Sig-Sig ∆ elab A D <: D ζ <: ζ ⇒ f ∆ elab sig A D end <: sig A D end I : ζ <: I : ζ ⇒ λx. I : (f ζ) x : τ ) <: (val x : τ ) τ <: τ ⇒ λx. f (x.val) t = τ ) <: (type t = τ ) τ : κ <: τ : κ ⇒ λx. τ : κ E-Sub-Mod ∆ elab R <: R Σ <: Σ ⇒ f ∆ elab A (module X : R) <: (module X : R ) Σ <: Σ ⇒ λx. f (x.mod) type T = λα.R) <: (module type T = λα.R ) λα.Σ <: λα.Σ ⇒ λx. λα.Σ end : λα.sig A D end λα. ζ E-Cf-ModType ∆ elab P : sig A D end : Σ module type T = λα.R ∈ D Σ . T : λα.Σ ∆ elab A.T : λα.R λα.Σ E-Typ-Sig-LocalModType A.I : (module type T = λα.R, module type T = λα.Σ) ∈ ∆ ∆ elab A.T : λα.R λα.Σ E-Typ-Sig-Functor ∆ elab S a : λα.R a λα.Σ a ∆, α, Y : (R a , Σ a ) elab S : λβ.R λβ.Σ Y / ∈ ∆ ∆ elab (Y : S a ) → S : ∀α. (Y : R a ) → ∃β.R ∀α.Σ a → ∃β.Σ

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 ≺: being either <: or : S-Sub-Decl-Type Γ src τ ≺: τ Γ src A (type t = τ ) ≺: (type t = τ ) S-Sub-Decl-ModType

Module typingThe 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 Γ src P S Γ src P : S S-Typ-Mod-Sealing Γ src S : Γ src P : S Γ src S <: S Γ src (P : S) : S S-Typ-Mod-Struct Γ src

C-Typ-StructΓ can A B : ∃α.D A / ∈ Γ Γ can structA B end : ∃α.sig A D end C-Typ-Mod-Sealing Γ can S : λα.R Γ can

C-Cf-Empty ∅ can ∅ C-Cf-FctArg Γ can Γ s Γ can S : λα.R Γ, α, (Y : R) can Γ s , (Y : S) C-Cf-Decl

Adding a type field for t would not work, as it would not be an equivalent signature.

src τ ≈ τ -Type equivalence S-Eqv-Type-Local (A.t : type t = τ ) ∈ Γ Γ src A.t ≈ τ S-Eqv-Type-Res Γ src P sig A D end (type t = τ ) ∈ D Γ src P.t ≈ τ [A → P ] S-Eqv-Type-Trans Γ src τ 1 ≈ τ 2 Γ src τ 2 ≈ τ 3 Γ src τ 1 ≈ τ 3 S-Eqv-Type-Sym Γ src τ ≈ τ Γ src τ ≈ τ S-Eqv-Type-Refl Γ src τ ≈ τ C.2.2 Γ src A D ≈ D -Declaration equivalence

A D 1 , D ≈ D 1 , D C.2.3 Γ src S ≈ S -Signature equivalence S-Eqv-Sig-Modtype Γ src Q.T S Γ src Q.T ≈ S S-Eqv-Sig-Functor Γ src S a ≈ S a Γ, Y : S a src S ≈ S Γ src (Y : S a ) → S ≈ (Y : S a ) → S S-Eqv-Sig-Sig Γ src A D ≈ D Γ src sig A D end ≈ sig A D end S-Eqv-Sig-Trans Γ src S ≈ S Γ src S ≈ S Γ src S ≈ S S-Eqv-Sig-Refl Γ src S ≈ S S-Eqv-Sig-Sym Γ src S ≈ S Γ src S ≈ S C.3 Strengthening C.3.1 Γ S/P S -Signature strengthening S-Str-Sig-Functor Γ (Y : S a ) → S/P (Y : S a ) → S S-Str-Sig-Sig Γ D[A → P ] /P D Γ sig A D end/P sig A D end C.3.2 Γ D/P D -Declaration strengthening

Γ τ :x / ∈ Γ Γ, (x : τ ) : wf E.2 Γ τ : κ -Type checkingΓ τ 1 : Γ τ 2 : Γ τ 1 → τ 2 : Γ τ : Γ : wf Γ l : τ : Γ : wf Γ α : Γ(α) Γ, α : κ τ : Γ ∀α : κ.τ : Γ, α : κ τ : Γ ∃α : κ.τ : Γ, α : κ τ : κ Γ λα : κ.τ : κ → κ Γ τ 1 : κ → κ Γ τ 2 : κ Γ τ 1 τ 2 : κ E.3 Γ e : τ -Term typing Γ : wf Γ x : Γ(x) Γ, x : τ e : τ Γ λx : τ.e : τ → τ Γ e 1 : τ → τ Γ e 2 : τ Γ e 1 e 2 : τΓ e : τ Γ : wf Γ l = e : l : τ Γ e : l : τ, l : τ Γ e.l : τ Γ, α : κ e : τ Γ Λ(α : κ).e : ∀(α : κ).τ Γ e : ∀α : κ.τ Γ τ : κ Γ e τ : τ [τ → α] Γ τ : κ Γ e : τ [τ → α] Γ ∃α : κ.τ : Γ pack τ, e as ∃α : κ.τ : ∃α : κ.τ

S-Res-LocalMod


Bureaucraties sans fonctionnaires

Alors que le gouvernement a présenté en 2021 un plan de 2,2 milliards d'euros pour le développement de l'intelligence artificielle en France, ses applications sont déjà largement en usage, y compris dans l'administration et les services publics. Mais dans une bureaucratie automatisée, aucune marge de manoeuvre n'est plus possible pour l'application des règles inscrites dans les dispositifs, aucun lanceur d'alerte ne pourra plus avertir d'éventuelles dérives : l'automatisation bureaucratique a le potentiel de faire advenir un gouvernement totalement déshumanisé.

Depuis quelques années, à grand renfort d'un vocable issu du monde des « startups », on assiste à la consolidation d'un nouvel avatar de la réforme néo-libérale de l'État. À travers les concepts d'« État plateforme » ou de « start-up d'État » (Algan & Cazenave 2016 ;Bertholet & Létourneau 2017 ;[START_REF] Pezziardi | Des startups d'État à l'État plateforme[END_REF], les nouveaux réformateurs comptent sur les « corporate hackers » et l'innovation disruptive pour transformer de l'intérieur les bureaucraties publiques, laisser libre cours à la créativité, renouer avec la transparence, déployer des méthodes « agiles » et s'adapter à un environnement en perpétuelle transformation, le tout à moindre coût.

L'« État digital » -un concept vanté en juin 2017 par Emmanuel Macron lors d'une ode à la « startup nation » restée célèbre -est aussi et surtout un État en voie d'automatisation : pour accompagner l'horizon du non-remplacement de près de 50 000 fonctionnaires d'ici à 2022, le plan Action Publique 2022 lancé en octobre 2018 misait sur des « technologies telles que l'intelligence artificielle et les RPA (« robotic process automation »), ce afin « d'automatiser les tâches répétitives et à faible valeur ajoutée » (Gouvernement français 2018).

Le contexte est en effet propice à l'automatisation de nombreuses fonctions administratives. Outre la conversion d'une partie des élites politiques et administratives au concept de « gouvernance par les données », l'offre technologique des prestataires privés s'est aussi structurée, grâce notamment au développement rapide des techniques dites d'« intelligence artificielle » (IA). Du côté des « administrés », ce projet rencontre une plus grande acculturation de la population française au numérique, avec un taux d'équipement important et de nombreux programmes pour la « former » aux outils numériques, que ce soit à l'initiative des pouvoirs publics ou d'entreprises comme Google (accueillie à bras ouverts par plusieurs villes françaises pour installer ses « ateliers numériques »). Rappelons toutefois qu'en 2020, près de 10 millions de résidents français ne bénéficiaient pas d'accès à Internet (soit parce qu'ils ne disposent pas d'abonnement, soit qu'ils ne disposent pas d'équipements adéquats) (Arcep 2021, 308) et que trois français sur dix s'estimaient incompétents pour réaliser des démarches administratives en ligne [START_REF] Charrel | Illectronisme : les laissés-pour-compte du tout-numérique[END_REF].

Ces différents facteurs poussent à une multiplication des « assemblages algorithmiques » (Ananny & Crawford 2018) dans les administrations. Que ce soit la dématérialisation de nombreuses démarches administratives, l'automatisation partielle de l'affectation post-Bac avec Parcoursup, l'automatisation de l'accompagnement des demandeurs d'emploi avec le projet « Mon Assistant Personnel » expérimenté par Pôle Emploi, l'automatisation de la lutte contre la fraude sociale par les caisses d'allocation familiale ou par le fisc, l'automatisation du contrôle d'identité via la reconnaissance faciale des bornes PARAFE installées dans plusieurs aéroports, ou encore l'automatisation des communications ou comportements suspects au sein des services de police ou de renseignement, nombre de pratiques administratives sont aujourd'hui de plus en plus articulées à des algorithmes semi-autonomes.

Face à ce processus, des craintes s'expriment dans certains segments de la société -qui en dénoncent de nombreux angles morts. Sont notamment évoqués les risques pour la vie privée, l'avènement d'une « société de contrôle » appuyée sur l'informatique, l'opacité des assemblages algorithmiques, les formes aggravées de déshumanisation induites par l'automatisation ou encore l'accentuation des inégalités structurelles. Au sein même des bureaucraties concernées par ces transformations, la peur du déclassement de l'humain par la machine, le surcroît de procédures, le risque de bugs techniques ou le phénomène rampant de privatisation suscitent également leur lot de résistances parmi les agents.

Ces risques ont conduit à la multiplication de nombreux rapports, livres blancs ou textes de soft-law émanant du secteur privé, d'organismes de protection des données comme la CNIL, d'institutions comme le Parlement européen mais aussi d'organisations internationales comme le Conseil de l'Europe ou le Conseil des droits de l'Homme des Nations Unies.

Certains travaux en sociologie des sciences et des techniques ont pourtant montré la faible portée pratique des approches procédurales proposées dans de tels rapports, les règles ainsi posées étant souvent inapplicables, contournées, ou privées de leurs effets. Sur le plan juridique, l'expérience montre que les « gardefous » adoptés par le législateur ou les juges s'avèrent très fragiles. Compte tenu des logiques bureaucratiques d'optimisation (fonctionnelle, budgétaire, etc.) des tâches administratives, l'innovation technologique (dans le contrôle d'identité, le placement des bacheliers, etc.) tend systématiquement à créer un besoin, lequel se traduit tôt ou tard par des réformes visant à légaliser des usages qui paraissaient auparavant inenvisageables techniquement ou inacceptables socialement.

En réduisant les enjeux à des questions de procédures -donc à des questions souvent techniques sur la manière de réguler l'usage d'un dispositif -et en se focalisant sur les artefacts technologiques en négligeant leur environnement institutionnel, les controverses actuelles tendent à multiplier les angles morts de ces projets d'automatisation bureaucratique.

Par exemple, il est une question fondamentale dont il est rarement débattu : quelle serait la signification politique d'une bureaucratie presque entièrement automatisée ? La critique des tendances anti-démocratiques du pouvoir bureaucratique a occupé une place importante dans la théorie politique depuis le XIX e siècle. Mais sans minimiser les formes de violences associées aux bureaucraties passées et présentes, il n'en demeure pas moins qu'en pratique, leur potentiel dystopique peut être en partie contenu par les femmes et les hommes en leur sein.

C'est ce que soulignent de nombreux travaux en sociologie politique. Pour Michael Mann par exemple, la critique de Max Weber à l'encontre des bureaucraties exagère l'ampleur du pouvoir qu'elles peuvent imprimer sur la société : selon lui, puisque l'État doit procéder au recrutement massif de fonctionnaires pour garnir les rangs de bureaucraties toujours plus tentaculaires, le « pouvoir infrastructurel » de l'État sur la « société civile » se développe au prix d'une pénétration de ses propres structures administratives par cette même société civile, qui au travers de ces fonctionnaires toujours plus nombreux est en mesure d'influencer l'État (Mann 2012, 59). Dans une approche qui a le mérite d'éviter une opposition trop binaire entre État et « société civile », Timothy Mitchell évoque lui aussi les formes de résistance internes nourries par des « sujets politiques [. . . ] formés au sein de la sphère organisationnelle dénommée État » (Mitchell 2018, 372).

De manière plus empirique, la sociologie de l'action publique a largement souligné le rôle joué par les « street-level bureaucrats » -c'est-à-dire les agents placés au contact direct des administrés -dans le travail d'interprétation et d'adaptation des règles aux réalités des publics et des terrains [START_REF] Dubois | Le rôle des street-level bureaucrats dans la conduite de l'action publique en France[END_REF]. Au sein de la discipline, un débat a cours depuis une vingtaine d'années pour élucider les effets de l'introduction des technologies informatiques vis-à-vis de ce travail d'interprétation [START_REF] Snellen | Electronic Governance: Implications for Citizens, Politicians and Public Servants[END_REF][START_REF] Buffat | Street-Level Bureaucracy and e-Government[END_REF]. Si ces effets apparaissent ambivalents, il reste que, dans un certain nombre de contextes, la technologie rend d'ores et déjà quasiment impossible une telle herméneutique. Et quand bien même davantage d'études de terrain seraient nécessaires pour l'évaluer précisément, on peut s'attendre à ce que l'automatisation croissante de certaines tâches administratives en lien avec les dernières innovations technologiques rognent encore davantage sur les marges de manoeuvre laissées aux « street-level bureaucrats ».

Ce pourrait d'ailleurs être là l'un des ressorts tacites du mouvement d'automatisation bureaucratique. Si, comme le suggère l'anthropologue David [START_REF] Graeber | Bureaucratie: L'utopie des règles, Paris, Les Liens qui libèrent Mann, Michael[END_REF], la bureaucratie est « faite, d'abord et avant tout, d'agressions contre ceux qui persistent à défendre d'autres schémas ou des interprétations différentes », il n'est guère surprenant qu'elle appréhende la subjectivité de ses agents comme un aléas dispensable, en abordant le fonctionnaire et ses dilemmes moraux comme un bug à corriger. Dans une bureaucratie automatisée, aucune désobéissance possible dans l'application de la règle inscrite dans le dispositif, plus aucun lanceur d'alerte dont la conscience pourra être à ce point heurtée par la violence bureaucratique qu'il ou elle se décidera à porter l'affaire à la connaissance du public. En évinçant l'élément humain dans l'application des règles rationnelles et impersonnelles, l'automatisation bureaucratique a le potentiel de faire advenir le gouvernement totalement déshumanisé que décrivait Hannah Arendt (2003) au tournant des années 1960 : « dans une bureaucratie pleinement développée, il ne reste plus personne avec qui l'on puisse discuter, à qui l'on puisse présenter des griefs ».

Cette analyse signale un autre angle mort d'une bureaucratie sans fonctionnaires : le fait d'accepter d'être administré par des machines ne conduit-il pas à rompre avec l'horizon politique de l'humanisme, en acceptant de nous concevoir nousmêmes -personnes administrées -comme des machines, c'est-à-dire comme les objets d'un gouvernement plutôt que des sujets politiques ? Le droit libéral considère en effet que, même si les motivations et les états mentaux d'autrui ne peuvent pas toujours être sondés, ils sont en fait équivalents aux nôtres. Selon cette conception, autrui est réputé doué des mêmes facultés que nous, animé lui aussi par une volonté et des désirs. C'est ce qui fait de lui un pair devant jouir de droits et d'une dignité égale à la nôtre. Même si le fait d'être administré par des organisations bureaucratiques constitue bien une forme de dépossession et de violence, au moins est-elle en partie rendue plus tolérable (car plus « négociable ») par l'existence d'interlocuteurs humains (en espérant que ces personnes pourront user à bon escient d'une certaine marge d'interprétation).

Dès lors que cet « élément humain » disparaît, dès lors que ne subsiste plus que le fonctionnement froid et impénétrable d'un algorithme fondé sur des simplifications abstraites et une approche quantitative et probabiliste du réel (fût-il paramétré par un ingénieur), cette capacité à négocier avec un pair disparaît. Comme le notait Arendt, il devient dès lors impossible de faire valoir nos situations spécifiques, nos subjectivités et nos affects en comptant sur l'empathie d'autrui.

En édifiant des bureaucraties toujours plus automatisées, nous risquons donc de solder cette « anthropologie humaniste » au fondement du droit libéral, pour lui substituer une anthropologie guerrière et cybernétique au sein de laquelle, comme le souligne le philosophe des sciences Peter Galison, chacun est considéré comme une « boîte noire », avec « des entrées et des sorties et sans accès à la vie intérieure d'autrui » [START_REF] Galison | The Ontology of the Enemy: Norbert Wiener and the Cybernetic Vision[END_REF]Bruno, Lissovsky & Ferraz Vidal 2018). Ce qui revient, en fin de compte, à accepter de nous considérer les uns les autres comme des machines.

La focale procédurale et le primat donné aux dispositifs socio-techniques dans l'évaluation des « risques » occulte aussi d'autres angles morts causés par la logique d'optimisation bureaucratique. Par exemple, l'une des justifications les plus courantes à l'informatisation des administrations tient à des objectifs comptables et budgétaires : en réalisant un saut qualitatif dans l'automatisation, l'IA permettrait de faire « passer à l'échelle » tel ou tel process bureaucratique en réalisant des économies d'échelle. Ainsi, dans un courrier à la CNIL, la région PACA défendait récemment l'expérimentation de la reconnaissance faciale aux abords des lycées en affirmant que ce projet constituait « une réponse au différentiel croissant constaté entre les exigences de sécurisation des entrées dans les établissements et les moyens humains disponibles dans les lycées, dans le cadre des plans successifs de réduction des effectifs dans la fonction publique » (Région Sud 2018). Intimement liée aux politiques d'austérité, l'automatisation poursuit ainsi le mouvement néo-libéral de sape du service public mais aussi de précarisation et de déqualification d'une partie de la fonction publique, victime d'une atomisation croissante et du démantèlement de ses capacités d'action collective.

Parmi les autres angles morts fréquemment éludés par la focale procédurale, on pourrait encore évoquer le coût écologique engendré par le processus d'automatisation (l'un des arguments opposés par les abonnés Enedis à l'automatisation des relevés de leur consommation électrique via les compteurs connectés), la privatisation de l'expertise et l'affaiblissement des compétences des agents publics, dès lors que les algorithmes sont le plus souvent conçus par des prestataires externes (ce dont ont pu se plaindre des syndicats policiers opposés à des partenariats avec des entreprises spécialisées dans des technologies de surveillance) (SDPM 2018), l'incapacité fréquemment constatée des grands chantiers de dématérialisation à atteindre l'objectif de « simplification » et leurs effets bien réels sur l'aggravation des inégalités [START_REF] Deville | Les chemins du droit : Ethnographie des parcours d'accès au RSA en milieu rural[END_REF][START_REF] Vallipuram | Non, il ne faut pas combattre la fracture numérique[END_REF][START_REF] Charrel | Illectronisme : les laissés-pour-compte du tout-numérique[END_REF][START_REF] Brygo | Peut-on encore vivre sans Internet ?[END_REF], ou encore la légitimité des revendications de celles et ceux qui refusent de répondre aux multiples injonctions technologiques et souhaitent continuer à bénéficier des services publics au travers de guichets physiques, peuplés d'humains en chair et en os (D'Allens & Pitton 2020).

Si l'automatisation bureaucratique aggrave les tendances totalitaires de la domination bureaucratique, et si la multiplication de procédures pour en contenir les effets délétères a fait la preuve de sa trop grande inefficacité, il est peut-être temps d'en tirer les conséquences. Sans forcément renoncer à dépasser l'antagonisme entre bureaucratie et démocratie (Bourgault 2017), il s'agirait alors de nous en tenir à un principe de précaution en joignant nos voix à celles et ceux qui, en différents endroits du monde social, disent haut et fort leur refus d'un « État digital » et du projet technocratique dont il procède.

Références

Dictature de la commodité

La dictature de la commodité renvoie à la propension des gens à se satisfaire de dispositifs techniques perçus comme plus « commodes », pratiques, économiques ou disposant d'interfaces jugées plus user-friendly, quitte à s'accommoder d'atteintes systémiques à leurs droits, d'abus en tous genres de la part des fournisseurs, et plus généralement de fortes externalités négatives. Par extension, cette notion renvoie à l'attrait qu'exercent souvent les solutions à forte composante informatique -et le plus souvent « sans contact » -sur les alternatives traditionnelles : recourir à Amazon pourra paraître plus pratique et rapide que d'aller passer commande auprès de son libraire de quartier ou autre commerce de proximité ; la reconnaissance faciale sera jugée plus sûre, plus commode, voire plus hygiénique que le contrôle d'une carte d'identité ou d'une carte d'adhésion pour accéder à tel lieu ou tel service ; solliciter Google Maps ou même Open Street Map pour s'orienter en ville paraîtra plus « efficace » que d'avoir à emporter une carte avec soi ou à demander son chemin à un passant, etc.

Des théoriciens et défenseurs des logiciels libres comme Philippe Aigrain ou Eben

Moglen ont eu recours à cette expression à partir du début des années 2010 pour expliquer, en lien avec l'effet de réseau, le formidable pouvoir d'attraction des grandes plateformes Web oligopolistiques en comparaison d'alternatives éthiques, fondées sur des logiciels libres et des architectures distribuées garantissant un plus grand contrôle des usagers sur leurs données. Cet attrait n'a pas simplement eu des effets sur le grand public, mais a aussi touché de nombreux groupes militants qui, dans les années 1990, avaient pourtant oeuvré à construire leurs autonomies médiatique et communicationnelle en travaillant main dans la main avec des collectifs hackers. À partir des années 2000, l'émergence du « web 2.0 » et des services « cloud » ont en effet contribué à rompre ces alliances : nombre d'organes militants choisissent alors d'aller « là où sont les gens », c'est-à-dire sur ces plateformes en apparence « gratuites » où les marchands d'attention ont réussi à les agréger. Les militants sont aussi séduits par des interfaces accessibles demandant un faible niveau de compétence technique, et des systèmes qui leur évitent de s'enquérir des capacités de stockage ou de la plupart des enjeux liés à la sécurité informatique -autant d'aspects directement pris en charge par le gestionnaire privé de la plateforme.

Hélas, ces avantages perçus se paient d'une soumission aux modèles toxiques induits par le capitalisme de surveillance, qu'il s'agisse par exemple de l'exploitation des données personnelles ou des politiques de censure exercées par ces plateformes. Les chercheurs Mathias Klang et Nora Madison parlent à cet égard d'une forme de « domestication » de l'engagement politique sur Internet.

La dictature de la commodité renvoie ainsi aux coûts politiques engendrés par des comportements individuels et à la manière dont, en l'absence de moyens d'action collective permettant de les résorber significativement, chacun de nos petits renoncements participe à la construction d'un macro-système technique aux potentialités totalitaires.

Interopérabilité

Dans le contexte des technologies informatiques, l'interopérabilité désigne la capacité de systèmes distincts à s'échanger des données grâce à des protocoles communs. La notion connaît un regain d'intérêt depuis quelques années, puisqu'elle est au coeur du design de nombreux réseaux sociaux décentralisés fondés sur des logiciels libres qui se sont constitués en « fédivers » (un néologisme issu de la contraction des mots « fédération » et « univers »). Ainsi, grâce au protocole appelé ActivityPub, l'ensemble des serveurs hébergeant des instances de tels logiciels -par exemple des applications de micro-blogging comme Mastodon ou Pleroma, conçus comme des alternatives à twitter -deviennent interopérables, permettant ainsi à l'ensemble des utilisateurs de ces services de communiquer les uns avec les autres, et ce quel que soit le serveur qui les héberge (chacun de ces serveurs pouvant avoir des conditions d'utilisation distinctes, par exemple s'agissant des politiques de modération).

L'interopérabilité constitue aussi une manière de « casser » les « effets de réseaux » qui sont au fondement du monopole des grandes plateformes Web, et en particulier des réseaux sociaux comme Facebook, YouTube ou Twitter. Certains acteurs proposent ainsi de créer de nouvelles obligations juridiques imposant à ces grands acteurs de se rendre interopérables avec d'autres services similaires. Ainsi, si une personne utilisant Facebook souhaite résilier son compte -par exemple pour éviter que Facebook n'exploite ses données personnelles, ou pour s'émanciper des politiques de censure mises en oeuvre par l'entreprise -elle pourra « exporter » ses données chez un prestataire alternatif offrant des fonctionnalités équivalentes. La garantie d'une interopérabilité technique permettra ensuite à cette personne de continuer à communiquer avec ses contacts restés sur Facebook, sapant ainsi les effets de réseau qui dissuadent nombre d'entre nous de nous émanciper des grands plateformes toxiques.

Référence

Palfrey, John., & Gasser, Urs., 2012), Interop: The Promise and Perils of Highly Interconnected Systems, Basic Books.

Reféodalisation d'Internet

Dans son « archéologie de l'espace public » publiée en 1962, le philosophe Jürgen Habermas décrivait l'émergence, à partir du XVIII e siècle, de nouvelles pratiques politiques dans différents espaces sociaux -clubs, salons, journaux -dédiées à l'usage public de la raison et à la critique du pouvoir, pratiques qui étaient parties prenantes d'un processus de démocratisation. Cependant, à partir du second XIX e siècle, l'arrivée de la publicité, l'industrialisation, la massification de médias désormais adossés à de grands groupes privés, puis plus tard l'exercice d'un monopole d'État sur les nouveaux moyens de télécommunication allaient conduire à saper les conditions même d'un espace de critique autonome et pluriel. De nouveau soumis aux intérêts privés et au contrôle politique de l'État, l'espace public se trouvait, d'après Habermas, reféodalisé.

Cette analyse peut être transposée à Internet. Alors qu'il était présenté dans les années 1990 comme le vecteur d'un renouveau démocratique de l'espace public médiatique, et comme une technologie propice à la multiplication d'espaces publics alternatifs libérés de la tutelle des médias de masse, Internet aura à son tour connu une forme de reféodalisation, au gré des mutations de son économie politique et des stratégies de pouvoir des États. L'émergence, à partir du début des années 2000, d'un capitalisme de surveillance fondé sur la publicité ciblée, la mise au point d'algorithmes conçus pour maximiser les émotions négatives et le temps passé sur les écrans, de même que les alliances toujours plus poussées entre les États et les grandes plateformes pour surveiller et réguler les communications auront à leur tour marqué un retour en force de logiques propagandistes et manipulatoires, obérant les potentialités critiques et démocratiques d'Internet.

Références

Habermas, Jürgen, 1993, L'espace public : Archéologie de la publicité comme dimension constitutive de la société bourgeoise, Payot.

Tréguer, Félix, 2019, L'utopie déchue : Une contre-histoire d'Internet, XVè-XXIè siècle, Fayard.

Technopolice

Le terme de technopolice a aujourd'hui trois types d'emplois, dont les uns font l'objet d'un affichage officiel, tandis que les autres ont pour visée de dénoncer les dangers et les angles morts des programmes gouvernementaux : 1°Néologisme formé pour désigner les applications policières des dernières innovations technologiques et les formes de pouvoir qu'elles induisent. 2°Nom de la campagne de recherche-action lancée en septembre 2019 par La Quadrature du Net pour documenter les déploiements de nouvelles technologies de surveillance policière dans l'espace public urbain français, le plus souvent justifiés par l'horizon de la « ville intelligente » (smart city). Dans ce contexte, le

  Algan, Yann & Cazenave, Thomas, 2016, L'État en mode start-up, Paris, Eyrolles Ananny, Mike & Crawford, Kate, 2018, « Seeing without Knowing: Limitations of the Transparency Ideal and Its Application to Algorithmic Accountability », New Media & Society, 20(3), p. 973-989 Arcep, 2021, Baromètre du numérique Arendt, Hannah, 2003, Du mensonge à la violence, Paris, Presses Pocket Bertholet, Clément & Létourneau, Laura, 2017, Ubérisons l'État ! Avant que d'autres ne s'en chargent, Malakoff, Armand Colin Bourgault, Sophie, 2017, « Prolegomena to a Caring Bureaucracy », The European Journal of Women's Studies, 24(3), p. 202-17 Bruno, Fernanda, Lissovsky, Maurício & Ferraz Vidal, Icaro, 2018, « Abstraction, expropriation, anticipation : Note généalogique sur les visions machiniques de la gestualité », Réseaux, n°211(5), p. 105-35.