viewgit/inc/functions.php:78 Function create_function() is deprecated [8192]

second version

Author Gabriel Scherer <gabriel dot scherer at inria dot fr>
Author date 2012-01-02 17:06:13
Author local date 2012-01-02 18:06:13 +0100
Committer Gabriel Scherer <gabriel dot scherer at inria dot fr>
Committer date 2012-01-02 17:06:28
Committer local date 2012-01-02 18:06:28 +0100
Commit c1632b8532edb84354555898f05513aa6a069111
Tree ae4391a1c15b329b238eabfb0c97bd3eba45ffd5
Parent 30ff408904207ab7fadea0b1edb0abaac322a6f3
second version
Affected files:
namespaces.text : file, diff
diff --git a/namespaces.text b/namespaces.text
index bc912c0..063055f 100644
--- a/namespaces.text
+++ b/namespaces.text
@@ -20,16 +20,24 @@ The discussed proposals are included, for reference, at the end of the
 document. If only to convince you that my "synthesis" is *not* longer
 than the four proposals concatenated!

-The document is split in three part:
+The document is split in five parts:

-1. A precise (formal?) framework to think about how the current
-  semantics (and eventually the various proposals) relate module
-  references in the OCaml source code to compilation units in the
-  filesystem. I came to this frame by comparing and trying to
-  synthetise the various proposals, and this is the novel aspect the
-  document.
+1. A lexicon, and a description of how the current OCaml implementation
+   resolves module references to compilation units

-2. A description of how, to my understanding, the current propositions
+2. A precise discussion of the linking problem; the linker depends on
+   choice made earlier during compilation (how dependencies are
+   recorded in each compiled file) and put constraints on our ability
+   to disambiguate.
+
+3. A precise (formal?) framework to think about how the current
+   resolution semantics (and eventually the various proposals) relate
+   module references in the OCaml source code to compilation units in
+   the filesystem. I came to this frame by comparing and trying to
+   synthesize the various proposals, and this is the novel aspect the
+   document.
+
+4. A description of how, to my understanding, the current propositions
    fit in this framework. I'm not trying to completely sum up or
    rewrite the proposals, but to describe in an unified manner
    a specific aspect of them (the module reference -> compilation unit
@@ -38,7 +46,7 @@ The document is split in three part:
    and make suggestions), and the framework does not encompass all
    aspects of all the proposals.

-3. Some discussion of how we should evaluate the proposals and which
+5. Some discussion of how we should evaluate the proposals and which
    aspects have not been considered in the unified presentation. While
    parts (1) and (2) aim at absolute objectivity, this one is more
    subjective and is warmly open to further discussion.
@@ -122,10 +130,15 @@ program, either in source or compiled form).
   defined by the various proposals. Roughly, a namespace is an
   identifier (whose syntax is proposal-dependent) that refers to
   a place where compilation units live; the name and the "place" are
-  considered one same thing. Namespaces are 'open': there is no intra-
-  or extra-linguistic way to list *all* the units present in a given
-  nameplace, it is only possible to say that some specific modules
-  (between others) live in a given namespace.
+  considered one same thing.
+
+  There are various intuitions around the 'namespace' concept. For
+  some, namespaces should be considered 'open': there would be no
+  intra-linguistic way to list *all* the units present in a given
+  namespace, it is only possible to say that some specific modules
+  (between others) live in a given namespace. For others, namespaces
+  are just specific modes of use of modules: they are defined once and
+  for all and cannot be extended.

   I will use 'N' as a metavariable to denote namespaces.

@@ -136,11 +149,14 @@ program, either in source or compiled form).
   All proposals add a new way to refer to a module in OCaml code : it
   is possible to prefix a module name by a namespace : N|M.

-  Of all the considered proposals, only Alain's doesn't explicitely
-  use a concept of 'namespace'. I will still use the 'namespace' name
-  to designate a concept of Alain's proposal (in-code references to
+  Of all the considered proposals, only Alain's doesn't explicitly use
+  a concept of 'namespace'. I will still use the 'namespace' name to
+  designate a concept of Alain's proposal (in-code references to
   'namespace maps'), as it is consistent with the other proposals, in
-  particular Nicolas's which is very close to Alain's.
+  particular Nicolas's which is very close to Alain's. In particular,
+  'namespace maps' in Alain's proposal do not have a hierarchical
+  structure; this is a special case where namespaces have at most one
+  component.

   Note that this is just abstract syntax. Concrete syntax choices
   differ between proposals (most of them use '.' instead of ':' and
@@ -184,13 +200,222 @@ module references to compilation units in a way that is more easy to
 control and more resilient to unit name conflicts? The module
 references prefixed by 'namespaces' should behave better.

-Some of the proposals also adress tangential issues such that:
+Some of the proposals also address related issues such as:
+
+- how to preserve that disambiguation information in later stages of
+  the compilation process, in particular linking which obeys different
+  rules. That is a very important aspect -- that I had shamefully
+  neglected in previous versions of this document -- as it's no good
+  to disambiguate the typechecker if the linker is still confused.
+
 - providing dependency information to the toolchain, in particular so
   that `ocamldep` continues to work correctly
+
 - `open`ing name hierarchies and importing opening/renaming/shadowing
   decisions (at the semantic level of OCaml programs)

-## Compilation unit resolution: a unified two-steps presentation
+
+# Part 2: A description of the current linker behavior
+
+Summary: this section discuss the highly relevant issue of linking,
+and is necessary to understand some aspects of the proposals (and the
+flaws of the current state of some others, including previous versions
+of this document). However, my conclusion is that we can solve the
+problem internally without asking the user intervention and
+independently of namespace choices; if my solution works -- which is
+not so certain -- the linking problem becomes irrelevant to the
+namespace discussion, and you can jump to the next section directly.
+
+As described above, when type-checking a module, references to
+external compilation units are resolved. Those external compilation
+units are called "imports" of the current compilation unit. When
+a .cmi or .cmo is saved for the current unit, the name of each import,
+along with a checksum of the import interface (.cmi), is saved in the
+compiled object (.cmi or .cmo). The name of the current module and its
+interface checksum (found by looking for the corresponding .cmi) is
+also saved; that is, "imports" actually contain name and interface
+checksums of all dependencies *and* the current module.
+
+Those names and checksums are used later by the linker: each
+compilation unit is compiled independently into a .cmo, and a set of
+.cmo is later brought together to form a complete executable. The set
+of .cmo to link must be in topological order (each .cmo must come
+after all its dependencies), and this is checked with the list of
+imported modules contained in each .cmo. So currently, the check that
+"this dependency is satisfied" relies on module names.
+
+Besides, the linker also check that checksums are correct (to avoid
+linking together modules compiled against different interfaces of the
+same name): each dependency must correspond to a .cmo that was given
+earlier, so we have it's "official" checksum and can compare the
+checksum stored in the current .cmo for this dependency against it.
+
+That reliance on module names to associate modules to their
+dependencies means that the linker, as well as the typer, needs help
+for disambiguation. It's useless to help the typer to distinguish two
+different .cmi of the same name, if later the linker is unable to
+combine two .cmo of the same name, or even to say which of those
+a given module implementation depends on.
+
+## Details: .cm(x)a, .cmx, -pack
+
+As far as I understand, .cma files (respectively .cmxa), for linking
+purposes, are just sets of .cmo files (resp. .cmx) that are not all
+linked, only those that are actually used by the module. In other
+words, passing a .cma is like passing all the .cmo it contains whose
+name is present as a dependency of one of the other needed modules.
+
+Native compilation behaves a bit differently (from bytecode
+compilation) as it relies on information from external modules
+*implementation* for code generation (simple cross-module
+optimizations, etc.). A .cmx contains not only the name and interface
+(.cmi) checksum of all the modules it depends on, but also the
+checksums of the compiled implementation (.cmx) of those
+dependencies. During linking, those are also checked for consistency.
+
+There is currently no way to change the module name stored in
+a compilation unit. If I understand correctly, the `-pack` option was
+initially designed to do this (rename the packed .cmo/.cmx as part of
+the hierarchy instead of isolated modules), but it turned out that
+changing the internal name of a .cmx was an inherently gore and
+non-portable operation that couldn't be made to work easily on all
+architectures/systems. The `-for-pack` option allows to choose an
+internal name that is not exactly derived from the file name, but it's
+still set in stone at compilation time.
+
+## How current proposals handle the linking problem
+
+The linker puts hard constraints on the disambiguation capacity of the
+whole toolchain. Only Fabrice and Alain have really discussed this
+aspect. I will describe how their proposal addresses the issue, and
+make a new proposal that is quite independent from the rest of the
+namespace handling question -- my point is that it can be made
+internal and never seen by the user.
+
+The "linker issue" needs synchronization between the compiler, which
+decides what "linktime information" to store in compiled .cm{i,o,x}
+files, and the linker, which uses that information to produce the
+executable. This linktime information can be relatively independent
+from what the user sees or how she uses the code and compiled files,
+and he doesn't access it -- except in debugging tools that dissect the
+content of a compiled file. We only need to make sure that:
+
+- the stored information is consistent with the users expectation:
+  when he compiles a compilation unit against a given library, the
+  dependency stored really corresponds to this library, so that the
+  linker links it with the library's implementation and not something
+  else
+
+- there are as few conflicts as possible, eg. two different external
+  dependencies do not get assigned the same linktime information
+
+The two proposals that consider the linking problem suggest very
+different (symmetric?) solutions:
+
+- Fabrice's idea is to use the user-visible namespace, in addition to
+  the file-derived module name, as part of the linktime
+  information. Conflicts are avoided by having a discipline of unique
+  namespaces (eg. containing personal information on the code
+  distributor in the spirit of Java namespaces: inria.stdlib.unix,
+  ocamlpro.tryocaml, rwmjones.libvirt). Operations are provided to
+  "open" or rename namespaces to avoid using those long unique names
+  all the time.
+
+- Alain's idea is to put the uniqueness information in the module
+  name, and to use namespaces to provide palatable short names to
+  designate those painfully long modules. This has the advantage of
+  requiring no change to the way the linktime information is computed
+  and stored, which simplifies implementation, tools handling etc.
+
+In both cases, the burden of avoiding conflicts is on the users. This
+is probably a reasonable burden assuming enough discipline and a bit
+of centralization (GODI, Oasis-DB, etc.) to detect and fix conflicts
+as early as possible.
+
+## Independence from user-visible naming decisions
+
+Both proposals chose to use user-visible information as part of
+linktime information to help uniqueness. It is actually not necessary:
+we can discuss user-facing naming/addressing choices and
+compiler-facing linktime information completely separately.
+
+The point of namespaces (see later sections) is to give OCaml-side
+names to compilation units. Any solution (including the current
+implementation) can be understood as a mapping from "module
+references" to compilation units in the filesystem.
+
+We could consider linktime information as a completely independent
+information. At compilation time, developers (or maybe some automated
+process, see next subsection) decide what linktime information will be
+associated to the compilation unit being produced. They must to their
+best to ensure that this linktime information is unique.
+
+Splitting those two aspects allows to imagine, for example, two
+different addressing hierarchies: one designed to face the user and
+provide a logical organization of modules (in the spirit of Haskell's
+`Data.Array.Persistent` module names), and the other to help linktime
+disambiguation and using hopefully-unique organization names
+(`janestreet.core.persistent_array`).
+
+
+## An attempt at silently fixing the problem
+
+I believe it is actually possible to choose non-conflicting linktime
+information automatically, without involving user intervention. The
+idea is to internally generate a seed that is added to the module name
+(just as Fabrice's namespaces are):
+
+- when creating a .cmi, generate a random seed and add it to the
+  stored compilation unit name
+
+- when compiling a .cmo or .cmx, extract the seed from the relevant
+  .cmi and insert it in the current file
+
+- when resolving an external reference to a compilation unit, add the
+  seed (as well as the name) to the dependency information of the
+  current module; this is naturally done by simply copying the whole
+  "compilation unit name" information
+
+- when linking compilation units, dependencies are matched on both the
+  module name and the seed (again this requires no change, the whole
+  "name" component is manipulated).
+
+This means that two independent .ml compiled against independent .mli
+will always be correctly differentiated, even if they have the same
+name, as the seed differ (... with high probably; if it doesn't work,
+clean and retry!), even if the .mli are exactly the same
+content-wise.
+
+There are a bit more recompilations than previously: the .cmo, and
+depending modules, needs to be recompiled as soon as the .cmi is
+*recompiled*, rather than when the .cmi content *changes*, but this is
+arguably a small difference. If you didn't change the .mli, just don't
+recompile it! We could add an heuristic to not change the seed if
+there already exist a .cmi with the same checksum. The important point
+(and the reason to generate the seed on .cmi creation rather than
+.cmo's) is that for bytecode compilation, implementation changes do
+not force recompilation of dependencies.
+
+A corner case where this doesn't provide perfect disambiguation is the
+following: I have only one .mli, but two .ml that I may want to
+compile against (say `foo.mli` but `foo_windows.ml`, `foo_unix.ml`;
+I copy `foo_windows.ml` to `foo.ml`, compile, move `foo.cmo` to
+`foo_windows.cmo`, and again with `unix`). I believe this is possible
+with the current implementation -- though certainly not advised by the
+manual/specification. It is not currently possible to link both
+foo_windows.cmo and foo_unix.cmo together in an application, but the
+proposed "cmi seed" method also wouldn't do it directly: you would
+have to explicitly recompile the .cmi between each compilation, to get
+different seeds.
+
+
+
+# Part 3: An abstract, unified presentation of compilation unit
+   resolution
+
+In this part, I'm not considering linking matters anymore: only the
+way the compiler resolves external module reference to compilation
+units located at some place in the filesystem.

 The current OCaml compiler interleaves two different aspects:
 - type-checking of the source file currently being processed
@@ -207,7 +432,6 @@ A compilation unit environment is built by the following procedure:
 - iterate on all directories present in the load path
 - for each directory, iterate on all the compiled interface
   compilation units (.cmi) in the directory
-
 - for each such unit U, add the association (ε|mod(U) -> U) to the
   compilation unit environment (ε is the empty namespace).

@@ -246,52 +470,139 @@ build the initial environment:
 - instead of searching a load path, using arbitrary mapping as defined
   in a mapping file passed to the compiler...

-## Semantics of the "opening" namespaces: an `open-namespace` construct

-This two-pass semantics allows a simple explanation of `open`
-semantics for namespaces. The current semantics of `open <expr>`
-cannot be explained as an action on the `module environment`, but on
-the complete typing environment of an OCaml program: it looks for the
+## Formal structure of hierarchical compilation unit environments
+
+In the most general case, compilation units environments are trees
+recursively defined as having two components:
+  - units: a (possibly empty) mapping from module names to compilation units
+  - subenv.: a (possibly empty) mapping (C ↦ T) from namespace components to
+    compilation unit (sub)environments
+The empty environment has has two empty maps.
+
+For example, the following compilation unit environment maps
+foo:bar|Baz to "baz.cmo":
+{
+  Baz -> "/tmp/foo.cmo"
+  foo -> {
+    bar -> { Baz -> "baz.cmo" }
+  }
+  foobar -> { }
+}
+
+This is slightly more refined than a simple mapping from module
+references to compilation units, as we can make a difference between
+namespaces that are defined in the environment, but empty (here
+'foobar'), and namespaces that do not exist in the environment.
+
+A previous version of the document considered all possible namespaces
+to exist and be empty by default, which made certain errors impossible
+(`open-namespace N` would always succeed; in some cases we want an
+error because the namespace N does not exist). It is still possible to
+represent the previous behavior, by considering as "default
+environment" an environment where all possibles namespaces are defined
+as empty.
+
+We can define a `merge` operation that takes the union of two
+environment E₁ and E₂. It returns:
+  - the union of the units mappings
+  - a subenv. mapping defined by, for each component C of E₁ or E₂,
+    the merging of both subenvironments E₁(C) (or the empty
+    environment if undefined) and E₂(C) (or the empty environment if
+    undefined)
+
+## Two semantics for the `open` construct
+
+This two-pass semantics allows simple explanations of `open` semantics
+for namespaces. The current semantics of `open <expr>` cannot be
+explained as an action on the `module environment`, but on the
+complete typing environment of an OCaml program: it looks for the
 module (OCaml semantic object; not necessarily associated to
 a compilation unit, eg. possibly a submodule of a compilation unit, or
 result from a functor application, etc.) denoted by the expression
 <expr>, and adds all its declarations to the environment.

-We define a new `open-namespace N` construct, reflecting constructions
-used in the proposals (again, this is not a choice of concrete syntax;
-all propositions but Alain's only use `open`). `open-namespace N₁` is
-defined by its action on the compilation unit environment: for each
-binding of the form (N₁:N₂|M -> U) in the environment, (N₂|M -> U) is
-also added to the environment.
+We can define a new `open-namespace N` construct, reflecting
+constructions used in the proposals (again, this is not a choice of
+concrete syntax; all propositions but Alain's only use
+`open`). `open-namespace N₁` is defined by its action on the
+compilation unit environment. Informally, for each binding of the form
+(N₁:N₂|M -> U) in the environment, (N₂|M -> U) is also added to the
+environment.
+
+More precisely, there are two possible choices of semantics
+
+- a "merging" open, that follows the intuition that namespaces are
+  "open" (sic): `open-namespace N₁` finds the subenvironment E₁ at N₁
+  in the current environment E (or fails if it doesn't exist), adds
+  its units to the units of E, and merge each subenvironment (C:E₂) of E₁ to
+  the current subenvironment E.C.
+
+- a "shadowing" open, that respect the semantics of "closed"
+  namespaces that cannot be extended after definition: `open-namespace
+  N₁` finds the subenvironment E₁ at N₁ in the current environment
+  E (or fails if it doesn't exist), adds its units to the units of E,
+  and use each subenvironment (C:E₂) of E₁ to *replace* the current
+  subenvironment E.C.
+
+(On units, different behavior are possible in case of conflict: error
+if the mappings differ, or silent shadowing.)
+
+My previous synthesis only described the "merging open". Fabrice
+noticed that this failed to account for his proposal, that uses
+a "shadowing open", which is consistent with the behavior of OCaml
+modules.
+
+
+## Other operations on environment
+
+The tree-mapping structure of compilation unit environments is quite
+flexible, and a lot of operations can be defined in this framework.
+
+It is easy for example to adapt the `open-namespace N₁` definition
+into a more general `alias-namespace N₁ to N₂` (which adds the
+subenvironment located at N₁, but prefixed with N₂), in two "merging"
+and "shadowing" variants. This "prefixing" operation also describes
+the "include" operation of Nicolas's proposal.

-Remark: with the described semantics, `open-namespace N` never fails:
-it filters environment bindings to process those prefixed by N, and do
-nothing if this set is empty. It could be sensible to add a warning,
-but raising an error would break the "namespace are open" intended
-semantics.
+There is a large design space of reasonable operations on compilation
+unit environments (projection, prefixing, deep merging, intersection,
+removal...). We have found that they are interestingly close (in
+particular the deep merging operation) to "mixin operations" as
+defined in the article "Mixin' Up the ML Module System", by Derek
+Dreyer and Andreas Rossberg, 2008/2011; this is not so surprising, as
+mixins are supposed to be "open" modules, and are therefore a good fit
+for (unrestricted) namespaces.


-# Part 2: How does the current proposals relate module references to
+
+# Part 4: How does the current proposals relate module references to
    compilation units?

 In Alain's and Nicolas's proposal, new mappings are added by files
 mapping OCaml identifiers or path to compilation units (given by
 a filesystem path). Those mapping files:
 - may be found in the search path (Alain's proposal)
-- may be passed explicitely to the tool (Nicolas's proposal)
+- may be passed explicitly to the tool (Nicolas's proposal)

 In Alain's proposal, the 'namespace' N associated to all those mapping
 files is derived from the filesystem path of the mapping file. Each
 line of the mapping files associates a module name M to a compilation
 unit U, but the compilation unit environment is really enriched with
-the binding (N|M -> U). For example, neglecting concrete syntax
-difference, the file `ex.ns` containing `Foo: /tmp/a.cmi; Bar:
-/tmp/b.cmi` would enrich the environment with (ex|Foo -> "/tmp/a.cmi",
-ex|Bar -> "/tmp/b.cmi").
-
-In Nicolas's proposal, the (compiled) mapping files is already
-a sequence of bindings (R -> U), which are added as is, without any
-influence from the mapping file's filename.
+the binding (N|M -> U) : the mapping file defines the subenvironment
+N. For example, neglecting concrete syntax difference, the file
+`ex.ns` containing `Foo: /tmp/a.cmi; Bar: /tmp/b.cmi` would enrich the
+current environment with the mapping
+  ex -> {
+    Foo -> "/tmp/a.cmi"
+    Bar -> "/tmp/b.cmi"
+  }
+.
+
+In Nicolas's proposal, the mapping files already have the structure of
+a compilation unit environment (including nested subenvironments),
+which is merged as is, without any influence from the mapping file's
+filename.

 In Fabrice's and Martin's proposals, the environment-building
 pass does not act the same on all directories of the search path,
@@ -299,52 +610,58 @@ depending on whether the directory contains a distinguished
 configuration file (Package, ocaml.ns). If not, the current semantics
 is used (all .cmi are added to the environment). Otherwise:

-- in Martin's proposal, the Package file explicitely lists the
+- in Martin's proposal, the Package file explicitly lists the
   compilation unit U¹, U²... Uⁿ exported (I suppose the directory
   isn't searched for other compilation units), with an optional
-  namespace N (default value ε). The mappings (N|mod(U¹) -> U¹),
-  (N|mod(U²) -> U²)... (N|mod(Uⁿ) -> Uⁿ) are added to the
-  environment.
+  namespace N (default value ε). The mappings { mod(U¹) -> U¹,
+  mod(U²) -> U² ... mod(Uⁿ) -> Uⁿ } are added to the subenvironment N.

 - in Fabrice's proposal, the ocaml.ns file only specifies the
-  directory-common namespace N. It is searched for compilation units:
-  for each compiled interface compilation unit U in the directory,
-  (N|mod(U) -> U) is added to the environment.
+  directory-common namespace N. The directory is searched for
+  compilation units: the mappings (mod(U) -> U), for each compiled
+  interface compilation unit U in the directory, define a new
+  subenvironment N.

 In another variant of Fabrice's proposal, there is no configuration
 file, but each compilation unit U may optionally specify a namespace
-N. In this case the repository is scanned as usual, and (N|mod(U) ->
-U) is added to the environment.. Should the usual (ε|mod(U) -> U)
-binding also be added? This is a flexibility point of the proposal;
-Fabrice suggests to also bind it only in the case where the currently
-processed unit does not mention namespaces ("compatibility mode").
+N. In this case the repository is scanned as usual, and
+(N|mod(U) -> U) is added to the environment.. Should the usual
+(ε|mod(U) -> U) binding also be added? This is a flexibility point of
+the proposal; Fabrice suggests to also bind it only in the case where
+the currently processed unit does not mention namespaces
+("compatibility mode").

 Once the compilation unit environment is built, typechecking proceeds
 as usual in all proposals.

 When a proposal defined an `open` construct, I believe it always
 coincided with the behavior of the `open-namespace` construct defined
-in part 1. Note that some proposals use the same syntax for modules
-and namespaces: when encountering the concrete code `open Foo`, it is
-unclear if Foo is a module or a namespace, and the semantics differ;
-ambiguity resolution rules are needed. In Alain's proposal, there is
-a distinct `open namespace Foo` syntax which resolves the ambiguity.
+in part 1, in either the "merging" or the "shadowing" variant. Note
+that some proposals use the same syntax for modules and namespaces:
+when encountering the concrete code `open Foo`, it is unclear if Foo
+is a module or a namespace, and the semantics differ; ambiguity
+resolution rules are needed. In Alain's proposal, there is a distinct
+`open namespace Foo` syntax which resolves the ambiguity.

-A namespace-aliasing construct could be treated as a compilation unit
-environment transformer, just as we handle `open-namespace
-N`. `alias-namespace N₁ to N₂` would add, for all bindings of the form
-(N₁:N -> U), a new binding (N₂:N -> U). `open-namespace N` is then the
-special case `alias-namespace N to ε`.
+Remark: it is tempting to try to define the semantics of module
+renamings as action on the compilation unit environment (from ε|M₁ to
+ε|M₂), but I think they rather belong, as `open` on modules, to the
+typing environment. In particular, you may want to alias a module
+*path* to a module name, to address submodules directly. This would
+require maintaining separate 'path substitutions', as done in a recent
+article by Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo
+Park, for entirely different purposes.


-# Part 3: How should we evaluate and compare the different proposals?
+# Part 5: How should we evaluate and compare the different proposals?

 ## What they compare against: uniquifying file names

 Alain made an extremely simple proposition that doesn't request much
 change from the current behavior. He only suggested that library
 writers adopt the convention to use only 'unique' file names, to avoid
-any conflict issue.
+any conflict issue -- in the type_checker, as well as in the linker
+stage.

 To avoid having to use painfully long module names in an OCaml
 program, Alain suggested to introduce a module name aliasing syntax;
@@ -358,16 +675,6 @@ seems to be that it is too impractical. However, it is good to keep it
 in mind when evaluating other proposals, as a 'placebo proposal' to
 compare against.

-Remark: it is tempting to try to define the semantics of module
-renamings as action on the compilation unit enviroment (from ε|M₁ to
-ε|M₂), but I think they rather belong, as `open` on modules, to the
-typing environment. In particular, you may want to alias a module
-*path* to a module name, to adress submodules directly. This would
-require maintaining separate 'path substitutions', as done in a recent
-article by Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo
-Park, for entirely different purposes.
-
-
 ## Subjective comparison: User-side resolution of conflicts

 Disclaimer: while the previous sections were purely an objective
@@ -385,11 +692,12 @@ of two libraries are able to resolve a naming conflict.
 Note that this is not a *necessary* feature for a namespace
 proposal. In particular, the 'placebo' proposal (just use long,
 hopefully-unique names) doesn't have any way to deal with this: if
-your names were not long and unique enough, well, it's your fault;
-just ask the code producers to rename them (or recompile them locally
-under a different filename, which makes you a code producer). It's
-less of a problem if names are, by convention, long and hopefully
-unique than it is currently, with short common names.
+your names were not long and unique enough, well, you lose; you have
+to ask the code producers to rename them (or recompile them locally
+under a different filename, if you have the source code, which makes
+you a code producer). It's less of a problem if names are, by
+convention, long and hopefully unique than it is currently, with short
+common names.

 Fabrice's proposal does not handle conflicts: once your compiled unit
 has a namespace recorded, you cannot change it from the code user
@@ -430,6 +738,14 @@ awkward as the proposal was clearly not optimized for this use case
 implicit directory/unit relation). Still, it can be done purely from
 the user side.

+Remark: it is useless to try to handle such conflicts if they are also
+present at the linker stage -- remember, we can't change the internal
+name of a .cmx. In Fabrice's proposal for example, even if we found
+a way to distinguish two modules of the same name in the same
+namespace, the internal name would be the same and it would be
+impossible to link them both at the same time. I believe that the
+internal seeding solution allows to dissociate linking from module
+discovery, and can be applied in addition to each proposal.

 ## Aspects not discussed
ViewGit