Fix LaTeX in core-spec
[ghc.git] / docs / core-spec / core-spec.mng
1 \documentclass{article}
2
3 \usepackage{supertabular}
4 \usepackage{amsmath}
5 \usepackage{amssymb}
6 \usepackage{stmaryrd}
7 \usepackage{xcolor}
8 \usepackage{fullpage}
9 \usepackage{multirow}
10 \usepackage{url}
11
12 \newcommand{\ghcfile}[1]{\textsl{#1}}
13 \newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
14
15 \input{CoreOtt}
16
17 % increase spacing between rules for ease of reading:
18 \renewcommand{\ottusedrule}[1]{\[#1\]\\[1ex]}
19
20 \setlength{\parindent}{0in}
21 \setlength{\parskip}{1ex}
22
23 \newcommand{\gram}[1]{\ottgrammartabular{#1\ottafterlastrule}}
24
25 \begin{document}
26
27 \begin{center}
28 \LARGE
29 System FC, as implemented in GHC\footnote{This
30 document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
31 but it should be maintained by anyone who edits the functions or data structures
32 mentioned in this file. Please feel free to contact Richard for more information.}\\
33 \Large 23 October, 2015
34 \end{center}
35
36 \section{Introduction}
37
38 This document presents the typing system of System FC, very closely to how it is
39 implemented in GHC. Care is taken to include only those checks that are actually
40 written in the GHC code. It should be maintained along with any changes to this
41 type system.
42
43 Who will use this? Any implementer of GHC who wants to understand more about the
44 type system can look here to see the relationships among constructors and the
45 different types used in the implementation of the type system. Note that the
46 type system here is quite different from that of Haskell---these are the details
47 of the internal language, only.
48
49 At the end of this document is a \emph{hypothetical} operational semantics for GHC.
50 It is hypothetical because GHC does not strictly implement a concrete operational
51 semantics anywhere in its code. While all the typing rules can be traced back to
52 lines of real code, the operational semantics do not, in general, have as clear
53 a provenance.
54
55 There are a number of details elided from this presentation. The goal of the
56 formalism is to aid in reasoning about type safety, and checks that do not
57 work toward this goal were omitted. For example, various scoping checks (other
58 than basic context inclusion) appear in the GHC code but not here.
59
60 \section{Grammar}
61
62 \subsection{Metavariables}
63
64 We will use the following metavariables:
65
66 \ottmetavars{}\\
67
68 \subsection{Literals}
69
70 Literals do not play a major role, so we leave them abstract:
71
72 \gram{\ottlit}
73
74 We also leave abstract the function \coderef{basicTypes/Literal.lhs}{literalType}
75 and the judgment \coderef{coreSyn/CoreLint.lhs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
76
77 \subsection{Variables}
78 \enlargethispage{10pt} % without this first line of "z" definition is placed on
79                        % second page and it becomes the only line of text on that
80                        % page, resulting in whole page being empty.
81 GHC uses the same datatype to represent term-level variables and type-level
82 variables:
83
84 \gram{
85 \ottz
86 }
87
88 \gram{
89 \ottn
90 }
91
92 We sometimes omit the type/kind annotation to a variable when it is obvious from context.
93
94 \subsection{Expressions}
95
96 The datatype that represents expressions:
97
98 \gram{\otte}
99
100 There are a few key invariants about expressions:
101 \begin{itemize}
102 \item The right-hand sides of all top-level and recursive $[[let]]$s
103 must be of lifted type, with one exception: the right-hand side of a top-level
104 $[[let]]$ may be of type \texttt{Addr\#} if it's a primitive string literal.
105 See \verb|#top_level_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
106 \item The right-hand side of a non-recursive $[[let]]$ and the argument
107 of an application may be of unlifted type, but only if the expression
108 is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.lhs}.
109 \item We allow a non-recursive $[[let]]$ for bind a type variable.
110 \item The $[[_]]$ case for a $[[case]]$ must come first.
111 \item The list of case alternatives must be exhaustive.
112 \item Types and coercions can only appear on the right-hand-side of an application.
113 \item The $[[t]]$ form of an expression must not then turn out to be a coercion.
114 In other words, the payload inside of a \texttt{Type} constructor must not turn out
115 to be built with \texttt{CoercionTy}. 
116 \end{itemize}
117
118 Bindings for $[[let]]$ statements:
119
120 \gram{\ottbinding}
121
122 Case alternatives:
123
124 \gram{\ottalt}
125
126 Constructors as used in patterns:
127
128 \gram{\ottKp}
129
130 Notes that can be inserted into the AST. We leave these abstract:
131
132 \gram{\otttick}
133
134 A program is just a list of bindings:
135
136 \gram{\ottprogram}
137
138 \subsection{Types}
139
140 \gram{\ottt}
141
142 \ctor{ForAllTy}s are represented in two different ways, depending on whether
143 the \ctor{ForAllTy} is anonymous (written $[[t1 -> t2]]$) or
144 named (written $[[forall n . t]]$).
145
146 There are some invariants on types:
147 \begin{itemize}
148 \item The name used in a type must be a type-level name (\ctor{TyVar}).
149 \item The type $[[t1]]$ in the form $[[t1 t2]]$ must not be a type constructor
150 $[[T]]$. It should be another application or a type variable.
151 \item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp})
152 does \emph{not} need to be saturated.
153 \item A saturated application of $[[(->) t1 t2]]$ should be represented as
154 $[[t1 -> t2]]$. This is a different point in the grammar, not just pretty-printing.
155 The constructor for a saturated $[[(->)]]$ is \texttt{ForAllTy}.
156 \item A type-level literal is represented in GHC with a different datatype than
157 a term-level literal, but we are ignoring this distinction here.
158 \item A coercion used as a type should appear only in the right-hand side of
159   an application.
160 \end{itemize}
161
162 Note that the use of the $[[T </ ti // i />]]$ form and the $[[t1 -> t2]]$ form
163 are purely representational. The metatheory would remain the same if these forms
164 were removed in favor of $[[t1 t2]]$. Nevertheless, we keep all three forms in
165 this documentation to accurately reflect the implementation.
166
167 The \texttt{Named} variant of a \texttt{Binder} (the first argument to a
168 \texttt{ForAllTy}) also tracks visibility of arguments. Visibility affects
169 only source Haskell, and is omitted from this presentation.
170
171 We use the notation $[[t1 k1~#k2 t2]]$ to stand for $[[(~#) k1 k2 t1 t2]]$.
172
173 \subsection{Coercions}
174
175 \gram{\ottg}
176
177 Invariants on coercions:
178 \begin{itemize}
179 \item $[[<t1 t2>_R]]$ is used; never $[[<t1>_R <t2>_Nom]]$.
180 \item If $[[<T>_R]]$ is applied to some coercions, at least one of which is not
181 reflexive, use $[[T_R </ gi // i />]]$, never $[[<T>_R g1 g2]] \ldots$.
182 \item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
183 be a type function.
184 \item Every non-reflexive coercion coerces between two distinct types.
185 \item The name in a coercion must be a term-level name (\ctor{Id}).
186 \item The contents of $[[<t>_R]]$ must not be a coercion. In other words,
187 the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
188 \end{itemize}
189
190 The \texttt{UnivCo} constructor takes several arguments: the two types coerced
191 between, a coercion relating these types' kinds, a role for the universal coercion,
192 and a provenance. The provenance states what created the universal coercion:
193
194 \gram{\ottprov}
195
196 Roles label what equality relation a coercion is a witness of. Nominal equality
197 means that two types are identical (have the same name); representational equality
198 means that two types have the same representation (introduced by newtypes); and
199 phantom equality includes all types. See \url{http://ghc.haskell.org/trac/ghc/wiki/Roles} and \url{http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/coercible.pdf}
200 for more background.
201
202 \gram{\ottR}
203
204 Is it a left projection or a right projection?
205
206 \gram{\ottLorR}
207
208 Axioms:
209
210 \gram{
211 \ottC\ottinterrule
212 \ottaxBranch
213 }
214
215 The left-hand sides $[[ </ tj // j /> ]]$ of different branches of one axiom must
216 all have the same length.
217
218 The definition for $[[axBranch]]$ above does not include the list of
219 incompatible branches (field \texttt{cab\_incomps} of \texttt{CoAxBranch}),
220 as that would unduly clutter this presentation. Instead, as the list
221 of incompatible branches can be computed at any time, it is checked for
222 in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}.
223
224 Axiom rules, produced by the type-nats solver:
225
226 \gram{\ottmu}
227
228 \label{sec:axiom_rules}
229 An axiom rule $[[mu]] = [[M(I, role_list, R')]]$ is an axiom name $[[M]]$, with a
230 type arity $[[I]]$, a list of roles $[[role_list]]$ for its coercion parameters,
231 and an output role $[[R']]$. The definition within GHC also includes a field named
232 $[[coaxrProves]]$ which computes the output coercion from a list of types and
233 a list of coercions. This is elided in this presentation, as we simply identify
234 axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
235 and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
236
237 In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands for following checks:
238 \begin{itemize}
239     \item both types are unboxed;
240     \item types should have same size;
241     \item both types should be either integral or floating;
242     \item coercion between vector types are not allowed;
243     \item unboxed tuples should have same length and each element should be coercible to
244     appropriate element of the target tuple;
245 \end{itemize}
246 For function implementation see \coderef{coreSyn/CoreLint.lhs}{checkTypes}.
247 For further discussion see \url{https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions}.
248
249 \subsection{Type constructors}
250
251 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
252 for this formalism:
253
254 \gram{\ottT}
255
256 We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.lhs}.
257
258 \gram{\ottH}
259
260 Note that although GHC contains distinct type constructors $[[*]]$
261 and $[[Constraint]]$, this formalism treats only $[[*]]$. These two type
262 constructors are considered wholly equivalent. In particular the function
263 \texttt{eqType} returns \texttt{True} when comparing $[[*]]$ and $[[Constraint]]$.
264 We need them both because they serve different functions in source Haskell.
265
266 \paragraph{$[[TYPE]]$}
267 The type system is rooted at the special constant $[[TYPE]]$ and the
268 (quite normal) datatype \texttt{data Levity = Lifted | Unlifted}.
269 The type of $[[TYPE]]$ is $[[Levity -> TYPE 'Lifted]]$. The idea is that
270 $[[TYPE 'Lifted]]$ classifies lifted types and $[[TYPE 'Unlifted]]$
271 classifies unlifted types. Indeed $[[*]]$ is just a plain old type
272 synonym for $[[TYPE 'Lifted]]$, and $[[#]]$ is just a plain old type
273 synonym for $[[TYPE 'Unlifted]]$.
274
275 \section{Contexts}
276
277 The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
278 This monad contains a context with a set of bound variables $[[G]]$. The
279 formalism treats $[[G]]$ as an ordered list, but GHC uses a set as its
280 representation.
281
282 \gram{
283 \ottG
284 }
285
286 We assume the Barendregt variable convention that all new variables are
287 fresh in the context. In the implementation, of course, some work is done
288 to guarantee this freshness. In particular, adding a new type variable to
289 the context sometimes requires creating a new, fresh variable name and then
290 applying a substitution. We elide these details in this formalism, but
291 see \coderef{types/Type.lhs}{substTyVarBndr} for details.
292
293 \section{Typing judgments}
294
295 The following functions are used from GHC. Their names are descriptive, and they
296 are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
297 \coderef{types/TyCon.lhs}{tyConArity}, \coderef{basicTypes/DataCon.lhs}{dataConTyCon}, \coderef{types/TyCon.lhs}{isNewTyCon}, \coderef{basicTypes/DataCon.lhs}{dataConRepType}.
298
299 \subsection{Program consistency}
300
301 Check the entire bindings list in a context including the whole list. We extract
302 the actual variables (with their types/kinds) from the bindings, check for duplicates,
303 and then check each binding.
304
305 \ottdefnlintCoreBindings{}
306
307 Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs}{bindersOf}:
308
309 \[
310 \begin{array}{ll}
311 [[vars_of n = e]] &= [[n]] \\
312 [[vars_of rec </ ni = ei // i />]] &= [[</ ni // i />]]
313 \end{array}
314 \]
315
316 \subsection{Binding consistency}
317
318 \ottdefnlintXXbind{}
319
320 \ottdefnlintSingleBinding{}
321
322 In the GHC source, this function contains a number of other checks, such
323 as for strictness and exportability. See the source code for further information.
324
325 \subsection{Expression typing}
326
327 \ottdefnlintCoreExpr{}
328
329 \begin{itemize}
330 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
331 second premise ($[[</ G, G'i |-ty si : ki // i />]]$) is that we wish
332 to check each substituted type $[[s'i]]$ in a context containing all the types
333 that come before it in the list of bindings. The $[[G'i]]$ are contexts
334 containing the names and kinds of all type variables (and term variables,
335 for that matter) up to the $i$th binding. This logic is extracted from
336 \coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
337
338 \item The GHC source code checks all arguments in an application expression
339 all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
340 and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
341 has been unfolded for presentation here.
342
343 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
344 (scoping) checks.
345
346 \item The rule for $[[case]]$ statements also checks to make sure that
347 the alternatives in the $[[case]]$ are well-formed with respect to the
348 invariants listed above. These invariants do not affect the type or
349 evaluation of the expression, so the check is omitted here.
350
351 \item The GHC source code for \ottdrulename{Tm\_Var} contains checks for
352 a dead id and for one-tuples. These checks are omitted here.
353 \end{itemize}
354
355 \subsection{Kinding}
356
357 \ottdefnlintType{}
358
359 \subsection{Kind validity}
360
361 \ottdefnlintKind{}
362
363 \subsection{Coercion typing}
364
365 In the coercion typing judgment, the $\#$ marks are left off the equality
366 operators to reduce clutter. This is not actually inconsistent, because
367 the GHC function that implements this check, \texttt{lintCoercion}, actually
368 returns five separate values (the two kinds, the two types, and the role), not
369 a type with head $[[(~#)]]$ or $[[(~Rep#)]]$. Note that the difference between
370 these two forms of equality is interpreted in the rules \ottdrulename{Co\_CoVarCoNom}
371 and \ottdrulename{Co\_CoVarCoRepr}.
372
373 \ottdefnlintCoercion{}
374
375 See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
376 see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
377
378 \subsection{Name consistency}
379
380 There are two very similar checks for names, one declared as a local function:
381
382 \ottdefnlintSingleBindingXXlintBinder{}
383
384 \ottdefnlintBinder{}
385
386 \subsection{Substitution consistency}
387
388 \ottdefnlintTyKind{}
389
390 \subsection{Case alternative consistency}
391
392 \ottdefnlintCoreAlt{}
393
394 \subsection{Telescope substitution}
395
396 \ottdefnapplyTys{}
397
398 \subsection{Case alternative binding consistency}
399
400 \ottdefnlintAltBinders{}
401
402 \subsection{Arrow kinding}
403
404 \ottdefnlintArrow{}
405
406 \subsection{Type application kinding}
407
408 \ottdefnlintXXapp{}
409
410 \subsection{Axiom argument kinding}
411
412 \ottdefncheckXXki{}
413
414 \subsection{Roles}
415 \label{sec:tyconroles}
416
417 During type-checking, role inference is carried out, assigning roles to the
418 arguments of every type constructor. The function $[[tyConRoles]]$ extracts these
419 roles. Also used in other judgments is $[[tyConRolesX]]$, which is the same as
420 $[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to account
421 for potential oversaturation.
422
423 The checks encoded in the following
424 judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
425 when \texttt{-dcore-lint} is set.
426
427 \ottdefncheckValidRoles{}
428
429 \ottdefncheckXXdcXXroles{}
430
431 In the following judgment, the role $[[R]]$ is an \emph{input}, not an output.
432 The metavariable $[[O]]$ denotes a \emph{role context}, as shown here:
433
434 \gram{\ottO}
435
436 \ottdefncheckXXtyXXroles{}
437
438 These judgments depend on a sub-role relation:
439
440 \ottdefnltRole{}
441
442 \subsection{Branched axiom conflict checking}
443 \label{sec:no_conflict}
444
445 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
446 sure that a type family application cannot unify with any previous branch
447 in the axiom. The actual code scans through only those branches that are
448 flagged as incompatible. These branches are stored directly in the
449 $[[axBranch]]$. However, it is cleaner in this presentation to simply
450 check for compatibility here.
451
452 \ottdefncheckXXnoXXconflict{}
453
454 The judgment $[[apart]]$ checks to see whether two lists of types are surely
455 apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
456 ]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
457 \emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
458     // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
459 see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
460 Flattening takes all type family applications and replaces them with fresh variables,
461 taking care to map identical type family applications to the same fresh variable.
462
463 The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
464 It performs a standard unification, returning a substitution upon success.
465
466 \section{Operational semantics}
467
468 \subsection{Disclaimer}
469 GHC does not implement an operational semantics in any concrete form. Most
470 of the rules below are implied by algorithms in, for example, the simplifier
471 and optimizer. Yet, there is no one place in GHC that states these rules,
472 analogously to \texttt{CoreLint.lhs}.
473 Nevertheless, these rules are included in this document to help the reader
474 understand System FC.
475
476 \subsection{The context $[[S]]$}
477 We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
478 recursive group. Its definition is as follows:
479 \[
480 [[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]]
481 \]
482 The presence of the context $[[S]]$ is solely to deal with recursion. If your
483 use of FC does not require modeling recursion, you will not need to track $[[S]]$.
484
485 \subsection{Operational semantics rules}
486
487 \ottdefnstep{}
488
489 \subsection{Notes}
490
491 \begin{itemize}
492 \item The \ottdrulename{S\_LetRec} rules
493 implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
494 for all of the mutually recursive equations. Then, after perhaps many steps,
495 when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
496 in the $[[let]]\ [[rec]]$, the context is popped in \ottdrulename{S\_LetRecReturn}.
497 The other \ottdrulename{S\_LetRecXXX}
498 rules are there to prevent reduction from getting stuck.
499 \item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
500 lists of arguments: two lists of types and a list of terms. The types passed
501 in are the universally and, respectively, existentially quantified type variables
502 to the constructor. The terms are the regular term arguments stored in an
503 algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
504 \item The rule \ottdrulename{S\_CasePush} is the most complex rule.
505 \begin{itemize}
506 \item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
507 \item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
508 extracts the two types (and their kinds) from
509 a coercion. It does not require a typing context, as it does not \emph{check} the
510 coercion, just extracts its types.
511 \item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
512 constructor expressions, the parameters to the constructor are broken into three
513 groups: universally quantified types, existentially quantified types, and terms.
514 \item The substitutions in the last premise to the rule are unusual: they replace
515 \emph{type} variables with \emph{coercions}. This substitution is called lifting
516 and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
517 essentially a pun on the fact that types and coercions have such similar structure.
518 This operation is quite non-trivial. Please see \emph{System FC with Explicit
519 Kind Equality} for details.
520 \item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
521 types---do not change during this step.
522 \end{itemize}
523 \end{itemize}
524
525 \end{document}