Update to core-spec documentation.
[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 21 November, 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 Axiom rules, produced by the type-nats solver:
185
186 \gram{\ottmu}
187
188 \label{sec:axiom_rule}
189 An axiom rule $[[mu]] = [[M(I, role_list, R')]]$ is an axiom name $[[M]]$, with a
190 type arity $[[I]]$, a list of roles $[[role_list]]$ for its coercion parameters,
191 and an output role $[[R']]$. The definition within GHC also includes a field named
192 $[[coaxrProves]]$ which computes the output coercion from a list of types and
193 a list of coercions. This is elided in this presentation, as we simply identify
194 axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
195 and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
196
197 \subsection{Type constructors}
198
199 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
200 for this formalism:
201
202 \gram{\ottT}
203
204 We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.lhs}.
205
206 \gram{\ottH}
207
208 \section{Contexts}
209
210 The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
211 This monad contains a context with a set of bound variables $[[G]]$. The
212 formalism treats $[[G]]$ as an ordered list, but GHC uses a set as its
213 representation.
214
215 \gram{
216 \ottG
217 }
218
219 We assume the Barendregt variable convention that all new variables are
220 fresh in the context. In the implementation, of course, some work is done
221 to guarantee this freshness. In particular, adding a new type variable to
222 the context sometimes requires creating a new, fresh variable name and then
223 applying a substitution. We elide these details in this formalism, but
224 see \coderef{types/Type.lhs}{substTyVarBndr} for details.
225
226 \section{Typing judgments}
227
228 The following functions are used from GHC. Their names are descriptive, and they
229 are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
230 \coderef{types/TyCon.lhs}{tyConArity}, \coderef{basicTypes/DataCon.lhs}{dataConTyCon}, \coderef{types/TyCon.lhs}{isNewTyCon}, \coderef{basicTypes/DataCon.lhs}{dataConRepType}.
231
232 \subsection{Program consistency}
233
234 Check the entire bindings list in a context including the whole list. We extract
235 the actual variables (with their types/kinds) from the bindings, check for duplicates,
236 and then check each binding.
237
238 \ottdefnlintCoreBindings{}
239
240 Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs}{bindersOf}:
241
242 \[
243 \begin{array}{ll}
244 [[vars_of n = e]] &= [[n]] \\
245 [[vars_of rec </ ni = ei // i />]] &= [[</ ni // i />]]
246 \end{array}
247 \]
248
249 \subsection{Binding consistency}
250
251 \ottdefnlintXXbind{}
252
253 \ottdefnlintSingleBinding{}
254
255 In the GHC source, this function contains a number of other checks, such
256 as for strictness and exportability. See the source code for further information.
257
258 \subsection{Expression typing}
259
260 \ottdefnlintCoreExpr{}
261
262 \begin{itemize}
263 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
264 second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
265 to check each substituted type $[[s'i]]$ in a context containing all the types
266 that come before it in the list of bindings. The $[[G'i]]$ are contexts
267 containing the names and kinds of all type variables (and term variables,
268 for that matter) up to the $i$th binding. This logic is extracted from
269 \coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
270
271 \item There is one more case for $[[G |-tm e : t]]$, for type expressions.
272 This is included in the GHC code but is elided
273 here because the case is never used in practice. Type expressions
274 can only appear in arguments to functions, and these are handled
275 in \ottdrulename{Tm\_AppType}.
276
277 \item The GHC source code checks all arguments in an application expression
278 all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
279 and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
280 has been unfolded for presentation here.
281
282 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
283 (scoping) checks.
284
285 \item The rule for $[[case]]$ statements also checks to make sure that
286 the alternatives in the $[[case]]$ are well-formed with respect to the
287 invariants listed above. These invariants do not affect the type or
288 evaluation of the expression, so the check is omitted here.
289
290 \item The GHC source code for \ottdrulename{Tm\_Var} contains checks for
291 a dead id and for one-tuples. These checks are omitted here.
292 \end{itemize}
293
294 \subsection{Kinding}
295
296 \ottdefnlintType{}
297
298 \subsection{Kind validity}
299
300 \ottdefnlintKind{}
301
302 \subsection{Coercion typing}
303
304 In the coercion typing judgment, the $\#$ marks are left off the equality
305 operators to reduce clutter. This is not actually inconsistent, because
306 the GHC function that implements this check, \texttt{lintCoercion}, actually
307 returns four separate values (the kind, the two types, and the role), not
308 a type with head $[[(~#)]]$ or $[[(~R#)]]$. Note that the difference between
309 these two forms of equality is interpreted in the rules \ottdrulename{Co\_CoVarCoNom}
310 and \ottdrulename{Co\_CoVarCoRepr}.
311
312 \ottdefnlintCoercion{}
313
314 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
315 the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of 
316 folding the substitution over the kinds for kind-checking.
317
318 See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
319 see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
320
321 \subsection{Name consistency}
322
323 There are two very similar checks for names, one declared as a local function:
324
325 \ottdefnlintSingleBindingXXlintBinder{}
326
327 \ottdefnlintBinder{}
328
329 \subsection{Substitution consistency}
330
331 \ottdefncheckTyKind{}
332
333 \subsection{Case alternative consistency}
334
335 \ottdefnlintCoreAlt{}
336
337 \subsection{Telescope substitution}
338
339 \ottdefnapplyTys{}
340
341 \subsection{Case alternative binding consistency}
342
343 \ottdefnlintAltBinders{}
344
345 \subsection{Arrow kinding}
346
347 \ottdefnlintArrow{}
348
349 \subsection{Type application kinding}
350
351 \ottdefnlintXXapp{}
352
353 \subsection{Sub-kinding}
354
355 \ottdefnisSubKind{}
356
357 \subsection{Roles}
358 \label{sec:tyconroles}
359
360 During type-checking, role inference is carried out, assigning roles to the
361 arguments of every type constructor. The function $[[tyConRoles]]$ extracts these
362 roles. Also used in other judgments is $[[tyConRolesX]]$, which is the same as
363 $[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to account
364 for potential oversaturation.
365
366 The checks encoded in the following
367 judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
368 when \texttt{-dcore-lint} is set.
369
370 \ottdefncheckValidRoles{}
371
372 \ottdefncheckXXdcXXroles{}
373
374 In the following judgment, the role $[[R]]$ is an \emph{input}, not an output.
375 The metavariable $[[O]]$ denotes a \emph{role context}, as shown here:
376
377 \gram{\ottO}
378
379 \ottdefncheckXXtyXXroles{}
380
381 These judgments depend on a sub-role relation:
382
383 \ottdefnltRole{}
384
385 \subsection{Branched axiom conflict checking}
386 \label{sec:no_conflict}
387
388 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
389 sure that a type family application cannot unify with any previous branch
390 in the axiom. The actual code scans through only those branches that are
391 flagged as incompatible. These branches are stored directly in the
392 $[[axBranch]]$. However, it is cleaner in this presentation to simply
393 check for compatibility here.
394
395 \ottdefncheckXXnoXXconflict{}
396
397 The judgment $[[apart]]$ checks to see whether two lists of types are surely
398 apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
399 ]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
400 \emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
401     // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
402 see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
403 Flattening takes all type family applications and replaces them with fresh variables,
404 taking care to map identical type family applications to the same fresh variable.
405
406 The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
407 It performs a standard unification, returning a substitution upon success.
408
409 \section{Operational semantics}
410
411 \subsection{Disclaimer}
412 GHC does not implement an operational semantics in any concrete form. Most
413 of the rules below are implied by algorithms in, for example, the simplifier
414 and optimizer. Yet, there is no one place in GHC that states these rules,
415 analogously to \texttt{CoreLint.lhs}.
416 Nevertheless, these rules are included in this document to help the reader
417 understand System FC.
418
419 \subsection{The context $[[S]]$}
420 We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
421 recursive group. Its definition is as follows:
422 \[
423 [[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]]
424 \]
425 The presence of the context $[[S]]$ is solely to deal with recursion. If your
426 use of FC does not require modeling recursion, you will not need to track $[[S]]$.
427
428 \subsection{Operational semantics rules}
429
430 \ottdefnstep{}
431
432 \subsection{Notes}
433
434 \begin{itemize}
435 \item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
436 implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
437 for all of the mutually recursive equations. Then, after perhaps many steps,
438 when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
439 in the $[[let]]\ [[rec]]$, the context is popped.
440 \item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
441 lists of arguments: two lists of types and a list of terms. The types passed
442 in are the universally and, respectively, existentially quantified type variables
443 to the constructor. The terms are the regular term arguments stored in an
444 algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
445 \item The rule \ottdrulename{S\_CasePush} is the most complex rule.
446 \begin{itemize}
447 \item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
448 \item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
449 extracts the two types (and their kind) from
450 a coercion. It does not require a typing context, as it does not \emph{check} the
451 coercion, just extracts its types.
452 \item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
453 constructor expressions, the parameters to the constructor are broken into three
454 groups: universally quantified types, existentially quantified types, and terms.
455 \item The substitutions in the last premise to the rule are unusual: they replace
456 \emph{type} variables with \emph{coercions}. This substitution is called lifting
457 and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
458 essentially a pun on the fact that types and coercions have such similar structure.
459 \item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
460 types---do not change during this step.
461 \end{itemize}
462 \end{itemize}
463
464 \end{document}