summaryrefslogtreecommitdiff
path: root/docs/backpack/backpack-manual.tex
blob: 89826789a5659407269b1b647c75678b9ee736c2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
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
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
\documentclass{article}

\usepackage{color}
\usepackage{fullpage}
\usepackage{hyperref}

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

\title{The Backpack Manual}

\begin{document}

\maketitle

Backpack is a new module system for Haskell, intended to enable
``separate modular development'': a style of development where
application-writers can develop against abstract interfaces or
\emph{signatures}, while separately library-writers write software which
implement these interfaces.  Backpack was originally described in a
POPL'14 paper \url{http://plv.mpi-sws.org/backpack/}, but the point of
this document is to describe the syntax of a language you might actually
be able to \emph{write}, as well as describe some of the changes to the
design we've made since this paper.

\paragraph{Examples}

Before we dive in, here are some examples of Backpack files to whet
your appetite:

\begin{verbatim}
package p(A) where
    module A(a) where
        a = True

package q(B, C) where
    include p
    module B(b) where
        import A
        b = a
    module C(c) where
        import B
        c = b
\end{verbatim}

In this example package \verb|p| exports a single module \verb|A|; package \verb|q| exports
two modules, and includes package \verb|p| so that its modules are in
scope.  The form of a \verb|package| and a \verb|module| are quite similar:
a package can express an explicit export list of modules in much the same
way a module exports identifiers. \\

Here is a more complicated Backpack file taking advantage of the availability
of signatures in Backpack.  This example omits the actual module bodies: GHC
will automatically look for them in appropriate files (e.g. \verb|p/Map.hsig|,
\verb|p/P/Types.hs|, \verb|p/P.hs|, \verb|q/QMap.hs| and \verb|q/Q.hs|).

\begin{verbatim}
package p (P) requires (Map) where
    include base
    signature Map
    module P.Types
    module P

package q (Q) where
    include base
    module QMap
    include p (P) requires (Map as QMap)
    module Q
\end{verbatim}

Package \verb|p| provides a module \verb|P|, but it also \emph{requires}
a module \verb|Map| (which must fulfill the specification described
in \verb|signature Map|).  This makes it an \emph{indefinite package}:
a package which isn't fully implemented, and cannot be compiled into
executable code until its ``hole'' (\verb|Map|) is filled.
It also sports an internal module named \verb|P.Types| which
is missing from the export list, and thus not exported.

Package \verb|q|, on the other hand, is a \emph{definite package}; as it
has no requirements, it can be compiled.  When it includes \verb|p|
into scope, it also fills the \verb|Map| requirement with an
implementation \verb|QMap|.

\section{The Backpack file}

\begin{verbatim}
packages ::= "{" package_0 ";" ... ";" package_n "}"
\end{verbatim}

A Backpack file consists of a list of named packages.
All packages in a Backpack file live in the global namespace.
A package defines a collection of modules, exporting some of
these modules so that other modules can make use of them via
\emph{include}.  You can compile a definite package \verb|p| in a Backpack file \verb|foo.bkp|
with \verb|ghc --backpack foo.bkp p|; you can type-check an indefinite package by
adding \verb|-fno-code|.

\Red{ToDo: How do you import an external Backpack file?}

\Red{ToDo: Facility for private packages.}

\begin{verbatim}
package ::= "package" pkgname [pkgexports] "where" pkgbody
pkgname ::= /* package name, e.g. containers (no version!) */
pkgbody ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
\end{verbatim}

A package begins with the keyword \verb|package|, its name, and an
optional export specification (e.g., a list of modules to be exposed).
The header is followed a list of declarations which define modules,
signatures and include other packages.

\section{Declarations}

\begin{verbatim}
pkgdecl ::= "module"    modid [exports] "where" body
          | "signature" modid [exports] "where" body
          | "include"   pkgname ["as" pkgname] [inclspec]
\end{verbatim}

A package is made up of package declarations, which either introduce a
new module implementation, introduces a new module
signature, or includes a package from the package environment.
The declaration of modules and signatures is exactly as it is in Haskell98,
so we don't reprise the grammar here.

\Red{ToDo: Clarify whether order matters.  Both are valid designs, but I think order-less is more user-friendly.}

We generally don't expect users to place their module source code
in package files; thus we provide the following forms to refer to
\verb|hs| and \verb|hsig| files living on the file-system:

\begin{verbatim}
pkgdecl ::= "module"    modid_0 "=" path_0 "," ... "," modid_n "=" path_n
          | "signature" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
          | "module"    modid_0 "," ... "," modid_n
          | "signature" modid_0 "," ... "," modid_n
\end{verbatim}

Thus, \verb|module A = "A.hs"| defines the body of \verb|A| based
on the contents of \verb|A.hs| in the package's source directory.
When the assignment is omitted, we implicitly refer to the file path
created by replacing periods with directory separators and adding
an appropriate file extension (thus, we can also write \verb|module A|).

\begin{verbatim}
pkgdecl ::= "source" path
\end{verbatim}

The \verb|source| keyword is another construct which allows us to
define modules by simply scanning the path in question.  For example,
if \verb|src| contains two files, \verb|A.hs| and \verb|B.hsig|,
then ``\verb|source "src"|'' is equivalent to
``\verb|module A = "src/A.hs"; signature B = "src/B.hsig"|''.

\Red{ToDo: Allow defining package-wide module imports, which propagate to all inline
modules and signatures.}

\Red{ToDo: Allow defining anonymous modules with bare type/expression declarations.}

\section{Signatures}

A signature, denoted with \verb|signature| in a Backpack file and a file
with the \verb|hsig| extension on the file system, represents a (type) signature for a
Haskell module. It can contain type signatures, data declarations, type
classes, type class instances and reexports(!), but it cannot contain any
value definitions.\footnote{Signatures are the backbone of the Backpack
module system.  A signature can be used to type-check client code which
uses a module (without the module implementation), or to verify that an
implementation upholds some signature (without a client
implementation.)} Signatures are essentially
\texttt{hs-boot} modules which do not support mutual recursion but
have no runtime efficiency cost.  Here is an example of a module signature
representing an abstract map type:

\begin{verbatim}
module Map where
    type role Map nominal representational
    data Map k v
    instance Functor (Map k)
    empty :: Map k a
\end{verbatim}

\section{Includes and exports}

\begin{verbatim}
pkgdecl  ::= "include" pkgname ["as" pkgname] [inclspec]

inclspec ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
             [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]

renaming ::= modid [ "as" modid ]
           | "package" pkgname
\end{verbatim}

% Add me later:
%          | "hiding" "(" modid_0 "," ... "," modid_n [","] ")"

An include brings the modules and signatures of a package into scope.
If these modules/signatures have the same names as other
modules/signatures in scope, \emph{mix-in linking} occurs.
In particular:

\begin{itemize}
    \item Module + module = error (unless they really are the same!)
    \item Module + signature = the signature is filled in, and is
        no longer part of the requirements of the package.
    \item Signature + signature = the signatures are merged together.
\end{itemize}

An include is associated with an optional \verb|inclspec|,
which can be to thin the provided modules and rename the provided and
required modules of an include.  In its simplest mode of use,
an \verb|inclspec| is a list of modules to be brought into scope,
e.g. \verb|include p (A, B)|.  Requirements cannot be hidden, but
they can be renamed to provide an implementation (or even to just
reexport the requirement under another name.)  If a requirement is
not mentioned in an explicit requirements list, it is implicitly included
(thus, \verb|requires (Hole)| has only a purely documentary effect).
It is not valid to rename a provision to a requirement, or a requirement
to a provision.

\begin{verbatim}
pkgexports ::= inclspec
\end{verbatim}

An export, symmetrically, specifies what modules a package will bring
into scope if it is included without any \verb|inclspec|.  Any module
which is omitted from an explicit export list is not exposed (however,
like before, requirements cannot be hidden.)

When an explicit export list is omitted, you can calculate the provides
and requires of a package as follows:

\begin{itemize}
    \item A package provides any non-included modules and signatures.
        (It only provides an included module/signature if it is explicitly
        reexported.)
    \item A package requires any transitively reachable signatures or
        hole signatures which are not filled in with an implementation.
\end{itemize}

\Red{ToDo: Properly describe ``hole signatures'' in the declarations section}

\subsection{Requirements}

The fact that requirements are \emph{implicitly} propagated from package
to package can result in some spooky ``action at a distance''. However,
this implicit behavior is one of the key ingredients to making mix-in
modular development scale: you don't want to have to explicitly link
everything up, as you might have to do in a traditional ML module
system.

You cannot, however, import a requirement, unless it is also provided,
which helps increase encapsulation.  If a package provides a
module, it can be imported:

\begin{verbatim}
package p (A) requires (A) where
    signature A where
        x :: Bool
package q (B) requires (A) where
    include p
    module B where
        import A    -- OK
\end{verbatim}

If it does not, it cannot be imported:
\Red{Alternately, the import is OK but doesn't result in any identifiers
being brought into scope.}

\begin{verbatim}
package p () requires (A) where -- yes, this is kind of pointless
    signature A where
        x :: Bool
package q (B) requires (A) where
    include p
    module B where
        import A    -- ERROR!
\end{verbatim}

This means that it is always safe for a package to remove requirements
or weaken holes; clients will always continue to compile.

Of course, if there is a different signature for the hole in scope, the
import is not an error; however, no declarations from \verb|p| are in scope:

\begin{verbatim}
package p () requires (A) where
    signature A where
        x :: Bool
package q (B) requires (A) where
    include p
    signature A where
        y :: Bool
    module B where
        import A
        x' = x      -- ERROR!
        y' = y      -- OK
\end{verbatim}

To summarize, requirements are part of the interface of a package; however,
they provide no identifiers as far as imports are concerned.  \Red{There is
some subtle interaction with requirements and shaping; see Shaping by example
for more details.}

\subsection{Package includes/exports}

A package export is easy enough to explain by analogy of module exports
in Haskell: a \verb|package p| in an export list explicitly reexports
the identifiers from that package; whereas even a default, wildcard export
list would only export locally defined identifiers/modules.

For example, this module exports the modules of both \verb|base|
and \verb|array|.

\begin{verbatim}
package combined(package base, package array) where
    include base
    include array
\end{verbatim}

However, in Backpack, a package may be included multiple times, making
such declarations ambiguous.  Thus, a package can be included as a local
package name to disambiguate:

\begin{verbatim}
package p(package q1) where         -- equivalent to B1
    include impls (A1, A2)
    include q as q1 (hole A as A1, B as B1)
    include q as q2 (hole A as A2, B as B2)
\end{verbatim}

A package include, e.g. \verb|include a (package p)| is only valid if
\verb|a| exports the package \verb|p| explicitly.\footnote{It's probably
possible to use anonymous packages to allow easily dividing a package
into subpackages, but this is silly and you can always just put it
in an actual package.}

\section{(Transparent) signature ascription}

\begin{verbatim}
inclspec ::= ...
           | "::" pkgexp

pkgexp ::= pkgname
         | "package" [exports] "where" pkgbody
\end{verbatim}

Signature ascription subsumes thinning: it narrows the exports
of modules in a package to those specified by a signature
package. This package \verb|pkgexp| is specified with either
a reference to a named package or an \emph{anonymous package}
(in prior work, these have been referred to as \emph{units},
although here the distinction is not necessary as our system
is \emph{purely applicative}).

Ascription also imposes a \emph{requirement} on the package
being abscribed.  Suppose you have \verb|p :: psig|, then:

\begin{itemize}
    \item Everything provided \verb|psig| must also
    be provided by \verb|p|.
    \item Everything required by \verb|p| must also
    be required by \verb|psig|.
\end{itemize}

\Red{Alternately, the second requirement is not necessary, and you
calculate the new requirements by taking the requirements of \texttt{psig},
removing the provides of \texttt{p}, and then adding the requirements of \texttt{p}.
This makes it possible to ascribe includes for \emph{adapter} packages, which
provide some modules given a different set of requirements.}

Semantically, ascription replaces the module with a signature,
type-checks the package against the signature, and then \emph{post
facto} links the signature against the implementation.
An ascribed include can be replaced with the signature
it is ascribed with, resulting in a package which still typechecks
but has more holes.  \Red{You have to link at the VERY END, because
if you link immediately after processing the module with the
ascribed include, the module identities will leak.  Of course, if
we're compiling we just link eagerly.  But now this means that
if you have a definite package which uses ascription, even assuming
all packages in the environment type-check, you must still type-check
this package twice, once indefinitely and then with the actual
linking relationship.}

For example, ascription in the export specification thins out all
private identifiers from the package:

\begin{verbatim}
    package psig where
        signature A where
            public :: Bool
    package p :: psig where
        module A.Internal where
            not_exported = 0
        module A where
            public = True
            private = False
\end{verbatim}

and, symmetrically, ascription in an include hides identifiers:

\begin{verbatim}
    package psig where
        signature A where
            public :: Bool
    package p where
        module A where
            public = True
            private = False
    package q where
        include p :: psig
        module B where
            import A
            ... public ...  -- OK
            ... private ... -- ERROR
\end{verbatim}

\Red{OBSERVATION: thinning is subsumed by transparent signature ascription, but NOT renaming.  Thus RENAMING does not commute across signature ascription; you must do it either before or after.  Syntax for this is tricky.}

\paragraph{Syntactic sugar for anonymous packages}

\begin{verbatim}
pkgexp ::= pkgbody
         | path
\end{verbatim}

It may be useful to provide two forms of sugar for specifying anonymous packages:
\verb|pkgbody| is equivalent to \verb|package where pkgbody|; and \verb|"path"|
is equivalent to \verb|package where source "path"|.

\appendix
\section{Full grammar}

\begin{verbatim}
packages ::= "{" package_0 ";" ... ";" package_n "}"

package ::= "package" pkgname [pkgexports] "where" pkgbody
pkgname ::= /* package name, e.g. containers (no version!) */
pkgbody ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"

pkgdecl ::= "module"    modid [exports] "where" body
          | "signature" modid [exports] "where" body
          | "include"   pkgname ["as" pkgname] [inclspec]
          | "module"    modid_0 "=" path_0 "," ... "," modid_n "=" path_n
          | "signature" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
          | "module"    modid_0 "," ... "," modid_n
          | "signature" modid_0 "," ... "," modid_n
          | "source" path

inclspec ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
             [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
           | "::" pkgexp
pkgexports ::= inclspec

renaming ::= modid [ "as" modid ]
           | "package" pkgname

pkgexp ::= pkgname
         | "package" [exports] "where" pkgbody
         | pkgbody
         | path
\end{verbatim}

\end{document}