Commit bbabb711 authored by Edward Z. Yang's avatar Edward Z. Yang

Updates to Backpack documentation based on recent visit to MSRC.

Includes lots of shaping examples, and a shaping algorithm description.
Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>
parent 72a92726
all: backpack-impl.pdf backpack-manual.pdf ubackpack.pdf
all: backpack-impl.pdf backpack-manual.pdf ubackpack.pdf backpack-shaping.pdf algorithm.pdf
ubackpack.pdf: ubackpack.tex
latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 ubackpack.tex || ! rm -f $@
......@@ -8,3 +8,9 @@ backpack-impl.pdf: backpack-impl.tex
backpack-manual.pdf: backpack-manual.tex
latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 backpack-manual.tex || ! rm -f $@
backpack-shaping.pdf: backpack-shaping.tex
latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 backpack-shaping.tex || ! rm -f $@
algorithm.pdf: algorithm.tex
latexmk -pdf -latexoption=-halt-on-error -latexoption=-file-line-error -latexoption=-synctex=1 algorithm.tex || ! rm -f $@
\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 } }
\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.
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}
\Red{Example of canonical choice for signature merging}
\Red{Example of how provides DO NOT merge}
\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}
(UNDER CONSTRUCTION)
%
% what do we know for each type checked package
% ModEnv
%
% ModIface -> ModDetails (rename + tcIface)
For type-checking, we assume that for every \verb|pkgname|, we have a mapping of \verb|ModName -> ModIface| (We distinguish \verb|ModIface| from the typechecked \verb|ModDetails|, which may have had \verb|HOLE|s renamed in the process.) We maintain a context of \verb|ModName -> Module| and \verb|Module -> ModDetails|
How to type-check a signature? Well, a signature has a \verb|Module|, but it's \emph{NOT} necessarily in the home package.
\subsection{Semantic objects}
\begin{verbatim}
PkgKey ::= SrcPkgId "(" { ModName "->" Module } ")"
| HOLE
Module ::= PkgKey ":" ModName
Name ::= Module "." OccName
OccName ::= -- a plain old name, e.g. undefined, Bool, Int
Shape ::= "provided:" { ModName "->" Module { Name } }
"required:" { ModName "->" { Name } }
Type ::= "shape:" Shape
"modenv:" { Module "->" ModIface }
\end{verbatim}
\begin{verbatim}
ModIface --- rename / tcIface ---> ModDetails
\end{verbatim}
A shape consists of the modules we provide (as well as what declarations
are provided), and what module names (with what declarations) must
be provided.
\subsection{Renamed packages}
\begin{verbatim}
spackage ::= "package" pkgname Shape "where" spkgbody
spkgbody ::= "{" spkgdecl_0 ";" ... ";" spkgdecl_n "}"
spkgdecl ::= "module" Module (rnexports) where rnbody
| "signature" Module (rnexports) where rnbody
| "include" pkgname sinclspec
sinclspec ::= "(" srenaming_0 "," ... "," srenaming_n ")"
"requires" "(" srenaming_0 "," ... "," srenaming_n ")"
srenaming ::= ModName "as" Module
\end{verbatim}
After shaping, we have renamed all of the identifiers inside a package.
Here is the elaborated version. This is now immediately ready for
type-checking. \Red{Representation is slightly redundant.}
\end{document}
......@@ -2436,6 +2436,33 @@ while it might be aesthetically displeasing to have the signature impose
extra restrictions on linking identities, we can carry this out without
violating the linking restriction.
\subsection{Orphans}
Controlling instance visibility via signature problems poses an implementation
challenge similar to that of orphan instances. To describe this problem,
we first have to describe how instance resolution works for orphans and
non-orphans in GHC today.
Type information for already compiled code in other packages is cached
on disk using interface files. For efficiency reasons, it's desirable to
avoid loading interface file until absolutely necessary: if we don't
use any of the identifiers for a file, it should not be necessary to
load the interface. Among other things, type class instances are stored
in interface files.
Signatures and hs-boot files notwithstanding, non-orphan instance
resolution is achieved through a (somewhat) astonishing coincidence: at
the point when a type class is resolved, we are guaranteed to have
loaded the interfaces for all of the names involved in the type class
instantiation. This means that if there is a type class, we will have
seen it; conversely, it means that non-orphan instances are a closed
world: if we load all these interfaces and see no non-orphan instance,
we know there never be a non-orphan instance.
Things are a bit worse for orphans: these instances are an open world,
and so the only way to tell if an orphan instance is in scope is by consulting
the transitive closure of module imports.
\section{Bits and bobs}
\subsection{Abstract type synonyms}
......
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment