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