algorithm.tex 28.9 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
\documentclass{article}

\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}
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
\usepackage{framed}

% Alter some LaTeX defaults for better treatment of figures:
% See p.105 of "TeX Unbound" for suggested values.
% See pp. 199-200 of Lamport's "LaTeX" book for details.
%   General parameters, for ALL pages:
\renewcommand{\topfraction}{0.9}	% max fraction of floats at top
\renewcommand{\bottomfraction}{0.8}	% max fraction of floats at bottom
%   Parameters for TEXT pages (not float pages):
\setcounter{topnumber}{2}
\setcounter{bottomnumber}{2}
\setcounter{totalnumber}{4}     % 2 may work better
\setcounter{dbltopnumber}{2}    % for 2-column pages
\renewcommand{\dbltopfraction}{0.9}	% fit big float above 2-col. text
\renewcommand{\textfraction}{0.07}	% allow minimal text w. figs
%   Parameters for FLOAT pages (not text pages):
\renewcommand{\floatpagefraction}{0.7}	% require fuller float pages
% N.B.: floatpagefraction MUST be less than topfraction !!
\renewcommand{\dblfloatpagefraction}{0.7}	% require fuller float pages

% remember to use [htp] or [htpb] for placement


\newcommand{\optionrule}{\noindent\rule{1.0\textwidth}{0.75pt}}
42 43

\newenvironment{aside}
44 45 46
  {\begin{figure}\def\FrameCommand{\hspace{2em}}
   \MakeFramed {\advance\hsize-\width}\optionrule\small}
{\par\vskip-\smallskipamount\optionrule\endMakeFramed\end{figure}}
47 48 49 50 51 52 53 54 55 56 57 58 59 60

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

61 62 63 64 65 66 67 68 69
\section{Changelog}

\paragraph{April 28, 2015}  A signatures declaration no longer provides
a signature in the technical shaping sense; the motivation for this change
is explained in \textbf{Signatures cannot be provided}.  This means that,
by default, all requirements are importable (Derek has stated that he doesn't
think this will be too much of a problem in practice); we can consider extensions
which allow us to hide requirements from import.

70 71
\section{Front-end syntax}

72
\begin{figure}[htpb]
73 74 75 76 77 78 79 80 81 82 83 84 85 86
$$
\begin{array}{rcll}
p,q,r && \mbox{Package names} \\
m,n   && \mbox{Module names} \\[1em]
\multicolumn{3}{l}{\mbox{\bf Packages}} \\
  pkg & ::= & \verb|package|\; p\; [provreq]\; \verb|where {| d_1 \verb|;| \ldots \verb|;| d_n \verb|}| \\[1em]
\multicolumn{3}{l}{\mbox{\bf Declarations}} \\
  d & ::= & \verb|module|\;    m \; [exports]\; \verb|where|\; body \\
    & |   & \verb|signature|\; m \; [exports]\; \verb|where|\; body \\
    & |   & \verb|include|\; p \; [provreq] \\[1em]
\multicolumn{3}{l}{\mbox{\bf Provides/requires specification}} \\
provreq & ::= & \verb|(| \, rns \, \verb|)| \; 
        [ \verb|requires(|\, rns \, \verb|)| ] \\
rns & ::= & rn_0 \verb|,| \, \ldots \verb|,| \, rn_n [\verb|,|] & \mbox{Renamings} \\
87
rn & ::= & m\; \verb|as| \; n & \mbox{Renaming} \\[1em] 
88 89 90 91 92 93 94
\multicolumn{3}{l}{\mbox{\bf Haskell code}} \\
exports & & \mbox{A Haskell module export list} \\
body    & & \mbox{A Haskell module body} \\
\end{array}
$$
\caption{Syntax of Backpack} \label{fig:syntax}
\end{figure}
95

96
The syntax of Backpack is given in Figure~\ref{fig:syntax}.
97 98
See the ``Backpack manual'' for more explanation about the syntax.  It
is slightly simplified here by removing any constructs which are easily implemented as
99
syntactic sugar (e.g., a bare $m$ in a renaming is simply $m\; \verb|as|\; m$.)
100

101
\newpage
102 103
\section{Shaping}

104 105 106 107 108 109 110 111 112 113 114 115 116
\begin{figure}[htpb]
$$
\begin{array}{rcll}
Shape & ::= & \verb|provides:|\; m \; \verb|->|\; Module\; \verb|{|\, Name \verb|,|\, \ldots \, \verb|};| \ldots \\
      &     & \verb|requires:| \; m \; \verb|->|\; \textcolor{white}{Module}\; \verb|{| \, Name \verb|,| \, \ldots \, \verb|}| \verb|;| \ldots \\
PkgKey & ::= & p \verb|(| \, m \; \verb|->| \; Module \verb|,|\, \ldots\, \verb|)| \\
Module & ::= & PkgKey \verb|:| m \\
Name   & ::= & Module \verb|.| OccName \\
OccName & & \mbox{Unqualified name in a namespace}
\end{array}
$$
\caption{Semantic entities in Backpack} \label{fig:semantic}
\end{figure}
117

118
Shaping computes a $Shape$, whose form is described in Figure~\ref{fig:semantic}.
119 120 121 122 123 124 125
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.

126 127 128 129 130 131 132
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.

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

136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
\begin{aside}
\textbf{\texttt{OccName} is implied by \texttt{Name}.}
In Haskell, the following is not valid syntax:

\begin{verbatim}
    import A (foobar as baz)
\end{verbatim}
In particular, a \verb|Name| which is in scope will always have the same
\verb|OccName| (even if it may be qualified.)  You might imagine relaxing
this restriction so that declarations can be used under different \verb|OccName|s;
in such a world, we need a different definition of shape:

\begin{verbatim}
    Shape ::=
        provided: ModName -> { OccName -> Name }
        required: ModName -> { OccName -> Name }
\end{verbatim}
Presently, however, such an \verb|OccName| annotation would be redundant: it can be inferred from the \verb|Name|.
\end{aside}

\begin{aside}
\textbf{Holes of a package are a mapping, not a set.} Why can't the \verb|PkgKey| just record a
set of \verb|Module|s, e.g. \verb|PkgKey ::= SrcPkgKey { Module }|?  Consider:

\begin{verbatim}
    package p (A) requires (H1, H2) where
        signature H1(T) where
            data T
        signature H2(T) where
            data T
        module A(A(..)) where
            import qualified H1
            import qualified H2
            data A = A H1.T H2.T

    package q (A12, A21) where
        module I1(T) where
            data T = T Int
        module I2(T) where
            data T = T Bool
        include p (A as A12) requires (H1 as I1, H2 as I2)
        include p (A as A21) requires (H1 as I2, H2 as I1)
\end{verbatim}
With a mapping, the first instance of \verb|p| has key \verb|p(H1 -> q():I1, H2 -> q():I2)|
while the second instance has key \verb|p(H1 -> q():I2, H2 -> q():I1)|; with
a set, both would have the key \verb|p(q():I1, q():I2)|.
\end{aside}


\begin{aside}
\textbf{Signatures can require a specific entity.}
With requirements like \verb|A -> { HOLE:A.T, HOLE:A.foo }|,
why not specify it as \verb|A -> { T, foo }|,
e.g., \verb|required: { ModName -> { OccName } }|?  Consider:

\begin{verbatim}
    package p () requires (A, B) where
        signature A(T) where
            data T
        signature B(T) where
            import T
\end{verbatim}
The requirements of this package specify that \verb|A.T| $=$ \verb|B.T|; this
can be expressed with \verb|Name|s as

\begin{verbatim}
    A -> { HOLE:A.T }
    B -> { HOLE:A.T }
\end{verbatim}
But, without \verb|Name|s, the sharing constraint is impossible:  \verb|A -> { T }; B -> { T }|. (NB: \verb|A| and \verb|B| don't have to be implemented with the same module.)
\end{aside}

\begin{aside}
\textbf{The \texttt{Name} of a value is used to avoid
ambiguous identifier errors.}  We state that two types
are equal when their \texttt{Name}s are the same; however,
for values, it is less clear why we care.  But consider this example:

\begin{verbatim}
    package p (A) requires (H1, H2) where
        signature H1(x) where
            x :: Int
        signature H2(x) where
            import H1(x)
        module A(y) where
            import H1
            import H2
            y = x
\end{verbatim}
The reference to \verb|x| in \verb|A| is unambiguous, because it is known
that \verb|x| from \verb|H1| and \verb|x| from \verb|H2| are the same (have
the same \verb|Name|.)  If they were not the same, it would be ambiguous and
should cause an error.  Knowing the \verb|Name| of a value distinguishes
between these two cases.
\end{aside}

\begin{aside}
\textbf{Absence of \texttt{Module} in \texttt{requires} implies holes are linear}
Because the requirements do not record a \verb|Module| representing
the identity of a requirement, it means that it's not possible to assert
that hole \verb|A| and hole \verb|B| should be implemented with the same module,
as might occur with aliasing:

\begin{verbatim}
    signature A where
    signature B where
    alias A = B
\end{verbatim}
%
The benefit of this restriction is that when a requirement is filled,
it is obvious that this is the only requirement that is filled: you won't
magically cause some other requirements to be filled.  The downside is
it's not possible to write a package which looks for an interface it is
looking for in one of $n$ names, accepting any name as an acceptable linkage.
If aliasing was allowed, we'd need a separate physical shaping context,
to make sure multiple mentions of the same hole were consistent.

\end{aside}

%\newpage
256 257 258

\subsection{\texttt{module M}}

259 260
A module declaration provides a module \verb|THIS:M| at module name \verb|M|. It
has the shape:
261 262

\begin{verbatim}
263
    provides: M -> THIS:M { exports of renamed M }
264 265
    requires: (nothing)
\end{verbatim}
266
Example:
267 268 269 270 271 272 273 274 275 276 277 278

\begin{verbatim}
    module A(T) where
        data T = T

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

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

279
A signature declaration creates a requirement at module name \verb|M|.  It has the shape:
280 281

\begin{verbatim}
282
    provides: (nothing)
283
    requires: M -> { exports of renamed M }
284 285 286 287 288 289 290 291
\end{verbatim}

\noindent Example:

\begin{verbatim}
    signature H(T) where
        data T

292 293 294
    -- provides: H -> (nothing)
    -- requires: H -> { HOLE:H.T }
\end{verbatim}
295

296 297 298 299 300 301 302
\begin{aside}
\textbf{Signatures cannot be provided}.  A signature \emph{never} counts
as a provision, as far as shaping is concerned.  While it seems like
a signature package which provides signatures for import should actually,
you know, \emph{provide} its signatures, this observation at its
logical conclusion is a mess.  The problem can most clearly be
seen in this example:
303

304 305 306 307
\begin{verbatim}
    package a-sigs (A) requires (A) where -- ***
        signature A where
            data T
308

309 310 311 312 313 314
    package a-user (B) requires (A) where
        signature A where
            data T
            x :: T
        module B where
            ...
315

316 317 318
    package p where
        include a-sigs
        include a-user
319
\end{verbatim}
320 321 322 323 324 325 326 327
%
When we consider merging in the shape of \verb|a-user|, does the
\verb|A| provided by \verb|a-sigs| fill in the \verb|A| requirement
in \verb|a-user|?  It \emph{should not}, since \verb|a-sigs| does not
actually provide enough declarations to satisfy \verb|a-user|'s
requirement: the intended semantics \emph{merges} the requirements
of \verb|a-sigs| and \verb|a-user|, but doesn't use the provision to
fill the signature.  However, in this case:
328

329 330 331 332 333 334 335 336 337
\begin{verbatim}
    package a-sigs (M as A) requires (H as A) where
        signature H(T) where
            data T
        module M(T) where
            import H(T)
\end{verbatim}
%
We rightly should error, since the provision is a module. And in this situation:
338

339 340 341 342 343 344 345 346
\begin{verbatim}
    package a-sigs (H as A) requires (H) where
        signature H(T) where
            data T
\end{verbatim}
%
The requirements should be merged, but should the merged requirement
be under the name \verb|H| or \verb|A|?
347

348 349 350 351 352 353 354
It may still be possible to use the \verb|(A) requires (A)| syntax to
indicate exposed signatures, but this would be a mere syntactic
alternative to \verb|() requires (exposed A)|.
\end{aside}
%

\newpage
355 356 357 358 359 360 361 362
\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
363
          be thinned, so non-mentioned requirements are implicitly passed through.)
364 365 366 367
          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.
\end{itemize}
368 369 370
%
If there are no thinnings/renamings, you just merge the
shape unchanged! Here is an example:
371 372 373 374 375 376 377 378 379 380 381 382

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

    package q (A) where
        module X where
            data T = T
383 384 385 386
        include p (M as A) requires (H as X)
\end{verbatim}
%
The shape of package \verb|p| is:
387

388 389 390 391 392 393 394 395 396
\begin{verbatim}
    requires: M -> { p(H -> HOLE:H):M.S }
    provides: H -> { HOLE:H.T }
\end{verbatim}
%
Thus, when we process the \verb|include| in package \verb|q|,
we make the following two changes: we rename the provisions,
and we rename the requirements, substituting \verb|HOLE|s.
The resulting shape to be merged in is:
397

398 399 400 401 402 403 404 405 406 407 408
\begin{verbatim}
    provides: A -> { p(H -> HOLE:X):M.S }
    requires: X -> { HOLE:X.T }
\end{verbatim}
%
After merging this in, the final shape of \verb|q| is:

\begin{verbatim}
    provides: X -> { q():X.T }              -- from shaping 'module X'
              A -> { p(H -> q():X):M.S }
    requires: (nothing)                     -- discharged by provided X
409 410 411 412 413 414
\end{verbatim}

\newpage

\subsection{Merging}

415 416 417 418 419 420 421 422 423 424 425 426 427
The shapes we've given for individual declarations have been quite
simple.  Merging combines two shapes, filling requirements with
implementations and substituting information we learn about the
identities of \verb|Name|s; it is the most complicated part of the
shaping process.

The best way to think about merging is that we take two packages with
inputs (requirements) and outputs (provisions) and ``wiring'' them up so
that outputs feed into inputs.  In the absence
of mutual recursion, this wiring process is \emph{directed}: the provisions
of the first package feed into the requirements of the second package,
but never vice versa.  (With mutual recursion, things can go in the opposite
direction as well.)
428

429 430
Suppose we are merging shape $p$ with shape $q$ (e.g., $p; q$).  Merging
proceeds as follows:
431 432 433

\begin{enumerate}
    \item \emph{Fill every requirement of $q$ with provided modules from
434 435
        $p$.} For each requirement $M$ of $q$ that is provided by $p$ (in particular,
        all of its required \verb|Name|s are provided),
436 437
        substitute each \verb|Module| occurrence of \verb|HOLE:M| with the
        provided $p(M)$, merge the names, and remove the requirement from $q$.
438 439 440 441 442 443 444
        Error if a provision is insufficient for the requirement.
    \item If mutual recursion is supported, \emph{fill every requirement of $p$ with provided modules from $q$.}
    \item \emph{Merge leftover requirements.}  For each requirement $M$ of $q$ that is not
        provided by $p$ but required by $p$, merge the names.  (It's not
        necessary to substitute \verb|Module|s, since they are guaranteed to be the same.)
    \item \emph{Add provisions of $q$.} Union the provisions of $p$ and $q$, erroring
        if there is a duplicate that doesn't have the same identity.
445
\end{enumerate}
446 447
%
To merge two sets of names, take each pair of names with matching \verb|OccName|s $n$ and $m$.
448 449

\begin{enumerate}
450
    \item If both are from holes, pick a canonical representative $m$ and substitute $n$ with $m$.
451 452 453
    \item If one $n$ is from a hole, substitute $n$ with $m$.
    \item Otherwise, error if the names are not the same.
\end{enumerate}
454
%
455 456 457
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|.
458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482

Since merging is the most complicated step of shaping, here are a big
pile of examples of it in action.

\subsubsection{A simple example}

In the following set of packages:

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

    package q where
        module A where
            data T = T
        include p
\end{verbatim}

When we \verb|include p|, we need to merge the partial shape
of \verb|q| (with just provides \verb|A|) with the shape
of \verb|p|.  Here is each step of the merging process:
483 484 485

\begin{verbatim}
          shape 1                       shape 2
486 487
          --------------------------------------------------------------------------------
(initial shapes)
488 489 490 491 492 493 494 495 496 497 498 499 500
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}

501
Notice that we substituted \verb|HOLE:A| with \verb|THIS:A|, but \verb|HOLE:A.T| with \verb|q():A.T|.
502

503
\subsubsection{Requirements merging can affect provisions}
504

505 506
When a merge results in a substitution, we substitute over both
requirements and provisions:
507 508

\begin{verbatim}
509 510 511 512 513 514
    signature H(T) where
        data T
    module A(T) where
        import H(T)
    module B(T) where
        data T = T
515

516 517 518
    -- provides: A -> THIS:A { HOLE:H.T }
    --           B -> THIS:B { THIS:B.T }
    -- requires: H ->        { HOLE:H.T }
519

520 521 522
    signature H(T, f) where
        import B(T)
        f :: a -> a
523

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

529 530 531 532 533 534 535
\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.
536 537

\begin{verbatim}
538 539 540
    signature A(T) where
        data T
    signature B(T) where
541 542
        data T

543 544
    -- requires: A -> { HOLE:A.T }
                 B -> { HOLE:B.T }
545

546 547 548 549 550
    -- the sharing constraint!
    signature A(T) where
        import B(T)
    -- (shape to merge)
    -- requires: A -> { HOLE:B.T }
551

552 553 554 555 556 557 558
    -- (after merge)
    -- requires: A -> { HOLE:A.T }
    --           B -> { HOLE:A.T }
\end{verbatim}
%
\Red{I'm pretty sure any choice of \texttt{Name} is OK, since the
subsequent substitution will make it alpha-equivalent.}
559

560
%   \subsubsection{Leaky requirements}
561

562 563
%   Both requirements and provisions can be imported, but requirements
%   are always available
564

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

567 568
%\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.}
569

570
%\Red{package p (A) requires (A); the input output ports should be the same}
571 572 573 574 575 576 577 578 579 580 581 582 583 584

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

585
%\newpage
586 587 588 589 590

\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
591
appropriate renaming applied to provisions and requirements.  (Requirements
592 593
are implicitly passed through if they are not named.)
If no explicit export declaration is given, the final shape is
594 595
the computed shape, including only provisions which were defined
in the declarations of the package.
596 597

\begin{aside}
598 599 600 601 602 603 604 605 606 607 608
\textbf{Signature visibility, and defaulting}
The simplest formulation of requirements is to have them always be
visible.  Signature visibility could be controlled by associating
every requirement with a flag indicating if it is importable or
not: a signature declaration sets a requirement to be visible, and
an explicit export list can specify if a requirement is to be visible
or not.

When an export list is absent, we have to pick a default visibility
for a signature.  If we use the same behavior as with modules,
a strange situation can occur:
609 610

\begin{verbatim}
611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
    package p where -- S is visible
        signature S where
            x :: True

    package q where -- use defaulting
        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           -- ???
629
\end{verbatim}
630
%
631
Absent the second signature declaration in \verb|q|, \verb|S.x| clearly
632
should not be visible in \verb|N|.  However, what ought to occur when this signature
633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660
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}
\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.

661
%\newpage
662 663 664

\section{Type checking}

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

668 669 670
\begin{verbatim}
Type ::= { Module "->" ModIface }
\end{verbatim}
671

672
\subsection{The basic plan}
673

674 675 676 677 678 679 680 681 682
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}
683

684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713
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:
714 715

\begin{verbatim}
716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751
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}
752

753 754 755 756 757 758 759 760 761
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)
762 763
\end{verbatim}

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

766
\begin{verbatim}
767 768 769 770 771 772 773 774 775
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
776 777
\end{verbatim}

778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794
%   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}
795

796
Our goal is to get the following type:
797 798

\begin{verbatim}
799 800 801 802 803 804
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)
805 806
\end{verbatim}

807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848
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.
849 850

\end{document}