Merge branch 'ghc-parmake-gsoc' (#910)
[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 9 September, 2013
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
79 GHC uses the same datatype to represent term-level variables and type-level
80 variables:
81
82 \gram{
83 \ottz
84 }
85
86 \gram{
87 \ottn
88 }
89
90 \subsection{Expressions}
91
92 The datatype that represents expressions:
93
94 \gram{\otte}
95
96 There are a few key invariants about expressions:
97 \begin{itemize}
98 \item The right-hand sides of all top-level and recursive $[[let]]$s
99 must be of lifted type.
100 \item The right-hand side of a non-recursive $[[let]]$ and the argument
101 of an application may be of unlifted type, but only if the expression
102 is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.lhs}.
103 \item We allow a non-recursive $[[let]]$ for bind a type variable.
104 \item The $[[_]]$ case for a $[[case]]$ must come first.
105 \item The list of case alternatives must be exhaustive.
106 \item Types and coercions can only appear on the right-hand-side of an application.
107 \end{itemize}
108
109 Bindings for $[[let]]$ statements:
110
111 \gram{\ottbinding}
112
113 Case alternatives:
114
115 \gram{\ottalt}
116
117 Constructors as used in patterns:
118
119 \gram{\ottKp}
120
121 Notes that can be inserted into the AST. We leave these abstract:
122
123 \gram{\otttick}
124
125 A program is just a list of bindings:
126
127 \gram{\ottprogram}
128
129 \subsection{Types}
130
131 \gram{\ottt}
132
133 There are some invariants on types:
134 \begin{itemize}
135 \item The type $[[t1]]$ in the form $[[t1 t2]]$ must not be a type constructor
136 $[[T]]$. It should be another application or a type variable.
137 \item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp}) 
138 does \emph{not} need to be saturated.
139 \item A saturated application of $[[(->) t1 t2]]$ should be represented as 
140 $[[t1 -> t2]]$. This is a different point in the grammar, not just pretty-printing.
141 The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
142 \item A type-level literal is represented in GHC with a different datatype than
143 a term-level literal, but we are ignoring this distinction here.
144 \end{itemize}
145
146 \subsection{Coercions}
147
148 \gram{\ottg}
149
150 Invariants on coercions:
151 \begin{itemize}
152 \item $[[<t1 t2>_R]]$ is used; never $[[<t1>_R <t2>_Nom]]$.
153 \item If $[[<T>_R]]$ is applied to some coercions, at least one of which is not
154 reflexive, use $[[T_R </ gi // i />]]$, never $[[<T>_R g1 g2]] \ldots$.
155 \item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
156 be a type function.
157 \end{itemize}
158
159 Roles label what equality relation a coercion is a witness of. Nominal equality
160 means that two types are identical (have the same name); representational equality
161 means that two types have the same representation (introduced by newtypes); and
162 phantom equality includes all types. See \url{http://ghc.haskell.org/trac/ghc/wiki/Roles}
163 for more background.
164
165 \gram{\ottR}
166
167 Is it a left projection or a right projection?
168
169 \gram{\ottLorR}
170
171 Axioms:
172
173 \gram{
174 \ottC\ottinterrule
175 \ottaxBranch
176 }
177
178 The definition for $[[axBranch]]$ above does not include the list of
179 incompatible branches (field \texttt{cab\_incomps} of \texttt{CoAxBranch}),
180 as that would unduly clutter this presentation. Instead, as the list
181 of incompatible branches can be computed at any time, it is checked for
182 in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}.
183
184 \subsection{Type constructors}
185
186 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
187 for this formalism:
188
189 \gram{\ottT}
190
191 We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.lhs}.
192
193 \gram{\ottH}
194
195 \section{Contexts}
196
197 The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
198 This monad contains a context with a set of bound variables $[[G]]$. The
199 formalism treats $[[G]]$ as an ordered list, but GHC uses a set as its
200 representation.
201
202 \gram{
203 \ottG
204 }
205
206 We assume the Barendregt variable convention that all new variables are
207 fresh in the context. In the implementation, of course, some work is done
208 to guarantee this freshness. In particular, adding a new type variable to
209 the context sometimes requires creating a new, fresh variable name and then
210 applying a substitution. We elide these details in this formalism, but
211 see \coderef{types/Type.lhs}{substTyVarBndr} for details.
212
213 \section{Typing judgments}
214
215 The following functions are used from GHC. Their names are descriptive, and they
216 are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
217 \coderef{types/TyCon.lhs}{tyConArity}, \coderef{basicTypes/DataCon.lhs}{dataConTyCon}, \coderef{types/TyCon.lhs}{isNewTyCon}, \coderef{basicTypes/DataCon.lhs}{dataConRepType}.
218
219 \subsection{Program consistency}
220
221 Check the entire bindings list in a context including the whole list. We extract
222 the actual variables (with their types/kinds) from the bindings, check for duplicates,
223 and then check each binding.
224
225 \ottdefnlintCoreBindings{}
226
227 Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs}{bindersOf}:
228
229 \[
230 \begin{array}{ll}
231 [[vars_of n = e]] &= [[n]] \\
232 [[vars_of rec </ ni = ei // i />]] &= [[</ ni // i />]]
233 \end{array}
234 \]
235
236 \subsection{Binding consistency}
237
238 \ottdefnlintXXbind{}
239
240 \ottdefnlintSingleBinding{}
241
242 In the GHC source, this function contains a number of other checks, such
243 as for strictness and exportability. See the source code for further information.
244
245 \subsection{Expression typing}
246
247 \ottdefnlintCoreExpr{}
248
249 %\arraylabel{\coderef{coreSyn/CoreLint.lhs}{checkCaseAlts}} \\
250 %\multicolumn{2}{l}{[[checkCaseAlts]] \text{ checks ordering and exhaustivity constr%aints}} \\
251
252 %\end{array}
253 %\]
254
255 \begin{itemize}
256 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
257 second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
258 to check each substituted type $[[s'i]]$ in a context containing all the types
259 that come before it in the list of bindings. The $[[G'i]]$ are contexts
260 containing the names and kinds of all type variables (and term variables,
261 for that matter) up to the $i$th binding. This logic is extracted from
262 \coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
263
264 \item There is one more case for $[[G |-tm e : t]]$, for type expressions.
265 This is included in the GHC code but is elided
266 here because the case is never used in practice. Type expressions
267 can only appear in arguments to functions, and these are handled
268 in \ottdrulename{Tm\_AppType}.
269
270 \item The GHC source code checks all arguments in an application expression
271 all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
272 and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
273 has been unfolded for presentation here.
274
275 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
276 (scoping) checks.
277
278 \item The rule for $[[case]]$ statements also checks to make sure that
279 the alternatives in the $[[case]]$ are well-formed with respect to the
280 invariants listed above. These invariants do not affect the type or
281 evaluation of the expression, so the check is omitted here.
282
283 \item The GHC source code for \ottdrulename{Tm\_Var} contains checks for
284 a dead id and for one-tuples. These checks are omitted here.
285 \end{itemize}
286
287 \subsection{Kinding}
288
289 \ottdefnlintType{}
290
291 \subsection{Kind validity}
292
293 \ottdefnlintKind{}
294
295 \subsection{Coercion typing}
296
297 In the coercion typing judgment, the $\#$ marks are left off the equality
298 operators to reduce clutter. This is not actually inconsistent, because
299 the GHC function that implements this check, \texttt{lintCoercion}, actually
300 returns four separate values (the kind, the two types, and the role), not
301 a type with head $[[(~#)]]$ or $[[(~R#)]]$. Note that the difference between
302 these two forms of equality is interpreted in the rules \ottdrulename{Co\_CoVarCoNom}
303 and \ottdrulename{Co\_CoVarCoRepr}.
304
305 \ottdefnlintCoercion{}
306
307 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
308 the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of 
309 folding the substitution over the kinds for kind-checking.
310
311 See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$.
312
313 \subsection{Name consistency}
314
315 There are two very similar checks for names, one declared as a local function:
316
317 \ottdefnlintSingleBindingXXlintBinder{}
318
319 \ottdefnlintBinder{}
320
321 \subsection{Substitution consistency}
322
323 \ottdefncheckTyKind{}
324
325 \subsection{Case alternative consistency}
326
327 \ottdefnlintCoreAlt{}
328
329 \subsection{Telescope substitution}
330
331 \ottdefnapplyTys{}
332
333 \subsection{Case alternative binding consistency}
334
335 \ottdefnlintAltBinders{}
336
337 \subsection{Arrow kinding}
338
339 \ottdefnlintArrow{}
340
341 \subsection{Type application kinding}
342
343 \ottdefnlintXXapp{}
344
345 \subsection{Sub-kinding}
346
347 \ottdefnisSubKind{}
348
349 \subsection{Roles}
350 \label{sec:tyconroles}
351
352 During type-checking, role inference is carried out, assigning roles to the
353 arguments of every type constructor. The function $[[tyConRoles]]$ extracts these
354 roles. Also used in other judgments is $[[tyConRolesX]]$, which is the same as
355 $[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to account
356 for potential oversaturation.
357
358 The checks encoded in the following
359 judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
360 when \texttt{-dcore-lint} is set.
361
362 \ottdefncheckValidRoles{}
363
364 \ottdefncheckXXdcXXroles{}
365
366 In the following judgment, the role $[[R]]$ is an \emph{input}, not an output.
367 The metavariable $[[O]]$ denotes a \emph{role context}, as shown here:
368
369 \gram{\ottO}
370
371 \ottdefncheckXXtyXXroles{}
372
373 These judgments depend on a sub-role relation:
374
375 \ottdefnltRole{}
376
377 \subsection{Branched axiom conflict checking}
378 \label{sec:no_conflict}
379
380 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
381 sure that a type family application cannot unify with any previous branch
382 in the axiom. The actual code scans through only those branches that are
383 flagged as incompatible. These branches are stored directly in the
384 $[[axBranch]]$. However, it is cleaner in this presentation to simply
385 check for compatibility here.
386
387 \ottdefncheckXXnoXXconflict{}
388
389 The judgment $[[apart]]$ checks to see whether two lists of types are surely
390 apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
391 ]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
392 \emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
393     // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
394 see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
395 Flattening takes all type family applications and replaces them with fresh variables,
396 taking care to map identical type family applications to the same fresh variable.
397
398 The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
399 It performs a standard unification, returning a substitution upon success.
400
401 \section{Operational semantics}
402
403 \subsection{Disclaimer}
404 GHC does not implement an operational semantics in any concrete form. Most
405 of the rules below are implied by algorithms in, for example, the simplifier
406 and optimizer. Yet, there is no one place in GHC that states these rules,
407 analogously to \texttt{CoreLint.lhs}.
408 Nevertheless, these rules are included in this document to help the reader
409 understand System FC.
410
411 \subsection{The context $[[S]]$}
412 We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
413 recursive group. Its definition is as follows:
414 \[
415 [[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]]
416 \]
417 The presence of the context $[[S]]$ is solely to deal with recursion. If your
418 use of FC does not require modeling recursion, you will not need to track $[[S]]$.
419
420 \subsection{Operational semantics rules}
421
422 \ottdefnstep{}
423
424 \subsection{Notes}
425
426 \begin{itemize}
427 \item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
428 implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
429 for all of the mutually recursive equations. Then, after perhaps many steps,
430 when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
431 in the $[[let]]\ [[rec]]$, the context is popped.
432 \item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
433 lists of arguments: two lists of types and a list of terms. The types passed
434 in are the universally and, respectively, existentially quantified type variables
435 to the constructor. The terms are the regular term arguments stored in an
436 algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
437 \item The rule \ottdrulename{S\_CasePush} is the most complex rule.
438 \begin{itemize}
439 \item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
440 \item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
441 extracts the two types (and their kind) from
442 a coercion. It does not require a typing context, as it does not \emph{check} the
443 coercion, just extracts its types.
444 \item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
445 constructor expressions, the parameters to the constructor are broken into three
446 groups: universally quantified types, existentially quantified types, and terms.
447 \item The substitutions in the last premise to the rule are unusual: they replace
448 \emph{type} variables with \emph{coercions}. This substitution is called lifting
449 and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
450 essentially a pun on the fact that types and coercions have such similar structure.
451 \item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
452 types---do not change during this step.
453 \end{itemize}
454 \end{itemize}
455
456 \end{document}