[docs/backpack] Get lint to stop complaining
[ghc.git] / docs / backpack / backpack-impl.tex
index 9be6465..46e397f 100644 (file)
@@ -108,6 +108,29 @@ file representing the module (so that later invocations of GHC can load the type
 of a module), and then after compilation projects object files and linked archives
 for programs to use.
 
+\paragraph{Original names} Original names are an important design pattern
+in GHC\@.
+Sometimes, a name can be exposed in an hi file even if its module
+wasn't exposed. Here is an example (compiled in package R):
+
+\begin{verbatim}
+module X where
+    import Internal (f)
+    g = f
+
+module Internal where
+    import Internal.Total (f)
+\end{verbatim}
+
+Then in X.hi:
+
+\begin{verbatim}
+g = <R.id, Internal.Total, f> (this is the original name)
+\end{verbatim}
+
+(The reason we refer to the package as R.id is because it's the
+full package ID, and not just R).
+
 \subsection{hs-boot}
 
 \verb|hs-boot| is a special mechanism used to support recursive linking
@@ -161,27 +184,16 @@ packaging system, some of which are subsets of the Backpack system.
         separate entries in the package database anyway.}
 
     \item Support typechecking a library against a module interface
-        as opposed to an actual implementation.  This would be useful
-        for moving towards a model where Cabal package dependency versions
-        are replaced with proper signature packages. %  See Section~\ref{sec:signature-packages} for more details.
+        as opposed to an actual implementation.  This includes not
+        only support proper, but also toolchain support for generating
+        and keeping interface files up-to-date, and taking advantage
+        of this discipline to augment Cabal package dependency resolution
+        with proper signature packages. %  See Section~\ref{sec:signature-packages} for more details.
 
     \item Support compiling the aforementioned libraries with actual implementations.
         It is \emph{not} a goal to be able to compile a library while only
         partially providing dependencies, and it is low priority to support
         mutually recursive implementations of these implementations.
-
-        \iffalse%
-    \item Support insertion of backwards compatibility shims for packages
-        that are using old versions of packages, so that you can continue
-        using them without having to patch them manually.  This is a
-        stylized use-case of Backpack features.  See Section~LINKME for
-        more details.
-
-    \item Some easy-to-implement subset of the functionality provided by
-        packages with holes (Backpack proper).  This includes support
-        of linking an executable containing multiple packages with the
-        same package name but different PackageIds.
-        \fi
 \end{itemize}
 
 A lower priority goal is to actually allow multiple instances of
@@ -263,11 +275,11 @@ Backpack proper can be implemented.  These additions are described in
 red in the architectural diagrams.  The current structure of this
 section is to describe the additions bottom up.
 
-\subsection{Concrete physical identity = PackageId$^*$ + Module name}\label{sec:ipi}
+\subsection{Concrete physical identity = PackageId + Module name + Module dependencies}\label{sec:ipi}
 
 \begin{figure}
     \center{\begin{tabular}{r l}
-        PackageId & hash of ``package name, package version, PackageIds of dependent packages'' \\
+            PackageId & hash of ``package name, package version, dependency resolution, \emph{module} environment'' \\
         InstalledPackageId & hash of ``PackageId, source code, way, compiler flags'' \\
     \end{tabular}}
 \label{fig:proposed-pkgid}\caption{Proposed new structure of package identifiers.}
@@ -276,23 +288,34 @@ section is to describe the additions bottom up.
 In Backpack, there needs to be some mechanism for assigning
 \emph{physical module identities} to modules, which are essential for
 typechecking Backpack packages, since they let us tell if two types are
-equal or not. In the paper, the physical identity was represented as the
-package that constructed it as well as some representation of the module
-source.  We can simplify this slightly: in current Cabal packages, we
-require that modules always be given a package-unique logical name;
-thus, physical identities can be simply represented as a PackageId plus
-module name. (See \ghcfile{compiler/basicTypes/Module.lhs:Module})
-In fact, this coincides with how GHC already internally handles
-the problem of type equality: it appeals to an \emph{original name}
-which is, presently, a PackageId and the module name.
-
-However, with the current representation of PackageIds, this is
-insufficient: a package is not just its name, but also the regular
-tree representing all of its package dependencies.  Thus, we have
-to adjust the representation of a PackageId so that it includes this
-regular tree, as seen Figure~\ref{fig:proposed-pkgid}.  Since this
-tree in general may be quite long, it needs to be shortened in some way,
-such as by hashing.
+equal or not.
+
+In GHC, our method of testing whether or not two types are equal is by
+comparing their original names, which is a tuple of a PackageId and the
+module name (summarized in Figure~\ref{fig:current-pkgid}).  If it looks
+like a duck and quacks like a duck, it is a duck: we might reasonable
+imagine that \emph{concrete physical identity = PackageId and module
+name}.  But is this sufficient to represent Backpack's physical module
+identities?
+
+If we look at how physical module identities are allocated in Paper Backpack,
+we can see that each module corresponds to an identity constructor (in
+Backpack this is the package name, some representation of the module
+source, and a disambiguating integer if module source is duplicated)
+\emph{as well as} physical module identities which were applied to
+this constructor.  The current PackageId + Module name scheme adequately encodes
+the constructor (in particular, a single package can't have multiple modules
+with the same name), but it does not encode the \emph{module} dependencies.
+We have to add these to our original names.  There are three ways we can do
+this:
+
+\begin{enumerate}
+    \item Augment original names to have a third component.  This is less than ideal because it requires pervasive changes to all parts of the compiler.
+    \item Augment the module name to record module dependency information.  This is a bit of an odd place to put the information, because our module names correspond quite concretely to the actual source file a user wrote some source in.
+    \item Augment the PackageId to record module dependency information.  For now, this is the regime we will use; however, see Section~\ref{sec:flatten} for why the issue is more subtle.
+\end{enumerate}
+
+(XXX Figure~\ref{fig:proposed-pkgid} is out of date now.)
 
 And now, the complications\ldots
 
@@ -302,8 +325,8 @@ package name (but different PackageIds).  This restriction needs to be
 lifted.  For backwards compatibility reasons, it's probably better to
 not overload \verb|-package-id| but add a new flag, maybe \verb|-force-package-id|;
 we also need to disable the old version masking behavior.  This is orthogonal
-to the IHG work, which wants to allow multiple InstalledPackageIds in the
-\emph{database} (here, we want to allow multiple PackageIds in compiled code).
+to the IHG work, which wants to allow multiple \emph{InstalledPackageIds} in the
+\emph{database} (here, we want to allow multiple \emph{PackageIds} in \emph{compiled code}).
 
 \paragraph{Linker symbols} As we increase the amount of information in
 PackageId, it's important to be careful about the length of these IDs,
@@ -326,12 +349,175 @@ suggested approach is to have a fixed table from these wired names to
 package IDs; alternately we can use something like the special \verb|inplace|
 version number.
 
+\paragraph{Version numbers}  The interaction of Backpack's package polymorphism
+(the ability to mixin different implementations to holes) and Cabal's dependency
+resolution mechanism (which permits a name libfoo to be resolved to a specific
+version libfoo-0.1) can be subtle: there are in fact \emph{two} levels of
+indirection going on here.
+
+The simplest way to think about the distinction is as follows.  When I write
+a Backpack package which does \verb|include foobar|, I have not actually
+written a Paper Backpack package.  Instead, I have written a \emph{pre-package},
+which Cabal's dependency solver then takes and rewrites all package references
+into versioned references \verb|include foobar-0.1|, which now corresponds to
+a Paper Backpack package.  For example, this is a pre-package:
+
+\begin{verbatim}
+package foo where
+    include bar
+\end{verbatim}
+
+and this is a Paper Backpack package:
+
+\begin{verbatim}
+package foo-0.3(bar-0.1) where
+    include bar-0.1(baz-0.2)
+\end{verbatim}
+
+Notably, we must \emph{rename} the package to include information about
+how we resolved all of the inner package references, and if these inner
+package references had dependencies, those must be included too!  In
+effect, the \emph{dependency resolution} must be encoded into the package ID,
+along with the existing Backpack \emph{physical identity regular tree}.
+Phew!
+
 \paragraph{Free variables (or, what is a non-concrete physical
 identity?)} Physical identities in their full generality are permitted
 to have free variables, which represent holes.  Handling this is a
-tricky question, and we defer it to Section~\ref{sec:variables}, when
+tricky question, and we defer it to Section~\ref{sec:typechecking-indefinite}, when
 we talk about packages with holes.
 
+\subsection{Flatten the package database}\label{sec:flatten}
+
+In the previous section, I implied that the \emph{module} dependencies
+could be recorded with the \emph{package} ID\@.  Type error? Yes!
+
+In the old world order, we think of dependencies as being associated with
+packages as a whole.  However, Paper Backpack specifies dependency tracking
+at the \emph{module} level, which means that different compilations of
+an indefinite package may result in modules which should be identified.
+Here is a Backpack package which demonstrates the issue:
+
+\begin{verbatim}
+package a where
+    P :: ...
+    Q :: [ x :: Int ]
+    A = [ import P; ... ]
+    B = [ import Q; ... ]
+package p where
+    P = [ ... ]
+package x where
+    include p
+    Q = [ x = 0 ]
+    include a
+package y where
+    include p
+    Q = [ x = 1 ]
+    include a
+\end{verbatim}
+
+Here, we have a package \verb|a| which probably should have been defined as
+two separate packages (since \verb|A| only relies on \verb|P| and \verb|B|
+only relies on \verb|Q|), but the functionality has been glommed together.
+Then, the downstream packages \verb|x| and \verb|y| fill in the holes using the
+same implementation of \verb|P|, but differing implementations of \verb|Q|.
+(For more explanation about how we would go about compiling this set of
+packages, please see Section~\ref{sec:compiling-definite}.)
+
+Is module \verb|A| from package \verb|x| the same as module \verb|A|
+from package \verb|y|?  In Paper Backpack, the answer is yes.
+However, presently, the installed package database acts as a cache at the \emph{package}
+level; code is only shared if it comes from the same package.  Can we share
+packages \verb|x| and \verb|y|? No!
+\verb|x:B| is \emph{not} the same module as \verb|y:B| (they are using differing
+versions of \verb|Q|).  The upshot is that we are in an awkward position,
+where package \verb|a| contains some modules which must be distinct, and other
+modules which must be unified over several installs.
+
+The theory, thus, demands that we flatten the package database, so that
+we no longer insist that all compiled code that is produced when a
+package is installed live together in a single directory: instead,
+\emph{the installed package database is a directory of physical module
+identities to objects/interfaces}.  Installed packages are represented
+as (possibly overlapping) sets over this store of modules.
+
+\paragraph{Do we really care about this use case?}  Scott gave me one
+good argument why this is a nice feature to have: it permits users to
+modularize third-party packages which were not packaged with modularity
+in mind, but happen to be modular.  For example, when libraries ship
+with test-cases, they currently have to split these test-cases to separate
+packages, so as to not introduce spurious dependencies with various
+test frameworks, which the user may not have or care about.  If dependencies
+are done on a per-module basis, as long as the user doesn't import a test
+module, they never gain the extra dependency.  Another situation is when
+a library also happens to have a helper utility module which doesn't have
+any of the dependencies of the primary library.
+
+One could argue that people already understand it is good practice to
+separate such cases into separate packages, and there is no pressing
+need to allow for sloppy habits.  The counterargument, however, is that
+you are often not in control of these third-party libraries, and the
+more control in the end-user's hands, the better.
+
+\paragraph{Operating system linking}  When the package database is flattened
+into a collection of modules, it becomes less clear how to generate library
+files corresponding to a package.  One possibility is to simply take the
+set of files corresponding to a package and wrap it up into a library.
+If an end-user links against two libraries which include the same object file,
+the linker needs to suppress the symbols associated with one of the instances
+of the object file (it's identical, right?)\footnote{It may not actually be
+possible to do this in the static linking case: one must refer to the actual object
+files}.
+
+If your modules are truly applicative, this might even work OK\@.  However, you will
+be a sad panda if there is any unsafe, mutable global state in the shared
+object (since the object files will each get separate data segments for this
+global state): a generative semantics.\footnote{Even if we did get this right,
+which would be possible when statically linking these modules together, the
+interaction could still be surprising: Backpack can remodularize modules, but
+it can't remodularize values inside a module, so if a module has a dependency
+but some global state in the module doesn't, the resulting behavior can be
+surprising.  Perhaps the moral of the story really is, ``Don't do side effects
+in an applicative module system! No really!''} \\
+
+\subsection{Alternatives to flattening package DB}
+Flattening can be seen as one of four different representations of packages
+at the OS/library level. While it promotes maximal sharing of identical
+modules, it is perhaps too fine-grained for most purposes.
+\emph{ToDo: Describe the alternatives.}
+
+\paragraph{Package slicing} Instead of changing the package database,
+we automatically
+slice a single package into multiple packages, so that the sliced
+packages have dependencies which accurately reflect their constitutent
+modules.  For a well modularized package, the slicing operation should
+be a no-op.  This would also be useful in some other situations (see the
+\verb|-module-env| discussion in Section~\ref{sec:compiling-definite}).
+In fact, which slice a module should be placed in can be automatically
+calculated by taking the package name with the regular tree
+associated with the module (Section~\ref{sec:ipi}).
+
+A minor downside of package slicing is in a dynamically linked environment,
+we pay a performance cost when we have to jump from one dynamic library
+to another, and slicing could introduce are large number of separate
+dynamic libraries which need to be switched between each other.
+
+Edward likes this proposal.
+
+\paragraph{Changing Backpack to disallow fine-grained dependencies}
+
+Another perspective is that we fell into a trap when we decided that
+dependencies should be calculated per-module.  What if, instead, we
+expanded the dependency of each module to cover \emph{all signatures}
+in the package?  Then the dependency tree would always be the same and
+the package would be shared only if all holes were precisely the same.
+Our motivating example, then, would fail to witness sharing.
+
+This might be the simplest thing to do, but it is a change in the
+Backpack semantics, and rules out modularization without splitting a package
+into multiple packages.  Maybe Scott can give other reasons why this
+would not be so good.  SPJ is quite keen on this plan.
+
 \subsection{Exposed modules should allow external modules}\label{sec:reexport}
 
 In Backpack, the definition of a package consists of a logical context,
@@ -352,7 +538,40 @@ For example, an traditional module export is simply (Name, my-pkg-id, Name);
 a renamed module is (NewName, my-pkg-id, OldName), and an external module
 is (Name, external-pkg-id, Name).
 
-\section{Simplifying Backpack}\label{sec:simplifying-backpack}
+As an example:
+
+\begin{verbatim}
+package P where
+    M = ...
+    N = ...
+package Q (M, R, T)
+    include P (N -> R)
+    T = ...
+\end{verbatim}
+
+And now if we look at Q\@:
+
+\begin{verbatim}
+exposed-modules:
+        <M, P.id, M>
+        <R, P.id, N>
+        <T, Q.id, T>
+\end{verbatim}
+
+When we compile Q, and the interface file gets generated, we have
+to generate identifiers for each of the exposed modules.  These should
+be calculated to directly refer to the ``original name'' of each them;
+so for example M and R point directly to package P, but they also
+include the original name they had in the original definition.
+
+\paragraph{Error messages}  When it is possible for multiple physical
+entities to have the same ``user-friendly'' name, this can result in a
+very confusing situation if both entities have to be referred to in the
+same message.  This is especially true when renaming is in place:
+you not only want to print out the name in scope, but probably some indication
+of what the original name is.  In short, when it comes to error messages, tread with care!
+
+\section{Shapeless Backpack}\label{sec:simplifying-backpack}
 
 Backpack as currently defined always requires a \emph{shaping} pass,
 which calculates the shapes of all modules defined in a package.
@@ -362,36 +581,52 @@ implementation problems:
 
 \begin{itemize}
 
-    \item A shaping pass means that it's not possible to compile modules
-        in a package one-by-one, even if there is \emph{no mutual
-        recursion} at all in the package.  Without mutual recursion, the
-        shaping pass should not be necessary.  (Maybe this is not true!)
-        Always enforcing two-passes means Backpack is not a ``pay as you
-        go'' language feature.
-
-    \item The calculated module shapes are quite intricate: in particular,
-        they contain information about the providences of all data types
-        and identifiers defined by a module.  To run a shape analysis, we
-        must preprocess and parse all modules\ldots and then parse them
-        again later, in the second, type-checking pass; furthermore, all
-        of this information must be passed to GHC later.
-
-    \item The conclusions of the shaping pass are \emph{incompatible} with
-        what types of mutual recursion GHC can actually compile today
-        via hs-boot: primarily, GHC requires that any data type or function
-        defined in an hs-boot file also be \emph{defined} in its corresponding
-        hs file. (In this way, we can assign an original name to it immediately,
-        which simplifies compilation immensely.)
-
-    \item The mode of program organization Backpack encourages, mutually
-        recursive modules, is less efficient than code without recursive
-        dependencies: thus programmers have good motivation to avoid
-        this design pattern when possible.
+    \item \emph{Shaping is a lot of work.} A module shape specifies the
+        providence of all data types and identifiers defined by a
+        module. To calculate this, we must preprocess and parse all
+        modules, even before we do the type-checking pass.  (Fortunately,
+        shaping doesn't require a full parse of a module, only enough
+        to get identifiers, which makes it a slightly more expensive
+        version of \verb|ghc -M|.)
+
+    \item \emph{Shaping must be done upfront.} In the current Backpack
+        design, all shapes must be computed before any typechecking can
+        occur.  While performing the shaping pass upfront is necessary
+        in order to solve the double vision problem (where a module
+        identity may be influenced by later definitions), it means
+        that GHC must first do a shaping pass, and then revisit every module and
+        compile them proper.  Nor is it (easily) possible to skip the
+        shaping pass when it is unnecessary, as one might expect to be
+        the case in the absence of mutual recursion.  Shaping is not
+        a ``pay as you go'' language feature.
+
+    \item \emph{GHC can't compile all programs shaping accepts.}  Shaping
+        accepts programs that GHC, with its current hs-boot mechanism, cannot
+        compile.  In particular, GHC requires that any data type or function
+        in a signature actually be \emph{defined} in the module corresponding
+        to that file (i.e., an original name can be assigned to these entities
+        immediately.)  Shaping permits unrestricted exports to implement
+        modules; this shows up in the formalism as $\beta$ module variables.
+
+    \item \emph{Shaping encourages inefficient program organization.}
+        Shaping is designed to enable mutually recursive modules, but as
+        currently implemented, mutual recursion is less efficient than
+        code without recursive dependencies. Programmers should avoid
+        this code organization, except when it is absolutely necessary.
+
+    \item \emph{GHC is architecturally ill-suited for directly
+        implementing shaping.}  Shaping implies that GHC's internal
+        concept of an ``original name'' be extended to accommodate
+        module variables.  This is an extremely invasive change to all
+        aspects of GHC, since the original names assumption is baked
+        quite deeply into the compiler.  Plausible implementations of
+        shaping requires all these variables to be skolemized outside
+        of GHC\@.
 
 \end{itemize}
 
-The shaping pass is fundamentally necessary for some types of Backpack packages.
-Here is the example which convinced Simon:
+To be clear, the shaping pass is fundamentally necessary for some
+Backpack packages.  Here is the example which convinced Simon:
 
 \begin{verbatim}
 package p where
@@ -400,18 +635,20 @@ package p where
     A = [export T(MkT), f, h; import B; f MkT = MkT]
 \end{verbatim}
 
-The key is to observe that B \emph{may or may not typecheck} depending
+The key to this example is that B \emph{may or may not typecheck} depending
 on the definition of A. Because A reexports B's definition T, B will
 typecheck; but if A defined T on its own, B would not typecheck.  Thus,
 we \emph{cannot} typecheck B until we have done some analysis of A (the
 shaping analysis!)
 
-All of these restrictions point to the desirability of a subset of
-Backpack which does not allow mutually recursive modules, and
-consequently does not require a shaping pass.
+Thus, it is beneficial (from an optimization point of view) to
+consider a subset of Backpack for which shaping is not necessary.
+Here is a programming discipline which does just that, which we will call the \textbf{linking restriction}: \emph{Module implementations must be declared before
+signatures.}  Formally, this restriction modifies the rule for merging
+polarized module shapes ($\widetilde{\tau}_1^{m_1} \oplus \widetilde{\tau}_2^{m_2}$) so that
+$\widetilde{\tau}_1^- \oplus \widetilde{\tau}_2^+$ is always undefined.\footnote{This seemed to be the crispest way of defining the restriction, although this means an error happens a bit later than I'd like it to: I'd prefer if we errored while merging logical contexts, but we don't know what is a hole at that point.}
 
-Here is the programming discipline, called the \textbf{linking restriction}: \emph{Module implementations
-must be declared before signatures.}  Alternately, $+ \oplus - \neq - \oplus +$.  Here's an example:
+Here is an example of the linking restriction. Consider these two packages:
 
 \begin{verbatim}
 package random where
@@ -422,6 +659,10 @@ package monte-carlo where
     System.MonteCarlo = [ ... ].hs
 \end{verbatim}
 
+Here, random is a definite package which may have been compiled ahead
+of time; monte-carlo is an indefinite package with a dependency
+on any package which provides \verb|System.Random|.
+
 Now, to link these two applications together, only one ordering
 is permissible:
 
@@ -431,7 +672,7 @@ package myapp where
     include monte-carlo
 \end{verbatim}
 
-or even (if myapp wants to provide its own random library):
+If myapp wants to provide its own random implementation, it can do so:
 
 \begin{verbatim}
 package myapp2 where
@@ -439,15 +680,16 @@ package myapp2 where
     include monte-carlo
 \end{verbatim}
 
-That is, all of \verb|monte-carlo|'s holes have been filled in by the time
-it is included.  The alternate ordering is not allowed, as it could have
-resulted in a recursive 
+In both cases, all of \verb|monte-carlo|'s holes have been filled in by the time
+it is included.  The alternate ordering is not allowed.
 
 Why does this discipline prevent mutually recursive modules?  Intuitively,
-the signature is the mechanism by which we can get a handle on an implementation
-before it is defined, thus allowing circularity. If there is never an earlier handle
-to an implementation, circularity is not possible.  A simple example of
-this violation is in the reordered version of \verb|myapp2|:
+a hole is the mechanism by which we can refer to an implementation
+before it is defined; otherwise, we can only refer to definitions which
+preceed our definition. If there are never any holes \emph{which get filled},
+implementation links can only go backwards, ruling out circularity.
+
+It's easy to see how mutual recursion can occur if we break this discipline:
 
 \begin{verbatim}
 package myapp2 where
@@ -455,113 +697,176 @@ package myapp2 where
     System.Random = [ import System.MonteCarlo ].hs
 \end{verbatim}
 
-(Nota bene: this restriction applies to aliasing to, which can induce
-linking as well).
+\subsection{Typechecking of definite modules without shaping}
 
-\subsection{Why isn't shaping necessary?}
+If we are not carrying out a shaping pass, we need to be able to calculate
+$\widetilde{\Xi}_{\mathsf{pkg}}$ on the fly.  In the case that we are
+compiling a package---there will be no holes in the final package---we
+can show that shaping is unnecessary quite easily, since with the
+linking restriction, everything is definite from the get-go.
 
-(ToDo: have this formally setup and everything)
+Observe the following invariant: at any given step of the module
+bindings, the physical context $\widetilde{\Phi}$ contains no
+holes.  We can thus conclude that there are no module variables in any
+type shapes.  As the only time a previously calculated package shape can
+change is due to unification, the incrementally computed shape is in
+fact the true one.
 
-In the case that we are compiling a definite package (there will be no leftover
-holes), the argument is quite simple.  In vanilla Backpack, when a
-signature is defined, we have to generate a pile of module variables
-which may get unified with physical module identities.  However, with
-the linking restriction, we only ever link a signature with a
-\emph{fully instantiated} module definition. Thus, all module variables
-can be immediately eliminated, and all we need to do is maintain an
-updating logical context (i.e., module environment) so that later
-modules know how to resolve imports.
+As far as the implementation is concerned, we never have to worry
+about handling module variables; we only need to do extra typechecks
+against (renamed) interface files.
 
-When we are typechecking an indefinite package (there may be leftover
-holes), things are a little more subtle.  When a signature is defined,
-we \emph{know} that it will never be unified against a proper module
-name.  So we can assign it some fresh original name.
+\subsection{Compilation of definite modules}\label{sec:compiling-definite}
 
-Edward: What I find a bit dodgy is that there still are circumstances
-where we will link a signature with a signature.  For example, if I have:
+Of course, we still have to compile the code, and this includes any
+subpackages which we have mixed in the dependencies to make them fully
+definite.  Let's take the following set of packages as an example:
 
 \begin{verbatim}
-package a where
-    A :: [ data A ]
-    B :: [ data A ]
-    M = ...
-    A = B
-    Q = ...
+package pkg-a where
+    A = ...
+    B = ... -- this code is ignored
+package pgk-b where -- indefinite package
+    A :: ...
+    B = [ import A; ... ]
+package pkg-c where
+    include pkg-a (A)
+    include pkg-b
+    C = [ import B; ... ]
 \end{verbatim}
 
-We haven't violated the linking rule, but if we chose separate original
-names for A and B, they need to be identified after the alias.
+With the linking invariant, we can simply walk the Backpack package ``tree'',
+compiling each of its dependencies.  Let's walk through it explicitly.\footnote{To simplify matters, we assume that there is only one instance of any
+PackageId in the database, so we omit the unique-ifying hashes from the
+ghc-pkg registration commands; we ignore the existence of version numbers
+and Cabal's dependency solver; finally, we do the compilation in
+one-shot mode, even though Cabal in practice will use the Make mode.}
 
-Fortunately, Q should typecheck as if the As are the same, but M should
-typecheck as if they are distinct.  There is some ordering here, and our
-claim (to be formally verified) is that these unifications can be
-resolved as we process them.
+First, we have to build \verb|pkg-a|.  This package has no dependencies
+of any kind, so compiling is much like compiling ordinary Haskell.  If
+it was already installed in the database, we wouldn't even bother compiling it.
 
-\subsection{Installing indefinite packages}\label{sec:indefinite-packages}
+\begin{verbatim}
+ADEPS =    # empty!
+ghc -c A.hs -package-name pkg-a-ADEPS
+ghc -c B.hs -package-name pkg-a-ADEPS
+# install and register pkg-a-ADEPS
+\end{verbatim}
 
-If an indefinite package contains no code at all, we only need
-to install the interface file for the signatures.  However, if
-they include code, we must provide all of the
-ingredients necessary to compile them when the holes are linked against
-actual implementations.  (Figure~\ref{fig:pkgdb})
+Next, we have to build \verb|pkg-b|.  This package has a hole \verb|A|,
+intuitively, it depends on package A.  This is done in two steps:
+first we check if the signature given for the hole matches up with the
+actual implementation provided, and then we build the module properly.
 
-\paragraph{Source tarball or preprocessed source?}  An ancillary design choice
-to be made is what the representation of the source that is saved is.  There
-are a number of possible choices:
+\begin{verbatim}
+BDEPS = "A -> pkg-a-ADEPS:A"
+# This doesn't actually create an hi-boot file
+ghc -c A.hs-boot -package-name pkg-b-BDEPS -module-env BDEPS
+ghc -c B.hs      -package-name pkg-b-BDEPS -module-env BDEPS
+# install and register pkg-b-BDEPS
+\end{verbatim}
 
-\begin{itemize}
-    \item The original tarballs downloaded from Hackage,
-    \item Preprocessed source files,
-    \item Some sort of internal, type-checked representation of Haskell code (maybe the output of the desugarer).
-\end{itemize}
+Notably, these commands diverge slightly from the traditional compilation process.
+Traditionally, we would specify the flags
+\verb|-hide-all-packages| \verb|-package-id package-a-ADEPS| in order to
+let GHC know that it should look at this package to find modules,
+including \verb|A|.  However, if we did this here, we would also pull in
+module B, which is incorrect, as this module was thinned out in the parent
+package description.  Conceptually, this package is being compiled in the
+context of some module environment \verb|BDEPS| (a logical context, in Backpack lingo)
+which maps modules to original names and is utilized by the module finder to
+lookup the import in \verb|B.hs|.
 
-Storing the tarballs is the simplest and most straightforward mechanism,
-but we will have to be very certain that we can recompile the module
-later in precisely the same we compiled it originally, to ensure the hi
-files match up (fortunately, it should be simple to perform an optional
-sanity check before proceeding.) The appeal of saving preprocessed
-source, or even the IRs, is that this is conceptually this is exactly
-what an indefinite package is: we have paused the compilation process
-partway, intending to finish it later. It allows us to reuse the work
-done preprocessing or typechecking.  However, it may be the case that
-these phases work differently once library dependencies are known; typechecking
-especially, see Section~\ref{sec:variables}.
+Finally, we created all of the necessary subpackages, and we can compile
+our package proper.
 
-\subsection{Compilation}
+\begin{verbatim}
+CDEPS =         # empty!!
+ghc -c C.hs -package-name pkg-c-CDEPS -hide-all-packages \
+    -package pkg-a-ADEPS -hide-module B \
+    -package pkg-b-BDEPS
+# install and register package pkg-c-CDEPS
+\end{verbatim}
 
-When we need to compile an indefinite package (since all of its
-dependencies have been found), there seem to be two implementation
-strategies possible.  Here is a very simple example to consider for the
-various cases:
+This mostly resembles traditional compilation, but there are a few
+interesting things to note.  First, GHC needs to know about thinning/renaming
+in the package description (here, it's transmitted using the \verb|-hide-module|
+command, intended to apply to the most recent package definition).\footnote{Concrete
+command line syntax is, of course, up for discussion.}  Second, even though C
+``depends'' on subpackages, these do not show in its package-name identifier,
+e.g. CDEPS\@.  This is because this package \emph{chose} the values of ADEPS and BDEPS
+explicitly (by including the packages in this particular order), so there are no
+degrees of freedom.\footnote{In the presence of a Cabal-style dependency solver
+which associates a-0.1 with a concrete identifier a, these choices need to be
+recorded in the package ID.}  Finally, in principle, we could have also used
+the \verb|-module-env| flag to communicate how to lookup the B import (notice
+that the \verb|-package pkg-a-ADEPS| argument is a bit useless because we
+never end up using the import.)  I will talk a little more about the tradeoffs
+shortly.
+
+Overall, there are a few important things to notice about this architecture.
+First, because the \verb|pkg-b-BDEPS| product is installed, if in another package
+build we instantiate the indefinite module B with exactly the same \verb|pkg-a|
+implementation, we can skip the compilation process and reuse the version.
+This is because the calculated \verb|BDEPS| will be the same, and thus the package
+IDs will be the same.
+
+XXX ToDo: actually write down pseudocode algorithm for this
+
+\paragraph{Module environment or package flags?}  In the previous
+section, I presented two ways by which one can tweak the behavior of
+GHC's module finder, which is responsible for resolving \verb|import B|
+into an actual physical module.  The first, \verb|-module-env| is to
+explicitly describe a full mapping from module names to original names;
+the second, \verb|-package| with \verb|-hide-module| and
+\verb|-rename-module|, is to load packages as before but apply
+thinning/renaming as necessary.
+
+In general, it seems that using \verb|-package| is desirable, because its
+input size is smaller. (If a package exports 200 modules, we would be obligated
+to list all of them in a module environment.)  However, a tricky situation
+occurs when some of these modules come from a parent package:
 
 \begin{verbatim}
-package pkg-a where
-    A = ...
-package pgk-b where -- indefinite package
-    A :: ...
-    B = [ b = ... ]
-package pkg-c where
-    include pkg-a
-    include pkg-b
+package myapp2 where
+    System.Random = [ ... ].hs
+    include monte-carlo
+    App = [ ... ].hs
 \end{verbatim}
 
-\paragraph{The ``downstream'' proposal}  This is Simon's favorite
-proposal.  Because of the linking invariant, if we traverse the Backpack
-specification, any given module we need to compile will have all of its
-dependencies compiled (since it could only depend on the dependency if
-there was a signature, and the signature could not have been linked
-unless it was implemented previously.)  So we just go ahead and compile
-everything one-by-one, as if the package was a single big package.  (Of
-course, if we encounter a definite package, don't bother recompiling
-it; just use it directly.)  In
-particular, we maintain the invariant that any code generated will
+Here, monte-carlo depends on a ``subpart of the myapp2 package'', and it's
+not entirely clear how monte-carlo should be represented in the installed
+package database: should myapp2 be carved up into pieces so that subparts
+of its package description can be installed to the database?  A package
+stub like this would never used by any other package, it is strictly local.
+
+On the other hand, if one uses a module environment for specifying how
+\verb|monte-carlo| should handle \verb|System.Random|, we don't actually
+have to create a stub package: all we have to do is make sure GHC knows
+how to find the module with this original name.  To make things better,
+the size of the module environment will only be as long as all of the
+holes visible to the module in the package description, so the user will
+have explicitly asked for all of this pluggability.
+
+The conclusion seems clear: package granularity for modules from includes,
+and module environments for modules from parent packages!
+
+\paragraph{An appealing but incorrect alternative}  In this section,
+we briefly describe an alternate compilation strategy that might
+sound good, but isn't so good.  The basic idea is, when compiling
+\verb|pkg-c|, to compile all of its indefinite packages as if the
+package were one single, big package.
+(Of course, if we encounter a
+definite package, don't bother recompiling it; just use it directly.)
+In particular, we maintain the invariant that any code generated will
 export symbols under the current package's namespace.  So the identifier
 \verb|b| in the example becomes a symbol \verb|pkg-c_pkg-b_B_b| rather
 than \verb|pkg-b_B_b| (package subqualification is necessary because
 package C may define its own B module after thinning out the import.)
 
-One big problem with this proposal is that it doesn't implement applicative
-semantics.  If there is another package:
+The fatal problem with this proposal is that it doesn't implement applicative
+semantics beyond compilation units.  While modules within a single
+compilation will get reused, if there is another package:
 
 \begin{verbatim}
 package pkg-d where
@@ -569,349 +874,583 @@ package pkg-d where
     include pkg-b
 \end{verbatim}
 
-this will generate its own instance of B, even though it should be the same
-as C.  Simon was willing to entertain the idea that, well, as long as the
-type-checker is able to figure out they are the same, then it might be OK
-if we accidentally generate two copies of the code (provided they actually
-are the same).
-
-\paragraph{The ``upstream'' proposal}
-The problem with the ``downstream'' proposal is that it always recompiles
-all of the indefinite parts of the package, even if some of them should
-be shared in some sense.  Hypothetically, a fully linked version of an
-indefinite package should be considered a package in its own right
-(in particular, it is associated with a physical module identity in Backpack).
-So all we need to do is store these installed packages somewhere, probably
-the local package database.  If we recompile the same dependency chain,
-the installed package can be simply reused.  These products do not have
-to be exposed.
-
-One problem with this proposal is in this previous example:
-
-\begin{verbatim}
-package myapp2 where
-    System.Random = [ ... ].hs
-    include monte-carlo
-\end{verbatim}
-
-Here, monte-carlo depends on a ``subpart of the myapp2 package'', and it's
-not entirely clear how to express this.
+when it is compiled by itself, it will generate its own instance of B,
+even though it should be the same as C.  This is bad news.
 
-\subsection{Restricted recursive modules ala hs-boot}
+\subsection{Restricted recursive modules ala hs-boot}\label{sec:hs-boot-restrict}
 
 It should be possible to support GHC-style mutual recursion using the
 Backpack formalism immediately using hs-boot files.  However, to avoid
 the need for a shaping pass, we must adopt an existing constraint that
 already applies to hs-boot files: \emph{at the time we define a signature,
-we must know what the original name for all data types is}.  We then
-compile modules as usual, but compiling against the signature as if it
-were an hs-boot file.
-
-(ToDo: Figure out why this eliminates the shaping pass)
+we must know what the original name for all data types is}.  In practice,
+GHC enforces this by stating that: (1) an hs-boot file must be
+accompanied with an implementation, and (2) the implementation must
+in fact define (and not reexport) all of the declarations in the signature.
+
+Why does this not require a shaping pass? The reason is that the
+signature is not really polymorphic: we require that the $\alpha$ module
+variable be resolved to a concrete module later in the same package, and
+that all the $\beta$ module variables be unified with $\alpha$. Thus, we
+know ahead of time the original names and don't need to deal with any
+renaming.\footnote{This strategy doesn't completely resolve the problem
+of cross-package mutual recursion, because we need to first compile a
+bit of the first package (signatures), then the second package, and then
+the rest of the first package.}
 
 Compiling packages in this way gives the tantalizing possibility
 of true separate compilation: the only thing we don't know is what the actual
 package name of an indefinite package will be, and what the correct references
 to have are.  This is a very minor change to the assembly, so one could conceive
-of dynamically rewriting these references at the linking stage.
+of dynamically rewriting these references at the linking stage.  But
+separate compilation achieved in this fashion would not be able to take
+advantage of cross-module optimizations.
+
+\section{Shaped Backpack}
+
+Despite the simplicity of shapeless Backpack with the linking
+restriction in the absence of holes, we will find that when we have
+holes, it will be very difficult to do type-checking without
+some form of shaping.  This section is very much a work in progress,
+but the ability to typecheck against holes, even with the linking restriction,
+is a very important part of modular separate development, so we will need
+to support it at some ponit.
+
+\subsection{Efficient shaping}
+
+(These are Edward's opinion, he hasn't convinced other folks that this is
+the right way to do it.)
+
+In this section, I want to argue that, although shaping constitutes
+a pre-pass which must be run before compilation in earnest, it is only
+about as bad as the dependency resolution analysis that GHC already does
+in \verb|ghc -M| or \verb|ghc --make|.
+
+In Paper Backpack, what information does shaping compute? It looks at
+exports, imports, data declarations and value declarations (but not the
+actual expressions associated with these values.)  As a matter of fact,
+GHC already must look at the imports associated with a package in order
+to determine the dependency graph, so that it can have some order to compile
+modules in.  There is a specialized parser which just parses these statements,
+and then ignores the rest of the file.
+
+A bit of background: the \emph{renamer} is responsible for resolving
+imports and figuring out where all of these entities actually come from.
+SPJ would really like to avoid having to run the renamer in order to perform
+a shaping pass.
+
+\paragraph{Is it necessary to run the Renamer to do shaping?}
+Edward and Scott believe the answer is no, well, partially.
+Shaping needs to know the original names of all entities exposed by a
+module/signature. Then it needs to know (a) which entities a module/signature
+defines/declares locally and (b) which entities that module/signature exports.
+The former, (a), can be determined by a straightforward inspection of a parse
+tree of the source file.\footnote{Note that no expression or type parsing
+is necessary. We only need names of local values, data types, and data
+constructors.} The latter, (b), is a bit trickier. Right now it's the Renamer
+that interprets imports and exports into original names, so we would still
+rely on that implementation. However, the Renamer does other, harder things
+that we don't need, so ideally we could factor out the import/export
+resolution from the Renamer for use in shaping.
+
+Unfortunately the Renamer's import resolution analyzes \verb|.hi| files, but for
+local modules, which haven't yet been typechecked, we don't have those.
+Instead, we could use a new file format, \verb|.hsi| files, to store the shape of
+a locally defined module. (Defined packages are bundled with their shapes,
+so included modules have \verb|.hsi| files as well.) (What about the logical
+vs.~physical distinction in file names?) If we refactor the import/export
+resolution code, could we rewrite it to generically operate on both
+\verb|.hi| files and \verb|.hsi| files?
+
+Alternatively, rather than storing shapes on a per-source basis, we could
+store (in memory) the entire package shape. Similarly, included packages
+could have a single shape file for the entire package. Although this approach
+would make shaping non-incremental, since an entire package's shape would
+be recomputed any time a constituent module's shape changes, we do not expect
+shaping to be all that expensive.
+
+\subsection{Typechecking of indefinite modules}\label{sec:typechecking-indefinite}
+
+Recall in our argument in the definite case, where we showed there are
+no holes in the physical context.  With indefinite modules, this is no
+longer true. While (with the linking restriction) these holes will never
+be linked against a physical implementation, they may be linked against
+other signatures.  (Note: while disallowing signature linking would
+solve our problem, it would disallow a wide array of useful instances of
+signature reuse, for example, a package mylib that implements both
+mylib-1x-sig and mylib-2x-sig.)
+
+With holes, we must handle module variables, and we sometimes must unify them:
 
-\iffalse%
+\begin{verbatim}
+package p where
+    A :: [ data A ]
+package q where
+    A :: [ data A ]
+package r where
+    include p
+    include q
+\end{verbatim}
 
-\section{Module variables and original names}\label{sec:variables}
+In this package, it is not possible to a priori assign original names to
+module A in p and q, because in package r, they should have the same
+original name.  When signature linking occurs, unification may occur,
+which means we have to rename all relevant original names. (A similar
+situation occurs when a module is typechecked against a signature.)
 
-In Backpack, the physical identities of modules are in fact trees of
-variables, constructors and recursive module identities.  As we
-mentioned in Section~\ref{sec:ipi}, for concrete modules where there are
-no free variables, physical identity maps nicely to an original name.
-For packages with holes, the original names mechanism needs to be more
-flexible; we need to first run a shaping pass in order to figure out if
-a module is actually equal to another.
+An invariant which would be nice to have is this: when typechecking a
+signature or including a package, we may apply renaming to the entities
+being brought into context.  But once we've picked an original name for
+our entities, no further renaming should be necessary. (Formally, in the
+unification for semantic object shapes, apply the unifier to the second
+shape, but not the first one.)
 
-The direct approach is to replace original names with Backpack's
-physical identities and use unification to do comparisons.  However,
-this would require extremely invasive changes to all aspects of GHC, as
-the original names assumption is baked quite deeply into the compiler:
-we'd like to avoid upsetting this applecart if possible.
+However, there are plenty of counterexamples here:
 
-One key insight is that when we can only compile when all of the holes
-are eliminated; thus all parts of the compilation pipeline beyond
-typechecking can, in fact, assume that they will only be dealing with
-concrete module identities.  One interpretation of this fact is that
-we might actually be able to implement unification properly.
+\begin{verbatim}
+package p where
+    A :: [ data A ]
+    B :: [ data A ]
+    M = ...
+    A = B
+\end{verbatim}
 
-This gives us more latitude for how to
-deal with the identities during typechecking: we may, for example,
-adopt a conservative analysis (or an optional, dangerously liberal one),
-secure in the knowledge that when we compile the final concrete module,
-we will typecheck again with everything put together properly.
+In this package, does module M know that A.A and B.A are type equal?  In
+fact, the shaping pass will have assigned equal module identities to A
+and B, so M \emph{equates these types}, despite the aliasing occurring
+after the fact.
 
-The next subsection describes one proposal for dealing with this issue,
-and in what ways it is unsound.  We imagine there are other strategies
+We can make this example more sophisticated, by having a later
+subpackage which causes the aliasing; now, the decision is not even a
+local one (on the other hand, the equality should be evident by inspection
+of the package interface associated with q):
 
-\subsection{Holes have physical module identities associated with definition site}
+\begin{verbatim}
+package p where
+    A :: [ data A ]
+    B :: [ data A ]
+package q where
+    A :: [ data A ]
+    B = A
+package r where
+    include p
+    include q
+\end{verbatim}
 
-When compiling a module with a hole, we create a set of interface files
-from the signature.  In the current architecture of GHC, we implicitly
-assume that all interface files are associated with an \emph{original
-name} (see below); thus, this means that it is very natural to assign an
-original name to every hole.  If we have a signature package:
+Another possibility is that it might be acceptable to do a mini-shaping
+pass, without parsing modules or signatures, \emph{simply} looking at
+names and aliases.  But logical names are not the only mechanism by
+which unification may occur:
 
 \begin{verbatim}
-package foo-1x-sig where
-    Foo :: ...
+package p where
+    C :: [ data A ]
+    A = [ data A = A ]
+    B :: [ import A(A) ]
+    C = B
 \end{verbatim}
 
-Then the physical identity associated with Foo would be
-\verb|foo-1x-sig_Foo| (rather than a fresh module variable $\alpha$).
+It is easy to conclude that the original names of C and B are the same.  But
+more importantly, C.A must be given the original name of p:A.A.  This can only
+be discovered by looking at the signature definition for B. In any case, it
+is worth noting that this situation parallels the situation with hs-boot
+files (although there is no mutual recursion here).
 
-This has implications for signature linking. Take this example from
-Section 2.3 of the Backpack paper:
+The conclusion is that you will probably, in fact, have to do real
+shaping in order to typecheck all of these examples.
+
+\paragraph{Hey, these signature imports are kind of tricky\ldots}
+
+When signatures and modules are interleaved, the interaction can be
+complex.  Here is an example:
 
 \begin{verbatim}
-package yourlib where
-    Prelude :: [data List a = ...]
-    Yours :: [import Prelude; ...]
+package p where
+    C :: [ data A ]
+    M = [ import C; ... ]
+    A = [ import M; data A = A ]
+    C :: [ import A(A) ]
+\end{verbatim}
 
-package mylib where
-    Prelude :: [data Bool = ...]
-    include yourlib
-    Mine = [import Prelude; import Yours; ...]
+Here, the second signature for C refers to a module implementation A
+(this is permissible: it simply means that the original name for p:C.A
+is p:A.A).  But wait! A relies on M, and M relies on C. Circularity?
+Fortunately not: a client of package p will find it impossible to have
+the hole C implemented in advance, since they will need to get their hands on module
+A\ldots but it will not be defined prior to package p.
+
+In any case, however, it would be good to emit a warning if a package
+cannot be compiled without mutual recursion.
+
+\subsection{Incremental typechecking}
+We want to typecheck modules incrementally, i.e., when something changes in
+a package, we only want to re-typecheck the modules that care about that
+change. GHC already does this today.%
+\footnote{\url{https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/RecompilationAvoidance}}
+Is the same mechanism sufficient for Backpack? Edward and Scott think that it
+is, mostly. Our conjecture is that a module should be re-typechecked if the
+existing mechanism says it should \emph{or} if the logical shape
+context (which maps logical names to physical names) has changed. The latter
+condition is due to aliases that affect typechecking of modules.
+
+Let's look again at an example from before:
+\begin{verbatim}
+package p where
+    A :: [ data A ]
+    B :: [ data A ]
+    M = [ import A; import B; ... ]
 \end{verbatim}
+Let's say that \verb|M| is typechecked successfully. Now we add an alias binding
+at the end of the package, \verb|A = B|. Does \verb|M| need to be
+re-typechecked? Yes! (Well, it seems so, but let's just assert ``yes'' for now.
+Certainly in the reverse case---if we remove the alias and then ask---this
+is true, since \verb|M| might have depended on the two \verb|A| types
+being the same.)
+The logical shape context changed to say that \verb|A| and
+\verb|B| now map to the same physical module identity. But does the existing
+recompilation avoidance mechanism say that \verb|M| should be re-typechecked?
+It's unclear. The \verb|.hi| file for \verb|M| records that it imported \verb|A| and
+\verb|B| with particular ABIs, but does it also know about the physical module
+identities (or rather, original module names) of these modules?
+
+Scott thinks this highlights the need for us to get our story straight about
+the connection between logical names, physical module identities, and file
+names!
+
+
+\subsection{Installing indefinite packages}\label{sec:installing-indefinite}
 
-The first order of business is that we have to merge the interfaces of
-the two Prelude holes, which are associated with different generated
-physical identities (\verb|yourlib_Prelude| and \verb|mylib_Prelude|),
-and furthermore, \emph{assign an original name to it}.  If we pick,
-for example, \verb|mylib_Prelude|, none of the types defined in \verb|yourlib|
-will unify in \verb|Mine|; thus, we would need to rename the original names
-in \verb|yourlib|.\footnote{Edward: I don't think this is really the
-right way to talk about this: Backpack requires a shaping pass and we should
-be talking about it}
+If an indefinite package contains no code at all, we only need
+to install the interface file for the signatures.  However, if
+they include code, we must provide all of the
+ingredients necessary to compile them when the holes are linked against
+actual implementations.  (Figure~\ref{fig:pkgdb})
 
-% ezyang: So, I thought I knew what I was talking about here, but actually
-% the text here needs to be put in the context of shaping, so I need to
-% think about this some more
+\paragraph{Source tarball or preprocessed source?}  What is the representation of the source that is saved is.  There
+are a number of possible choices:
 
-\paragraph{Instantiation and reuse}
+\begin{itemize}
+    \item The original tarballs downloaded from Hackage,
+    \item Preprocessed source files,
+    \item Some sort of internal, type-checked representation of Haskell code (maybe the output of the desugarer).
+\end{itemize}
 
-If we only ever linked any written signature with a signle implementation, this would actually
-be great: when it is time to properly compile a module with holes, we
-type check against the true original name of the new module (and just
-do a consistency check between the signature and the implementation, modulo
-differences in the physical identity)---a case of typechecking proceeding
-differently between the initial typecheck and final compilation.
+Storing the tarballs is the simplest and most straightforward mechanism,
+but we will have to be very certain that we can recompile the module
+later in precisely the same we compiled it originally, to ensure the hi
+files match up (fortunately, it should be simple to perform an optional
+sanity check before proceeding.) The appeal of saving preprocessed
+source, or even the IRs, is that this is conceptually this is exactly
+what an indefinite package is: we have paused the compilation process
+partway, intending to finish it later.  However, our compilation strategy
+for definite packages requires us to run this step using a \emph{different}
+choice of original names, so it's unclear how much work could actually be reused.
 
-However, conflating a variable with an original name is very bad business.
-Consider the graph library 
+\section{Surface syntax}
 
-However, Backpack supports the linking of two signatures together, which
-now presents a formidable difficulty: the original names of these two
-signatures now must be identified.  Here is a real-world example where
-this shows up:
+In the Backpack paper, a brand new module language is presented, with
+syntax for inline modules and signatures.  This syntax is probably worth implementing,
+because it makes it easy to specify compatibility packages, whose module
+definitions in general may be very short:
 
 \begin{verbatim}
-package foo-1x-sig where
-    Foo :: ...
+package ishake-0.12-shake-0.13 where
+    include shake-0.13
+    Development.Shake.Sys = Development.Shake.Cmd
+    Development.Shake = [ (**>) = (&>) ; (*>>) = (|*>)]
+    Development.Shake.Rule = [ defaultPriority = rule . priority 0.5 ]
+    include ishake-0.12
+\end{verbatim}
 
-package foo-2x-sig where
-    include foo-1x-sig
-    Foo :: ...
+However, there are a few things that are less than ideal about the
+surface syntax proposed by Paper Backpack:
 
-package foo-2.1 where
-    include foo-2x-sig
-    Foo = ...
+\begin{itemize}
+    \item It's completely different from the current method users
+        specify packages. There's nothing wrong with this per se
+        (one simply needs to support both formats) but the smaller
+        the delta, the easier the new packaging format is to explain
+        and implement.
+
+    \item Sometimes order matters (relative ordering of signatures and
+        module implementations), and other times it does not (aliases).
+        This can be confusing for users.
+
+    \item Users have to order module definitions topologically,
+        whereas in current Cabal modules can be listed in any order, and
+        GHC figures out an appropriate order to compile them.
+\end{itemize}
 
-package A where
-    include foo-1x-sig
-    A = ...
+Here is an alternative proposal, closely based on Cabal syntax.  Given
+the following Backpack definition:
 
-package B where
-    include foo-2x-sig
-    B = ...
+\begin{verbatim}
+package libfoo(A, B, C, Foo) where
+    include base
+    -- renaming and thinning
+    include libfoo (Foo, Bar as Baz)
+    -- holes
+    A :: [ a :: Bool ].hsig
+    A2 :: [ b :: Bool ].hsig
+    -- normal module
+    B = [
+        import {-# SOURCE #-} A
+        import Foo
+        import Baz
+        ...
+    ].hs
+    -- recursively linked pair of modules, one is private
+    C :: [ data C ].hsig
+    D = [ import {-# SOURCE #-} C; data D = D C ].hs
+    C = [ import D; data C = C D ].hs
+    -- alias
+    A = A2
+\end{verbatim}
 
-package C where
-    include A
-    include B
-    C = ...
+We can write the following Cabal-like syntax instead (where
+all of the signatures and modules are placed in appropriately
+named files):
 
-package D where
-    include C
-    include foo-2.1
+\begin{verbatim}
+package: libfoo
+...
+build-depends: base, libfoo (Foo, Bar as Baz)
+holes: A A2 -- deferred for now
+exposed-modules: Foo B C
+aliases: A = A2
+other-modules: D
 \end{verbatim}
 
-Here, we have two signatures for the \verb|foo| library, one of which
-is a subset of another (but they are ostensibly backwards compatible).
-Package A only uses the 1.x interface, but package B uses the 2.x interface.
-Package C uses both of these packages (and implicitly links the two signatures
-together), and package D finally links in an actual implementation of the
-library.
+Notably, all of these lists are \emph{insensitive} to ordering!
+The key idea is use of the \verb|{-# SOURCE #-}| pragma, which
+is enough to solve the important ordering constraint between
+signatures and modules.
 
+Here is how the elaboration works.  For simplicity, in this algorithm
+description, we assume all packages being compiled have no holes
+(including \verb|build-depends| packages). Later, we'll discuss how to
+extend the algorithm to handle holes in both subpackages and the main
+package itself.
 
+\begin{enumerate}
 
-However, directly modifying original names in this fashion
-is likely to be too invasive of a change, since the current compiler has
-the assumption that original names can always be checked for equality
-is deeply wired in.
+    \item At the top-level with \verb|package| $p$ and
+        \verb|exposed-modules| $ms$, record \verb|package p (ms) where|
+
+    \item For each package $p$ with thinning/renaming $ms$ in
+        \verb|build-depends|, record a \verb|include p (ms)| in the
+        Backpack package.  The ordering of these includes does not
+        matter, since none of these packages have holes.
+
+    \item Take all modules $m$ in \verb|other-modules| and
+        \verb|exposed-modules| which were not exported by build
+        dependencies, and create a directed graph where hs and hs-boot
+        files are nodes and imports are edges (the target of an edge is
+        an hs file if it is a normal import, and an hs-boot file if it
+        is a SOURCE import).  Topologically sort this graph, erroring if
+        this graph contains cycles (even with recursive modules, the
+        cycle should have been broken by an hs-boot file).  For each
+        node, in this order, record \verb|M = [ ... ]| or \verb|M :: [ ... ]|
+        depending on whether or not it is an hs or hs-boot.  If possible,
+        sort signatures before implementations when there is no constraint
+        otherwise.
 
-Aliasing of signatures means that it is no longer the case that
-original name means type equality.  We were not able to convince
-Simon of any satisfactory resolution.  Strawman proposal is to
-extending original names to also be variables probably won't work
-because it is so deeply wired, but it's difficult to construct hi
-files so that everything works out (quadratic).
+\end{enumerate}
 
+Here is a simple example which shows how SOURCE can be used to disambiguate
+between two important cases. Suppose we have these modules:
 
-There are some problems with respect to what occurs when two
-distinct signatures are linked together (aliasing), we talk these problems in
-Section~\ref{sec:open-questions}.
+\begin{verbatim}
+-- A1.hs
+import {-# SOURCE #-} B
 
-\fi
+-- A2.hs
+import B
 
-\subsection{Original names} Original names are an important design pattern
-in GHC\@.
-Sometimes, a name can be exposed in an hi file even if its module
-wasn't exposed. Here is an example (compiled in package R):
+-- B.hs
+x = True
+
+-- B.hs-boot
+x :: Bool
+\end{verbatim}
+
+Then we translate the following packages as follows:
 
 \begin{verbatim}
-module X where
-    import Internal (f)
-    g = f
+exposed-modules: A1 B
+-- translates to
+B :: [ x :: Bool ]
+A1 = [ import B ]
+B = [ x = True ]
+\end{verbatim}
 
-module Internal where
-    import Internal.Total (f)
+but
+
+\begin{verbatim}
+exposed-modules: A2 B
+-- translates to
+B = [ x = True ]
+B :: [ x :: Bool ]
+A2 = [ import B ]
 \end{verbatim}
 
-Then in X.hi:
+The import controls placement between signature and module, and in A1 it
+forces B's signature to be sorted before B's implementation (whereas in
+the second section, there is no constraint so we preferentially place
+the B's implementation first)
+
+\paragraph{Holes in the database} In the presence of holes,
+\verb|build-depends| resolution becomes more complicated.  First,
+let's consider the case where the package we are building is
+definite, but the package database contains indefinite packages with holes.
+In order to maintain the linking restriction, we now have to order packages
+from step (2) of the previous elaboration.  We can do this by creating
+a directed graph, where nodes are packages and edges are from holes to the
+package which implements them.  If there is a cycle, this indicates a mutually
+recursive package.  In the absence of cycles, a topological sorting of this
+graph preserves the linking invariant.
+
+One subtlety to consider is the fact that an entry in \verb|build-depends|
+can affect how a hole is instantiated by another entry.  This might be a
+bit weird to users, who might like to explicitly say how holes are
+filled when instantiating a package.  Food for thought, surface syntax wise.
+
+\paragraph{Holes in the package} Actually, this is quite simple: the
+ordering of includes goes as before, but some indefinite packages in the
+database are less constrained as they're ``dependencies'' are fulfilled
+by the holes at the top-level of this package.  It's also worth noting
+that some dependencies will go unresolved, since the following package
+is valid:
 
 \begin{verbatim}
-g = <R.id, Internal.Total, f> (this is the original name)
+package a where
+    A :: ...
+package b where
+    include a
 \end{verbatim}
 
-(The reason we refer to the package as R.id is because it's the
-full package ID, and not just R).
+\paragraph{Multiple signatures}  In Backpack syntax, it's possible to
+define a signature multiple times, which is necessary for mutually
+recursive signatures:
+
+\begin{verbatim}
+package a where
+    A :: [ data A ]
+    B :: [ import A; data B = B A ]
+    A :: [ import B; data A = A B ]
+\end{verbatim}
 
-How might internal names work with Backpack?
+Critically, notice that we can see the constructors for both module B and A
+after the signatures are linked together.  This is not possible in GHC
+today, but could be possible by permitting multiple hs-boot files.  Now
+the SOURCE pragma indicating an import must \emph{disambiguate} which
+hs-boot file it intends to include.  This might be one way of doing it:
 
 \begin{verbatim}
-package P where
-    M = ...
-    N = ...
-package Q (M, R, T)
-    include P (N -> R)
-    T = ...
+-- A.hs-boot2
+data A
+
+-- B.hs-boot
+import {-# SOURCE hs-boot2 #-} A
+
+-- A.hs-boot
+import {-# SOURCE hs-boot #-} B
 \end{verbatim}
 
-And now if we look at Q\@:
+\paragraph{Explicit or implicit reexports}  One annoying property of
+this proposal is that, looking at the \verb|exposed-modules| list, it is
+not immediately clear what source files one would expect to find in the
+current package.  It's not obvious what the proper way to go about doing
+this is.
+
+\paragraph{Better syntax for SOURCE}  If we enshrine the SOURCE import
+as a way of solving Backpack ordering problems, it would be nice to have
+some better syntax for it. One possibility is:
 
 \begin{verbatim}
-exposed-modules:
-        M -> <P.id, M>
-        R -> <P.id, N>
-        T -> <Q.id, T>
+abstract import Data.Foo
 \end{verbatim}
 
-When we compile Q, and the interface file gets generated, we have
-to generate identifiers for each of the exposed modules.  These should
-be calculated to directly refer to the ``original name'' of each them;
-so for example M and R point directly to package P, but they also
-include the original name they had in the original definition.
+which makes it clear that this module is pluggable, typechecking against
+a signature.  Note that this only indicates how type checking should be
+done: when actually compiling the module we will compile against the
+interface file for the true implementation of the module.
+
+It's worth noting that the SOURCE annotation was originally made a
+pragma because, in principle, it should have been possible to compile
+some recursive modules without needing the hs-boot file at all. But if
+we're moving towards boot files as signatures, this concern is less
+relevant.
 
-\section{Shaping}\label{sec:shaping}
+\section{Bits and bobs}
 
-Here is a hyper-simplified picture of how Backpack in its full glory might look.
+\subsection{Abstract type synonyms}
 
-Recall in Figure~\ref{fig:pkgdb}, we have Cabal which is responsible for
-taking Cabal files and invoking GHC to build an installed package.  The
-command line looks something like:
+In Paper Backpack, abstract type synonyms are not permitted, because GHC doesn't
+understand how to deal with them.  The purpose of this section is to describe
+one particularly nastiness of abstract type synonyms, by way of the occurs check:
 
 \begin{verbatim}
-ghc --make
-    -package-name a-0.1
-    -hide-all-packages
-    -package-id containers-0.9-ABCD
-    Module1 Module2
+A :: [ type T ]
+B :: [ import qualified A; type T = [A.T] ]
 \end{verbatim}
 
-We notice a few things, first that GHC accepts some flags which
-configure its view of the package database (really it's just loaded
-in-memory), so that when we perform an import, GHC knows how to find the
-module (\verb|findModule|).
-
-The claim is that we can implement Backpack by adding an extra pass
-to Cabal which we will call the shaper, which performs the shaping pass
-as described by the Backpack paper.  In full generality, the \emph{module shape}
-is what needs to be passed from Cabal to GHC, but in our simplified example
-we're just going to deal with what SPJ calls the ``module environment'' (which
-roughly corresponds to a logical shape context in the paper.)  This module
-environment maps logical module names to the \emph{original names}, i.e.
-overloading the behavior of how we find modules on imports.
-
-We'll go by way of an example:
-
-\begin{verbatim}
-package a1 where
-    A :: [ data T; f : T -> T ]
-package a2 where
-    A :: [ data T; g : T -> T ]
-package b
-    include a1
-    include a2
-    A = [ ... ] -- call physical identity b-2.7:A
-\end{verbatim}
-
-At the end of the day, we'd like package b to be compiled with a map from
-logical name A to physical identity \verb|b-2.7:A|. But what about packages
-a1 and a2?  Since these have holes, we don't really know what their physical
-identities are; but that doesn't mean we don't talk about them; instead,
-we have a module variable for the holes.  These holes have signatures, which can be thought
-of as the interface files.  So we have:\footnote{The type signatures are not quite right because they need provenance information, but never-mind that for now.} \\
-
-\noindent
-\verb|a1:| $\forall \alpha.\ \mathrm{A} \mapsto \alpha \mbox{\texttt{\ ::\ [ data T\@; f :\ T -> T ]}}$ \\ % chktex 26
-\verb|a2:| $\forall \alpha.\ \mathrm{A} \mapsto \alpha \mbox{\texttt{\ ::\ [ data T\@; g :\ T -> T ]}}$ % chktex 26
-
-Now lets consider what happens as we do the shaping analysis on package b.
-We process each line of the module one-by-one, and initially, we start
-with an empty module environment.  When we process the first include, we
-now know about a mapping $A \mapsto \beta$, but we don't know the physical
-identity of the module so we gin up a module variable for now.  The second
-include, we have to instantiate the universal quantifier with $\beta$ because
-signature linking demands the modules be the same. Finally, when we hit the
-module definition, we see that $A \mapsto \mathtt{b-2.7:A}$.
-
-Now, importantly, remember that there were hi files associated with each
-of the signatures, and these hi files may contained original names
-corresponding to our module variables.  As we processed the mapping, we
-also built up a renaming of physical variable names to their true
-symbols, so we need to rename the respective $\alpha$s in each interface
-file to point ot \texttt{b-2.7:A}, as we ended up seeing.
-
-(SPJ and I went through a few other examples, including the case of recursive
-module linking:
-
-\begin{verbatim}
-package a1 where
-    A :: ...
-    B = [import A]
-package b where
-    include a1
-    A = [import B]
+At this point, it is illegal for \verb|A = B|, otherwise this type synonym would
+fail the occurs check.  This seems like pretty bad news, since every instance
+of the occurs check in the type-checker could constitute a module inequality.
+
+\subsection{Type families}
+
+Like type classes, type families must not overlap (and this is a question of
+type safety!)
+
+A more subtle question is compatibility and apartness of type family
+equations.  Under these checks, aliasing of modules can fail if it causes
+two type families to be identified, but their definitions are not apart.
+Here is a simple example:
+
+\begin{verbatim}
+A :: [
+    type family F a :: *
+    type instance F Int = Char
+]
+B :: [
+    type family F a :: *
+    type instance F Int = Bool
+]
 \end{verbatim}
 
-and verified it worked.  Note that recursively linked modules do not get
-inlining! We ust need to know what the original name of what we're linking
-against is, so we can stick in the right symbols.)
+Now it is illegal for \verb|A = B|, because when the type families are
+unified, the instances now fail the apartness check.  However, if the second
+instance was \verb|F Int = Char|, the families would be able to link together.
 
-Now, the most paper-like thing one an do in this circumstance is to pass
-over the renaming, but we'd like to avoid having command line arguments
-that are too long.  So SPJ's proposal is that, instead, we have a \emph{module
-interface file} (or \emph{module manifest}) which collects the various information
-that we might be interested in about module providence and renaming.  Now,
-in order to program GHC to have the right logical namespace, we only need
-to list the appropriate package manifests but with the appropriate thinning
-and renaming.  This could be shorter, and maps more nicely onto the existing
-package command line flags.  We'd have to make sure this works out, but it's
-exactly analogous to how we do interface files.
+To make matters worse, an implementation may define more axioms than are
+visible in the signature:
+
+\begin{verbatim}
+package a where
+    A :: [
+        type family F a :: *
+        type instance F Int = Bool
+    ]
+package b where
+    include a
+    B = [
+        import A
+        type instance F Bool = Bool
+        ...
+    ]
+package c where
+    A = [
+        type family F a :: *
+        type instance F Int = Bool
+        type instance F Bool = Int
+    ]
+    include b
+\end{verbatim}
+
+It would seem that private axioms cannot be naively supported. Is
+there any way that thinning axioms could be made to work?
 
 \section{Open questions}\label{sec:open-questions}
 
@@ -919,91 +1458,35 @@ Here are open problems about the implementation which still require
 hashing out.
 
 \begin{itemize}
-    \item Aliasing of signatures means that it is no longer the case that
-      original name means type equality.  We were not able to convince
-      Simon of any satisfactory resolution.  Strawman proposal is to
-      extending original names to also be variables probably won't work
-      because it is so deeply wired, but it's difficult to construct hi
-      files so that everything works out (quadratic).
-
-  \item Relationship between linker names and InstalledPackageId? The reason
-      the obvious thing to do is use all of InstalledPackageId for linker
-      name, but this breaks recompilation.  So some of these things
-      should go in the linker name, and not others (yes package, yes
-      version, yes some compile flags (definitely ways), eventually
-      dependency package IDs, what about cabal build flags).  This is
-      approximately an ABI hash, but it's computable before compilation.
-      This worries Simon because now there are two names, but maybe
-      the DB can solve that problem---unfortunately, GHC doesn't ever
-      register during compilation; only later.
-
-        Simon also thought we should use shorter names for linker
-        names and InstallPkgIds.  This appears to be orthogonal.
-
-    \item In this example:
-
-\begin{verbatim}
-    package A where
-        A = ...
-    package A2 where
-        A2 = ...
-    package B (B)
-        A :: ...
-        B = ...
-    package C where
-        include A
-        include B
-    package D where
-        include A
-        include B
-    package E where
-        include C (B as CB)
-        include D (B as DB)
-\end{verbatim}
-
-      Do the seperate instantiations of B exist as seperate artifacts
-      in the database, or do they get constructed on the fly by
-      definite packages which include them?  The former is conceptually
-      nicer (identity of types work, closer to Backpack semantics), but
-      the latter is easier for linker names. (Simon's first inclination
-      is to construct it on the fly.)
-
-      There was another example, showing that we need to solve this
-      problem even for indefinite combinations of indefinite modules.
-      You can get to it by modifying the earlier example so that C and
-      D still have holes, which E does not fill.
-
-  \item We have to store the preprocessed sources for indefinite packages.
-      This is hard when we're constructing packages on the fly.
-
-  \item What is the impact on dependency solving in Cabal?  Old questions
-      of what to prefer when multiple package-versions are available
-      (Cabal originally only needed to solve this between different
-      versions of the same package, preferring the oldest version), but
-      with signatures, there are more choices.  Should there be a
-      complex solver that does all signature solving, or a preprocessing
-      step that puts things back into the original Cabal version.
-      Authors may want to suggest policy for what packages should actually
-      link against signatures (so a crypto library doesn't accidentally
-      link against a null cipher package).
-      \end{itemize}
-
-\section{Immediate tasks}
-
-At this point in time, it seems we can identify the following set
-of non-controversial tasks which can be started immediately.
 
-\begin{itemize}
-    \item Relax the package database constraint to allow multiple
-        instances of package-version. (Section~\ref{sec:ihg})
-    \item Propagate the use of \verb|InstalledPackageId| instead of
-        package IDs for typechecking. (Section~\ref{sec:ipi})
-    \item Implement export declarations in package format, so
-        packages can reexport modules from other packages. (Section~\ref{sec:reexport})
-\end{itemize}
+    \item In Section~\ref{sec:simplifying-backpack}, we argued that we
+        could implement Backpack without needing a shaping pass. We're
+        pretty certain that this will work for typechecking and
+        compiling fully definite packages with no recursive linking, but
+        in Section~\ref{sec:typechecking-indefinite}, we described some
+        of the prevailing difficulties of supporting signature linking.
+        Renaming is not an insurmountable problem, but backwards flow of
+        shaping information can be, and it is unclear how best to
+        accommodate this.  This is probably the most important problem
+        to overcome.
+
+    \item In Section~\ref{sec:installing-indefinite}, a few choices for how to
+        store source code were pitched, however, there is not consensus on which
+        one is best.
+
+    \item What is the impact of the multiplicity of PackageIds on
+        dependency solving in Cabal?  Old questions of what to prefer
+        when multiple package-versions are available (Cabal originally
+        only needed to solve this between different versions of the same
+        package, preferring the oldest version), but with signatures,
+        there are more choices.  Should there be a complex solver that
+        does all signature solving, or a preprocessing step that puts
+        things back into the original Cabal version.  Authors may want
+        to suggest policy for what packages should actually link against
+        signatures (so a crypto library doesn't accidentally link
+        against a null cipher package).
 
-The aliasing problem is probably the most important open problem
-blocking the rest of the system.
+\end{itemize}
 
 \bibliographystyle{plain}
 \bibliography{backpack-impl}