89826789a5659407269b1b647c75678b9ee736c2
[ghc.git] / docs / backpack / backpack-manual.tex
1 \documentclass{article}
2
3 \usepackage{color}
4 \usepackage{fullpage}
5 \usepackage{hyperref}
6
7 \newcommand{\Red}[1]{{\color{red} #1}}
8
9 \title{The Backpack Manual}
10
11 \begin{document}
12
13 \maketitle
14
15 Backpack is a new module system for Haskell, intended to enable
16 ``separate modular development'': a style of development where
17 application-writers can develop against abstract interfaces or
18 \emph{signatures}, while separately library-writers write software which
19 implement these interfaces. Backpack was originally described in a
20 POPL'14 paper \url{http://plv.mpi-sws.org/backpack/}, but the point of
21 this document is to describe the syntax of a language you might actually
22 be able to \emph{write}, as well as describe some of the changes to the
23 design we've made since this paper.
24
25 \paragraph{Examples}
26
27 Before we dive in, here are some examples of Backpack files to whet
28 your appetite:
29
30 \begin{verbatim}
31 package p(A) where
32 module A(a) where
33 a = True
34
35 package q(B, C) where
36 include p
37 module B(b) where
38 import A
39 b = a
40 module C(c) where
41 import B
42 c = b
43 \end{verbatim}
44
45 In this example package \verb|p| exports a single module \verb|A|; package \verb|q| exports
46 two modules, and includes package \verb|p| so that its modules are in
47 scope. The form of a \verb|package| and a \verb|module| are quite similar:
48 a package can express an explicit export list of modules in much the same
49 way a module exports identifiers. \\
50
51 Here is a more complicated Backpack file taking advantage of the availability
52 of signatures in Backpack. This example omits the actual module bodies: GHC
53 will automatically look for them in appropriate files (e.g. \verb|p/Map.hsig|,
54 \verb|p/P/Types.hs|, \verb|p/P.hs|, \verb|q/QMap.hs| and \verb|q/Q.hs|).
55
56 \begin{verbatim}
57 package p (P) requires (Map) where
58 include base
59 signature Map
60 module P.Types
61 module P
62
63 package q (Q) where
64 include base
65 module QMap
66 include p (P) requires (Map as QMap)
67 module Q
68 \end{verbatim}
69
70 Package \verb|p| provides a module \verb|P|, but it also \emph{requires}
71 a module \verb|Map| (which must fulfill the specification described
72 in \verb|signature Map|). This makes it an \emph{indefinite package}:
73 a package which isn't fully implemented, and cannot be compiled into
74 executable code until its ``hole'' (\verb|Map|) is filled.
75 It also sports an internal module named \verb|P.Types| which
76 is missing from the export list, and thus not exported.
77
78 Package \verb|q|, on the other hand, is a \emph{definite package}; as it
79 has no requirements, it can be compiled. When it includes \verb|p|
80 into scope, it also fills the \verb|Map| requirement with an
81 implementation \verb|QMap|.
82
83 \section{The Backpack file}
84
85 \begin{verbatim}
86 packages ::= "{" package_0 ";" ... ";" package_n "}"
87 \end{verbatim}
88
89 A Backpack file consists of a list of named packages.
90 All packages in a Backpack file live in the global namespace.
91 A package defines a collection of modules, exporting some of
92 these modules so that other modules can make use of them via
93 \emph{include}. You can compile a definite package \verb|p| in a Backpack file \verb|foo.bkp|
94 with \verb|ghc --backpack foo.bkp p|; you can type-check an indefinite package by
95 adding \verb|-fno-code|.
96
97 \Red{ToDo: How do you import an external Backpack file?}
98
99 \Red{ToDo: Facility for private packages.}
100
101 \begin{verbatim}
102 package ::= "package" pkgname [pkgexports] "where" pkgbody
103 pkgname ::= /* package name, e.g. containers (no version!) */
104 pkgbody ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
105 \end{verbatim}
106
107 A package begins with the keyword \verb|package|, its name, and an
108 optional export specification (e.g., a list of modules to be exposed).
109 The header is followed a list of declarations which define modules,
110 signatures and include other packages.
111
112 \section{Declarations}
113
114 \begin{verbatim}
115 pkgdecl ::= "module" modid [exports] "where" body
116 | "signature" modid [exports] "where" body
117 | "include" pkgname ["as" pkgname] [inclspec]
118 \end{verbatim}
119
120 A package is made up of package declarations, which either introduce a
121 new module implementation, introduces a new module
122 signature, or includes a package from the package environment.
123 The declaration of modules and signatures is exactly as it is in Haskell98,
124 so we don't reprise the grammar here.
125
126 \Red{ToDo: Clarify whether order matters. Both are valid designs, but I think order-less is more user-friendly.}
127
128 We generally don't expect users to place their module source code
129 in package files; thus we provide the following forms to refer to
130 \verb|hs| and \verb|hsig| files living on the file-system:
131
132 \begin{verbatim}
133 pkgdecl ::= "module" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
134 | "signature" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
135 | "module" modid_0 "," ... "," modid_n
136 | "signature" modid_0 "," ... "," modid_n
137 \end{verbatim}
138
139 Thus, \verb|module A = "A.hs"| defines the body of \verb|A| based
140 on the contents of \verb|A.hs| in the package's source directory.
141 When the assignment is omitted, we implicitly refer to the file path
142 created by replacing periods with directory separators and adding
143 an appropriate file extension (thus, we can also write \verb|module A|).
144
145 \begin{verbatim}
146 pkgdecl ::= "source" path
147 \end{verbatim}
148
149 The \verb|source| keyword is another construct which allows us to
150 define modules by simply scanning the path in question. For example,
151 if \verb|src| contains two files, \verb|A.hs| and \verb|B.hsig|,
152 then ``\verb|source "src"|'' is equivalent to
153 ``\verb|module A = "src/A.hs"; signature B = "src/B.hsig"|''.
154
155 \Red{ToDo: Allow defining package-wide module imports, which propagate to all inline
156 modules and signatures.}
157
158 \Red{ToDo: Allow defining anonymous modules with bare type/expression declarations.}
159
160 \section{Signatures}
161
162 A signature, denoted with \verb|signature| in a Backpack file and a file
163 with the \verb|hsig| extension on the file system, represents a (type) signature for a
164 Haskell module. It can contain type signatures, data declarations, type
165 classes, type class instances and reexports(!), but it cannot contain any
166 value definitions.\footnote{Signatures are the backbone of the Backpack
167 module system. A signature can be used to type-check client code which
168 uses a module (without the module implementation), or to verify that an
169 implementation upholds some signature (without a client
170 implementation.)} Signatures are essentially
171 \texttt{hs-boot} modules which do not support mutual recursion but
172 have no runtime efficiency cost. Here is an example of a module signature
173 representing an abstract map type:
174
175 \begin{verbatim}
176 module Map where
177 type role Map nominal representational
178 data Map k v
179 instance Functor (Map k)
180 empty :: Map k a
181 \end{verbatim}
182
183 \section{Includes and exports}
184
185 \begin{verbatim}
186 pkgdecl ::= "include" pkgname ["as" pkgname] [inclspec]
187
188 inclspec ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
189 [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
190
191 renaming ::= modid [ "as" modid ]
192 | "package" pkgname
193 \end{verbatim}
194
195 % Add me later:
196 % | "hiding" "(" modid_0 "," ... "," modid_n [","] ")"
197
198 An include brings the modules and signatures of a package into scope.
199 If these modules/signatures have the same names as other
200 modules/signatures in scope, \emph{mix-in linking} occurs.
201 In particular:
202
203 \begin{itemize}
204 \item Module + module = error (unless they really are the same!)
205 \item Module + signature = the signature is filled in, and is
206 no longer part of the requirements of the package.
207 \item Signature + signature = the signatures are merged together.
208 \end{itemize}
209
210 An include is associated with an optional \verb|inclspec|,
211 which can be to thin the provided modules and rename the provided and
212 required modules of an include. In its simplest mode of use,
213 an \verb|inclspec| is a list of modules to be brought into scope,
214 e.g. \verb|include p (A, B)|. Requirements cannot be hidden, but
215 they can be renamed to provide an implementation (or even to just
216 reexport the requirement under another name.) If a requirement is
217 not mentioned in an explicit requirements list, it is implicitly included
218 (thus, \verb|requires (Hole)| has only a purely documentary effect).
219 It is not valid to rename a provision to a requirement, or a requirement
220 to a provision.
221
222 \begin{verbatim}
223 pkgexports ::= inclspec
224 \end{verbatim}
225
226 An export, symmetrically, specifies what modules a package will bring
227 into scope if it is included without any \verb|inclspec|. Any module
228 which is omitted from an explicit export list is not exposed (however,
229 like before, requirements cannot be hidden.)
230
231 When an explicit export list is omitted, you can calculate the provides
232 and requires of a package as follows:
233
234 \begin{itemize}
235 \item A package provides any non-included modules and signatures.
236 (It only provides an included module/signature if it is explicitly
237 reexported.)
238 \item A package requires any transitively reachable signatures or
239 hole signatures which are not filled in with an implementation.
240 \end{itemize}
241
242 \Red{ToDo: Properly describe ``hole signatures'' in the declarations section}
243
244 \subsection{Requirements}
245
246 The fact that requirements are \emph{implicitly} propagated from package
247 to package can result in some spooky ``action at a distance''. However,
248 this implicit behavior is one of the key ingredients to making mix-in
249 modular development scale: you don't want to have to explicitly link
250 everything up, as you might have to do in a traditional ML module
251 system.
252
253 You cannot, however, import a requirement, unless it is also provided,
254 which helps increase encapsulation. If a package provides a
255 module, it can be imported:
256
257 \begin{verbatim}
258 package p (A) requires (A) where
259 signature A where
260 x :: Bool
261 package q (B) requires (A) where
262 include p
263 module B where
264 import A -- OK
265 \end{verbatim}
266
267 If it does not, it cannot be imported:
268 \Red{Alternately, the import is OK but doesn't result in any identifiers
269 being brought into scope.}
270
271 \begin{verbatim}
272 package p () requires (A) where -- yes, this is kind of pointless
273 signature A where
274 x :: Bool
275 package q (B) requires (A) where
276 include p
277 module B where
278 import A -- ERROR!
279 \end{verbatim}
280
281 This means that it is always safe for a package to remove requirements
282 or weaken holes; clients will always continue to compile.
283
284 Of course, if there is a different signature for the hole in scope, the
285 import is not an error; however, no declarations from \verb|p| are in scope:
286
287 \begin{verbatim}
288 package p () requires (A) where
289 signature A where
290 x :: Bool
291 package q (B) requires (A) where
292 include p
293 signature A where
294 y :: Bool
295 module B where
296 import A
297 x' = x -- ERROR!
298 y' = y -- OK
299 \end{verbatim}
300
301 To summarize, requirements are part of the interface of a package; however,
302 they provide no identifiers as far as imports are concerned. \Red{There is
303 some subtle interaction with requirements and shaping; see Shaping by example
304 for more details.}
305
306 \subsection{Package includes/exports}
307
308 A package export is easy enough to explain by analogy of module exports
309 in Haskell: a \verb|package p| in an export list explicitly reexports
310 the identifiers from that package; whereas even a default, wildcard export
311 list would only export locally defined identifiers/modules.
312
313 For example, this module exports the modules of both \verb|base|
314 and \verb|array|.
315
316 \begin{verbatim}
317 package combined(package base, package array) where
318 include base
319 include array
320 \end{verbatim}
321
322 However, in Backpack, a package may be included multiple times, making
323 such declarations ambiguous. Thus, a package can be included as a local
324 package name to disambiguate:
325
326 \begin{verbatim}
327 package p(package q1) where -- equivalent to B1
328 include impls (A1, A2)
329 include q as q1 (hole A as A1, B as B1)
330 include q as q2 (hole A as A2, B as B2)
331 \end{verbatim}
332
333 A package include, e.g. \verb|include a (package p)| is only valid if
334 \verb|a| exports the package \verb|p| explicitly.\footnote{It's probably
335 possible to use anonymous packages to allow easily dividing a package
336 into subpackages, but this is silly and you can always just put it
337 in an actual package.}
338
339 \section{(Transparent) signature ascription}
340
341 \begin{verbatim}
342 inclspec ::= ...
343 | "::" pkgexp
344
345 pkgexp ::= pkgname
346 | "package" [exports] "where" pkgbody
347 \end{verbatim}
348
349 Signature ascription subsumes thinning: it narrows the exports
350 of modules in a package to those specified by a signature
351 package. This package \verb|pkgexp| is specified with either
352 a reference to a named package or an \emph{anonymous package}
353 (in prior work, these have been referred to as \emph{units},
354 although here the distinction is not necessary as our system
355 is \emph{purely applicative}).
356
357 Ascription also imposes a \emph{requirement} on the package
358 being abscribed. Suppose you have \verb|p :: psig|, then:
359
360 \begin{itemize}
361 \item Everything provided \verb|psig| must also
362 be provided by \verb|p|.
363 \item Everything required by \verb|p| must also
364 be required by \verb|psig|.
365 \end{itemize}
366
367 \Red{Alternately, the second requirement is not necessary, and you
368 calculate the new requirements by taking the requirements of \texttt{psig},
369 removing the provides of \texttt{p}, and then adding the requirements of \texttt{p}.
370 This makes it possible to ascribe includes for \emph{adapter} packages, which
371 provide some modules given a different set of requirements.}
372
373 Semantically, ascription replaces the module with a signature,
374 type-checks the package against the signature, and then \emph{post
375 facto} links the signature against the implementation.
376 An ascribed include can be replaced with the signature
377 it is ascribed with, resulting in a package which still typechecks
378 but has more holes. \Red{You have to link at the VERY END, because
379 if you link immediately after processing the module with the
380 ascribed include, the module identities will leak. Of course, if
381 we're compiling we just link eagerly. But now this means that
382 if you have a definite package which uses ascription, even assuming
383 all packages in the environment type-check, you must still type-check
384 this package twice, once indefinitely and then with the actual
385 linking relationship.}
386
387 For example, ascription in the export specification thins out all
388 private identifiers from the package:
389
390 \begin{verbatim}
391 package psig where
392 signature A where
393 public :: Bool
394 package p :: psig where
395 module A.Internal where
396 not_exported = 0
397 module A where
398 public = True
399 private = False
400 \end{verbatim}
401
402 and, symmetrically, ascription in an include hides identifiers:
403
404 \begin{verbatim}
405 package psig where
406 signature A where
407 public :: Bool
408 package p where
409 module A where
410 public = True
411 private = False
412 package q where
413 include p :: psig
414 module B where
415 import A
416 ... public ... -- OK
417 ... private ... -- ERROR
418 \end{verbatim}
419
420 \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.}
421
422 \paragraph{Syntactic sugar for anonymous packages}
423
424 \begin{verbatim}
425 pkgexp ::= pkgbody
426 | path
427 \end{verbatim}
428
429 It may be useful to provide two forms of sugar for specifying anonymous packages:
430 \verb|pkgbody| is equivalent to \verb|package where pkgbody|; and \verb|"path"|
431 is equivalent to \verb|package where source "path"|.
432
433 \appendix
434 \section{Full grammar}
435
436 \begin{verbatim}
437 packages ::= "{" package_0 ";" ... ";" package_n "}"
438
439 package ::= "package" pkgname [pkgexports] "where" pkgbody
440 pkgname ::= /* package name, e.g. containers (no version!) */
441 pkgbody ::= "{" pkgdecl_0 ";" ... ";" pkgdecl_n "}"
442
443 pkgdecl ::= "module" modid [exports] "where" body
444 | "signature" modid [exports] "where" body
445 | "include" pkgname ["as" pkgname] [inclspec]
446 | "module" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
447 | "signature" modid_0 "=" path_0 "," ... "," modid_n "=" path_n
448 | "module" modid_0 "," ... "," modid_n
449 | "signature" modid_0 "," ... "," modid_n
450 | "source" path
451
452 inclspec ::= "(" renaming_0 "," ... "," renaming_n [","] ")"
453 [ "requires" "(" renaming_0 "," ... "," renaming_n [","] ")" ]
454 | "::" pkgexp
455 pkgexports ::= inclspec
456
457 renaming ::= modid [ "as" modid ]
458 | "package" pkgname
459
460 pkgexp ::= pkgname
461 | "package" [exports] "where" pkgbody
462 | pkgbody
463 | path
464 \end{verbatim}
465
466 \end{document}