\documentclass{article}

\usepackage{mdframed}
\usepackage{pifont}
\usepackage{graphicx} %[pdftex] OR [dvips]
\usepackage{fullpage}
\usepackage{wrapfig}
\usepackage{float}
\usepackage{titling}
\usepackage{hyperref}
\usepackage{tikz}
\usepackage{color}
\usepackage{footnote}
\usepackage{float}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{bigfoot}
\usepackage{amssymb}

\newenvironment{aside}
  {\begin{mdframed}[style=0,%
      leftline=false,rightline=false,leftmargin=2em,rightmargin=2em,%
          innerleftmargin=0pt,innerrightmargin=0pt,linewidth=0.75pt,%
      skipabove=7pt,skipbelow=7pt]\small}
  {\end{mdframed}}

\setlength{\droptitle}{-6em}

\newcommand{\Red}[1]{{\color{red} #1}}

\title{The Backpack algorithm}

\begin{document}

\maketitle

This document describes the Backpack shaping and typechecking
passes, as we intend to implement it.

\section{Front-end syntax}

For completeness, here is the package language we will be shaping and typechecking:

\begin{verbatim}
package     ::= "package" pkgname [pkgexports] "where" pkgbody
pkgbody     ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
pkgdecl     ::= "module"    modid [exports] where body
              | "signature" modid [exports] where body
              | "include"   pkgname [inclspec]
inclspec    ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
                [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
pkgexports  ::= inclspec
renaming    ::= modid "as" modid
\end{verbatim}

See the ``Backpack manual'' for more explanation about the syntax.  It
is slightly simplified here by removing any constructs which are easily implemented as
syntactic sugar (e.g. a \verb|modid| renaming is simply \verb|modid as modid|.)

\section{Shaping}

Shaping computes a \verb|Shape| which has this form:

\begin{verbatim}
Shape ::= provides: { ModName -> Module { Name } }
          requires: { ModName ->        { Name } }

PkgKey      ::= SrcPkgId "(" { ModName "->" Module } ")"
              | HOLE
Module      ::= PkgKey ":" ModName
Name        ::= Module "." OccName
OccName     ::= -- a plain old name, e.g. undefined, Bool, Int
\end{verbatim}

Starting with the empty shape, we incrementally construct a shape by
shaping package declarations (the partially constructed shape serves as
a context for renaming modules and signatures and instantiating
includes) and merging them until we have processed all declarations.
There are two things to specify: what shape each declaration has, and
how the merge operation proceeds.

One variation of shaping also computes the renamed version of a package,
i.e., where each identifier in the module and signature is replaced with
the original name (equivalently, we record the output of GHC's renaming
pass). This simplifies type checking because you no longer have to
recalculate the set of available names, which otherwise would be lost.
See more about this in the type checking section.

In the description below, we'll assume \verb|THIS| is the package key
of the package being processed.

\newpage

\subsection{\texttt{module M}}

Merge with this shape:

\begin{verbatim}
    provides: { M -> THIS:M { exports of renamed M } }
    requires: (nothing)
\end{verbatim}

\noindent Example:

\begin{verbatim}
    -- provides: (nothing)
    -- requires: (nothing)

    module A(T) where
        data T = T

    -- provides: A -> THIS:A { THIS:A.T }           -- NEW
    -- requires: (nothing)

    module M(T, f) where
        import A(T)
        f x = x

    -- provides: A -> THIS:A { THIS:A.T }
                 M -> THIS:M { THIS:A.T, THIS:M.f } -- NEW
    -- requires: (nothing)
\end{verbatim}

\newpage
\subsection{\texttt{signature M}}

Merge with this shape:

\begin{verbatim}
    provides: { M -> HOLE:M { exports of renamed M } }
    requires: { M ->        { exports of renamed M } }
\end{verbatim}

\noindent Example:

\begin{verbatim}
    -- provides: (nothing)
    -- requires: (nothing)

    signature H(T) where
        data T

    -- provides: H -> HOLE:H { HOLE:H.T }
    -- requires: H ->        { HOLE:H.T }

    module A(T) where
        import H(T)
    module B(T) where
        data T = T

    -- provides: H -> HOLE:H { HOLE:H.T }
    --           A -> THIS:A { HOLE:H.T } -- NEW
    --           B -> THIS:B { THIS:B.T } -- NEW
    -- requires: H ->        { HOLE:H.T }

    signature H(T, f) where
        import B(T)
        f :: a -> a

    -- provides: H -> HOLE:H { THIS:B.T, HOLE:H.f } -- UPDATED
    --           A -> THIS:A { THIS:B.T }           -- UPDATED
    --           B -> THIS:B { THIS:B.T }
    -- requires: H ->        { THIS:B.T, HOLE:H.f } -- UPDATED
\end{verbatim}

Notice that in the last example, when a signature with reexports is merged,
it can result in updates to the shapes of other module names.

\newpage

\subsection{\texttt{include pkg (X) requires (Y)}}

We merge with the transformed shape of package \verb|pkg|, where this
shape is transformed by:

\begin{itemize}
    \item Renaming and thinning the provisions according to \verb|(X)|
    \item Renaming requirements according to \verb|(Y)| (requirements cannot
          be thinned, so non-mentioned requirements are passed through.)
          For each renamed requirement from \verb|Y| to \verb|Y'|,
          substitute \verb|HOLE:Y| with \verb|HOLE:Y'| in the
          \verb|Module|s and \verb|Name|s of the provides and requires.
          (Freshen holes.)
    \item If there are no thinnings/renamings, you just merge the
          shape unchanged!
\end{itemize}

\noindent Example:

\begin{verbatim}
    package p (M) requires (H) where
        signature H where
            data T
        module M where
            import H
            data S = S T

    -- p requires: M -> { p(H -> HOLE:H):M.S }
    --   provides: H -> { HOLE:H.T }

    package q (A) where
        module X where
            data T = T

        -- provides: X -> { q():X.T }
        -- requires: (nothing)

        include p (M as A) requires (H as X)
        -- 1. Rename/thin provisions:
        --      provides: A -> { p(H -> HOLE:H):M.S }
        --      requires: H -> { HOLE:H.T }
        -- 2. Rename requirements, substituting HOLEs:
        --      provides: A -> { p(H -> HOLE:X):M.S }
        --      requires: X -> { HOLE:X.T }

        -- (after merge)
        -- provides: X -> { q():X.T }
        --           A -> { p(H -> q():X):M.S }
        -- requires: (nothing)
\end{verbatim}

\newpage

\subsection{Merging}

Merging combines two shapes, filling requirements with implementations
and substituting information we learn about the identities of
\verb|Name|s.  Importantly, merging is a \emph{directed} process, akin
to taking two boxes with input and output ports and wiring them up so
that the first box feeds into the second box.  This algorithm does not
support mutual recursion.

Suppose we are merging shape $p$ with shape $q$.  Merging proceeds as follows:

\begin{enumerate}
    \item \emph{Fill every requirement of $q$ with provided modules from
        $p$.} For each requirement $M$ of $q$ that is provided by $p$,
        substitute each \verb|Module| occurrence of \verb|HOLE:M| with the
        provided $p(M)$, merge the names, and remove the requirement from $q$.
    \item \emph{Merge in provided signatures of $q$, add the provided modules of $q$.}
        For each provision $M$ of $q$: if $q(M)$ is a hole, substitute every
        \verb|Module| occurrence of \verb|HOLE:|$q(M)$ with $p(M)$ if it exists and merge
        the names; otherwise, add it to $p$, erroring if $p(M)$ exists.
\end{enumerate}

Substitutions apply to both shapes.  To merge two sets of names, take
each pair of names with matching \verb|OccName|s $n$ and $m$.

\begin{enumerate}
    \item If both are from holes, pick a canonical representative $m$ and substitute $n$ with $m$. (E.g., pick the one with the lexicographically first \verb|ModName|).
    \item If one $n$ is from a hole, substitute $n$ with $m$.
    \item Otherwise, error if the names are not the same.
\end{enumerate}

It is important to note that substitutions on \verb|Module|s and substitutions on
\verb|Name|s are disjoint: a substitution from \verb|HOLE:A| to \verb|HOLE:B|
does \emph{not} substitute inside the name \verb|HOLE:A.T|.
Here is a simple example:

\begin{verbatim}
          shape 1                       shape 2
provides: A -> THIS:A { q():A.T }       M -> p(A -> HOLE:A) { HOLE:A.T, p(A -> HOLE:A).S }
requires: (nothing)                     A ->                { HOLE:A.T }

(after filling requirements)
provides: A -> THIS:A { q():A.T }       M -> p(A -> THIS:A) { q():A.T, p(A -> THIS:A).S }
requires: (nothing)                     (nothing)

(after adding provides)
provides: A -> THIS:A         { q():A.T }
          M -> p(A -> THIS:A) { q():A.T, p(A -> THIS:A).S }
requires: (nothing)
\end{verbatim}

Here are some more involved examples, which illustrate some important
cases:

\subsubsection{Sharing constraints}

Suppose you have two signature which both independently define a type,
and you would like to assert that these two types are the same.  In the
ML world, such a constraint is known as a sharing constraint.  Sharing
constraints can be encoded in Backpacks via clever use of reexports;
they are also an instructive example for signature merging.
For brevity, we've omitted \verb|provided| from the shapes in this example.

\begin{verbatim}
signature A(T) where
    data T
signature B(T) where
    data T

-- requires: A -> HOLE:A        { HOLE:A.T }
             B -> HOLE:B        { HOLE:B.T }

-- the sharing constraint!
signature A(T) where
    import B(T)
-- (shape to merge)
-- requires: A -> HOLE:A        { HOLE:B.T }

-- (after merge)
-- requires: A -> HOLE:A        { HOLE:A.T }
--           B -> HOLE:B        { HOLE:A.T }
\end{verbatim}

Notably, we could equivalently have chosen \verb|HOLE:B.T| as the post-merge
name.  \Red{Actually, I don't think any choice can be wrong. The point is to
ensure that the substitution applies to everything we know about, and since requirements
monotonically increase in size (or are filled), this will hold.}

\subsubsection{Provision linking does not discharge requirements}

It is not an error to define a module, and then define a signature
afterwards: this can be useful for checking if a module implements
a signature, and also for sharing constraints:

\begin{verbatim}
module M(T) where
    data T = T
signature S(T) where
    data T

signature M(T)
    import S(T)
-- (partial)
-- provides: S -> HOLE:S { THIS:M.T } -- resolved!

-- alternately:
signature S(T) where
    import M(T)
\end{verbatim}

However, in some circumstances, linking a signature to a module can cause an
unrelated requirement to be ``filled'':

\begin{verbatim}
package p (S) requires (S) where
    signature S where
        data T

package q (A) requires (B) where
    include S (S as A) requires (S as B)

package r where
    module A where
        data T = T
    include q (A) requires (B)
    -- provides: A -> THIS:A { THIS:A.T }
    -- requires: (nothing)
\end{verbatim}

Notice that the requirement was discharged because we unified \verb|HOLE:B|
with \verb|THIS:A|.  While this is certainly the most accurate picture
of the package we can get from this situation, it is a bit unsatisfactory
in that looking at the text of module \verb|r|, it is not obvious that
all the requirements were filled; only that there is some funny business
going on with multiple provisions with \verb|A|.

Note that we \emph{cannot} disallow multiple bindings to the same provision:
this is a very important use-case when you want to include one signature,
include another signature, and see the merge of the two signatures in your
context.  \Red{So maybe this is what we should do.}  However, there is
a saving grace, which is signature-signature linking can be done when
linking requirements; linking provisions is unnecessary in this case.
So perhaps the merge rule should be something like:

\begin{enumerate}
    \item \emph{Fill every requirement of $q$ with provided modules from
        $p$.} For each requirement $M$ of $q$ that is provided by $p$,
        substitute each \verb|Module| occurrence of \verb|HOLE:M| with the
        provided $p(M)$, merge the names, and remove the requirement from $q$.
    \item \emph{Merge requirements.}  For each requirement $M$ of $q$ that is not
        provided by $p$ but required by $p$, merge the names.
    \item \emph{Add provisions of $q$.} For each provision $M$ of $q$:
        add it to $p$, erroring if the addition is incompatible with an
        existing entry in $p$.
\end{enumerate}

Now, because there is no provision linking, and the requirement \verb|B| is
not linked against anything, \verb|A| ends up being incompatible with
the \verb|A| in context and is rejected.  We also reject situations where
a provision unification would require us to pick a signature:

\begin{verbatim}
package p (S) requires (S) where
    signature S

package q where
    include p (S) requires (S as A)
    include p (S) requires (S as B)
    -- rejected; provided S doesn't unify
    -- (if we accepted, what's the requirement? A? B?)
\end{verbatim}

\Red{How to relax this so hs-boot works}

\Red{Example of how loopy modules which rename requirements make it un-obvious whether or not
a requirement is still required.  Same example works declaration level.}

\Red{package p (A) requires (A); the input output ports should be the same}

% We figure out the requirements (because no loopy modules)
%
% package p (A, B) requires (B)
%   include base
%   sig B(T)
%       import Prelude(T)
%
% requirement example
%
% mental model: you start with an empty package, and you start accreting
% things on things, merging things together as you discover that this is
% the case.

\newpage

\subsection{Export declarations}

If an explicit export declaration is given, the final shape is the
computed shape, minus any provisions not mentioned in the list, with the
appropriate renaming applied to provisions and requirements.  (Provisions
are implicitly passed through if they are not named.)

If no explicit export declaration is given, the final shape is
the computed shape, minus any provisions which did not have an in-line
module or signature declaration.

\begin{aside}
\textbf{Guru meditation.}  The defaulting behavior for signatures
is slightly delicate, as can be seen in this example:

\begin{verbatim}
package p (S) requires (S) where
    signature S where
        x :: True

package q where
    include p
    signature S where
        y :: True
    module M where
        import S
        z = x && y      -- OK

package r where
    include q
    module N where
        import S
        z = y           -- OK
        z = x           -- ???
\end{verbatim}

Absent the second signature declaration in \verb|q|, \verb|S.x| clearly
should not be visible.  However, what ought to occur when this signature
declaration is added?  One interpretation is to say that only some
(but not all) declarations are provided (\verb|S.x| remains invisible);
another interpretation is that adding \verb|S| is enough to treat
the signature as ``in-line'', and all declarations are now provided
(\verb|S.x| is visible).

The latter interpretation avoids having to keep track of providedness
per declarations, and means that you can always express defaulting
behavior by writing an explicit provides declaration on the package.
However, it has the odd behavior of making empty signatures semantically
meaningful:

\begin{verbatim}
package q where
    include p
    signature S where
\end{verbatim}

Note that if \verb|p| didn't provide \verb|S|, \verb|x| would \emph{never}
be visible unless it was redeclared in an interface.
\end{aside}
%
%   SPJ: This would be too complicated (if there's yet a third way)

\subsection{Package key}

What is \verb|THIS|?  It is the package name, plus for every requirement \verb|M|,
a mapping \verb|M -> HOLE:M|.  Annoyingly, you don't know the full set of
requirements until the end of shaping, so you don't know the package key ahead of time;
however, it can be substituted at the end easily.

\newpage

\section{Type checking}

Type checking computes, for every \verb|Module|, a \verb|ModIface|
representing the type of the module in question:

\begin{verbatim}
Type ::= { Module "->" ModIface }
\end{verbatim}

\subsection{The basic plan}

Given a module or signature, we can type check given these two assumptions:

\begin{itemize}
    \item We have a renamed syntax tree, whose identifiers have been
          resolved as according to the result of the shaping pass.
    \item For any \verb|Name| in the renamed tree, the corresponding
          \verb|ModDetails| for the \verb|Module| has been loaded
          (or can be lazily loaded).
\end{itemize}

The result of type checking is a \verb|ModDetails| which can then be
converted into a \verb|ModIface|.
Arranging for these two assumptions to be true is the bulk of the
complexity of type checking.

\subsection{A little bit of night music}

A little bit of background about the relationship of GHC \verb|ModIface| and
\verb|ModDetails|.

A \verb|ModIface| corresponds to an interface file, it is essentially a
big pile of \verb|Name|s which have not been resolved to their locations
yet.  Once a \verb|ModIface| is loaded, we type check it
(\verb|tcIface|), which turns them into \verb|TyThing|s and \verb|Type|s
(linked up against their true locations.) Conversely, once we finish
type checking a module, we have a \verb|ModDetails|, which we then
serialize into a \verb|ModIface|.

One very important (non-obvious) distinction is that a \verb|ModDetails|
does \emph{not} contain the information for handling renaming.
(Actually, it does carry along a \verb|md_exports|, but this is only a
hack to transmit this information when we're creating an interface;
no code actually uses it.)  So any information about reexports is
recorded in the \verb|ModIface| and used by the renamer, at which point
we don't need it anymore and can drop it from \verb|ModDetails|.

\subsection{Loading modules from indefinite packages}

\paragraph{Everything is done modulo a shape}  Consider
this package:

\begin{verbatim}
package p where
    signature H(T) where
        data T = T
    module A(T) where
        data T = T
    signature H(T) where
        import A(T)

-- provides: A -> THIS:A { THIS:A.T }
--           H -> HOLE:H { THIS:A.T }
-- requires: H ->        { THIS:A.T }
\end{verbatim}

With this shaping information, when we are type-checking the first
signature for \verb|H|, it is completely wrong to try to create
a definition for \verb|HOLE:H.T|, since we know that it refers
to \verb|THIS:A.T| via the requirements of the shape.  This applies
even if \verb|H| is included from another package.  Thus, when
we are loading \verb|ModDetails| into memory, it is always done
\emph{with respect to some shaping}.  Whenever you reshape,
you must clear the module environment.

\paragraph{Figuring out where to consult for shape information}

For this example, let's suppose we have already type-checked
this package \verb|p|:

\begin{verbatim}
package p (A) requires (S) where
    signature S where
        data S
        data T
    module A(A) where
        import S
        data A = A S T
\end{verbatim}

giving us the following \verb|ModIface|s:

\begin{verbatim}
module HOLE:S.S where
    data S
    data T
module THIS:A where
    data A = A HOLE:S.S HOLE:S.T
-- where THIS = p(S -> HOLE:S)
\end{verbatim}

Next, we'd like to type check a package which includes \verb|p|:

\begin{verbatim}
package q (T, A, B) requires (H) where
    include p (A) requires (S as H)
    module T(T) where
        data T = T
    signature H(T) where
        import T(T)
    module B(B) where
        import A
        data B = B A
\end{verbatim}

%   package r where
%       include q
%       module H(S,T) where
%           import T(T)
%           data S = S
%       module C where
%           import A
%           import B
%           ...

Prior to typechecking, we compute its shape:

\begin{verbatim}
provides: (elided)
requires: H -> { HOLE:H.S, THIS:T.T }
-- where THIS = q(H -> HOLE:H)
\end{verbatim}

Our goal is to get the following type:

\begin{verbatim}
module THIS:T where
    data T = T
module THIS:B where
    data B = B p(S -> HOLE:H):A.A
        -- where data A = A HOLE:H.S THIS:T.T
-- where THIS = q(H -> HOLE:H)
\end{verbatim}

This type information does \emph{not} match the pre-existing
type information from \verb|p|: when we translate the \verb|ModIface| for
\verb|A| in the context into a \verb|ModDetails| from this typechecking,
we need to substitute \verb|Name|s and \verb|Module|s
as specified by shaping.  Specifically, when we load \verb|p(S -> HOLE:H):A|
to find out the type of \verb|p(S -> HOLE:H):A.A|,
we need to take \verb|HOLE:S.S| to \verb|HOLE:H.S| and \verb|HOLE:S.T| to \verb|THIS:T.T|.
In both cases, we can determine the right translation by looking at how \verb|S| is
instantiated in the package key for \verb|p| (it is instantiated with \verb|HOLE:H|),
and then consulting the shape in the requirements.

This process is done lazily, as we may not have typechecked the original
\verb|Name| in question when doing this.  \verb|hs-boot| considerations apply
if things are loopy: we have to treat the type abstractly and re-typecheck it
to the right type later.


\subsection{Re-renaming}

Theoretically, the cleanest way to do shaping and typechecking is to have shaping
result in a fully renamed syntax tree, which we then typecheck: when done this way,
we don't have to worry about logical contexts (i.e., what is in scope) because
shaping will already have complained if things were not in scope.

However, for practical purposes, it's better if we don't try to keep
around renamed syntax trees, because this could result in very large
memory use; additionally, whenever a substitution occurs, we would have
to substitute over all of the renamed syntax trees.  Thus, while
type-checking, we'll also re-compute what is in scope (i.e.,  just the
\verb|OccName| bits of \verb|provided|). Nota bene: we still use the
\verb|Name|s from the shape as the destinations of these
\verb|OccName|s!  Note that we can't just use the final shape, because
this may report more things in scope than we actually want.  (It's also
worth noting that if we could reduce the set of provided things in
scope in a single package, just the \verb|Shape| would not be enough.)

\subsection{Merging \texttt{ModDetails}}

After type-checking a signature, we may turn to add it to our module
environment and discover there is already an entry for it!  In that case,
we simply merge it with the existing entry, erroring if there are incompatible
entries.

\end{document}