[docs/backpack] Get lint to stop complaining
[ghc.git] / docs / backpack / backpack-impl.tex
index 4e56d4b..46e397f 100644 (file)
@@ -480,8 +480,11 @@ 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!''} \\
 
-\noindent Flattening the package database may be too stiff a medicine for this
-project. Here are two alternatives.
+\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
@@ -513,7 +516,7 @@ 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.
+would not be so good.  SPJ is quite keen on this plan.
 
 \subsection{Exposed modules should allow external modules}\label{sec:reexport}
 
@@ -808,6 +811,8 @@ 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|
@@ -878,17 +883,28 @@ 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}
 
@@ -900,6 +916,59 @@ 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
@@ -1013,32 +1082,41 @@ 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{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.
-
-It is not difficult to imagine extending this parser to pick up other entities
-which a Haskell file may define, while skipping their actual definitions
-(it's enough to know if the module defines it or not.)  If this can be
-done acceptably quickly, there is no need to perform a renaming pass or
-anything complicated; that is all the preprocessing necessary.
+\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!
 
-(XXX maybe you can do something even more sophisticated and avoid picking
-up entities. ToDo: show a counterexample for this case.)
 
 \subsection{Installing indefinite packages}\label{sec:installing-indefinite}
 
@@ -1237,10 +1315,19 @@ 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} XXX Actually, I think this is simple:
-these holes are just part of the module graph from step (3), and get
-sorted in a normal way.  You can probably just place them all up top without
-causing any problems.
+\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}
+package a where
+    A :: ...
+package b where
+    include a
+\end{verbatim}
 
 \paragraph{Multiple signatures}  In Backpack syntax, it's possible to
 define a signature multiple times, which is necessary for mutually
@@ -1285,7 +1372,85 @@ abstract import Data.Foo
 \end{verbatim}
 
 which makes it clear that this module is pluggable, typechecking against
-a signature.
+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{Bits and bobs}
+
+\subsection{Abstract type synonyms}
+
+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}
+A :: [ type T ]
+B :: [ import qualified A; type T = [A.T] ]
+\end{verbatim}
+
+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}
+
+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.
+
+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}