1 \documentclass{article}
3 \usepackage{supertabular}
4 \usepackage{amsmath}
5 \usepackage{amssymb}
6 \usepackage{stmaryrd}
7 \usepackage{xcolor}
8 \usepackage{fullpage}
9 \usepackage{multirow}
10 \usepackage{url}
12 \newcommand{\ghcfile}[1]{\textsl{#1}}
13 \newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
15 \input{CoreOtt}
17 % increase spacing between rules for ease of reading:
251 \subsection{Binding consistency}
253 \ottdefnlintXXbind{}
255 \ottdefnlintSingleBinding{}
257 In the GHC source, this function contains a number of other checks, such
258 as for strictness and exportability. See the source code for further information.
260 \subsection{Expression typing}
262 \ottdefnlintCoreExpr{}
264 \begin{itemize}
265 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
266 second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
267 to check each substituted type $[[s'i]]$ in a context containing all the types
268 that come before it in the list of bindings. The $[[G'i]]$ are contexts
269 containing the names and kinds of all type variables (and term variables,
270 for that matter) up to the $i$th binding. This logic is extracted from
271 \coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
273 \item There is one more case for $[[G |-tm e : t]]$, for type expressions.
274 This is included in the GHC code but is elided
275 here because the case is never used in practice. Type expressions
276 can only appear in arguments to functions, and these are handled
277 in \ottdrulename{Tm\_AppType}.
279 \item The GHC source code checks all arguments in an application expression
280 all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
281 and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
282 has been unfolded for presentation here.
284 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
285 (scoping) checks.
287 \item The rule for $[[case]]$ statements also checks to make sure that
288 the alternatives in the $[[case]]$ are well-formed with respect to the
289 invariants listed above. These invariants do not affect the type or
290 evaluation of the expression, so the check is omitted here.
292 \item The GHC source code for \ottdrulename{Tm\_Var} contains checks for
293 a dead id and for one-tuples. These checks are omitted here.
294 \end{itemize}
296 \subsection{Kinding}
298 \ottdefnlintType{}
300 \subsection{Kind validity}
302 \ottdefnlintKind{}
304 \subsection{Coercion typing}
306 In the coercion typing judgment, the $\#$ marks are left off the equality
307 operators to reduce clutter. This is not actually inconsistent, because
308 the GHC function that implements this check, \texttt{lintCoercion}, actually
309 returns four separate values (the kind, the two types, and the role), not
310 a type with head $[[(~#)]]$ or $[[(~R#)]]$. Note that the difference between
311 these two forms of equality is interpreted in the rules \ottdrulename{Co\_CoVarCoNom}
312 and \ottdrulename{Co\_CoVarCoRepr}.
314 \ottdefnlintCoercion{}
316 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
317 the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of
318 folding the substitution over the kinds for kind-checking.
320 See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
321 see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
323 \subsection{Name consistency}
325 There are two very similar checks for names, one declared as a local function:
327 \ottdefnlintSingleBindingXXlintBinder{}
329 \ottdefnlintBinder{}
331 \subsection{Substitution consistency}
333 \ottdefncheckTyKind{}
335 \subsection{Case alternative consistency}
337 \ottdefnlintCoreAlt{}
339 \subsection{Telescope substitution}
341 \ottdefnapplyTys{}
343 \subsection{Case alternative binding consistency}
345 \ottdefnlintAltBinders{}
347 \subsection{Arrow kinding}
349 \ottdefnlintArrow{}
351 \subsection{Type application kinding}
353 \ottdefnlintXXapp{}
355 \subsection{Sub-kinding}
357 \ottdefnisSubKind{}
359 \subsection{Roles}
360 \label{sec:tyconroles}
362 During type-checking, role inference is carried out, assigning roles to the
363 arguments of every type constructor. The function $[[tyConRoles]]$ extracts these
364 roles. Also used in other judgments is $[[tyConRolesX]]$, which is the same as
365 $[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to account
366 for potential oversaturation.
368 The checks encoded in the following
369 judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
370 when \texttt{-dcore-lint} is set.
372 \ottdefncheckValidRoles{}
374 \ottdefncheckXXdcXXroles{}
376 In the following judgment, the role $[[R]]$ is an \emph{input}, not an output.
377 The metavariable $[[O]]$ denotes a \emph{role context}, as shown here:
379 \gram{\ottO}
381 \ottdefncheckXXtyXXroles{}
383 These judgments depend on a sub-role relation:
385 \ottdefnltRole{}
387 \subsection{Branched axiom conflict checking}
388 \label{sec:no_conflict}
390 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
391 sure that a type family application cannot unify with any previous branch
392 in the axiom. The actual code scans through only those branches that are
393 flagged as incompatible. These branches are stored directly in the
394 $[[axBranch]]$. However, it is cleaner in this presentation to simply
395 check for compatibility here.
397 \ottdefncheckXXnoXXconflict{}
399 The judgment $[[apart]]$ checks to see whether two lists of types are surely
400 apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i /> 401 ]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
402 \emph{patterns} (as in a type family equation), first flattens the $[[ </ ti 403 // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
404 see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
405 Flattening takes all type family applications and replaces them with fresh variables,
406 taking care to map identical type family applications to the same fresh variable.
408 The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
409 It performs a standard unification, returning a substitution upon success.
411 \section{Operational semantics}
413 \subsection{Disclaimer}
414 GHC does not implement an operational semantics in any concrete form. Most
415 of the rules below are implied by algorithms in, for example, the simplifier
416 and optimizer. Yet, there is no one place in GHC that states these rules,
417 analogously to \texttt{CoreLint.lhs}.
418 Nevertheless, these rules are included in this document to help the reader
419 understand System FC.
421 \subsection{The context $[[S]]$}
422 We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
423 recursive group. Its definition is as follows:
424 $425 [[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]] 426$
427 The presence of the context $[[S]]$ is solely to deal with recursion. If your
428 use of FC does not require modeling recursion, you will not need to track $[[S]]$.
430 \subsection{Operational semantics rules}
432 \ottdefnstep{}
434 \subsection{Notes}
436 \begin{itemize}
437 \item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
438 implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
439 for all of the mutually recursive equations. Then, after perhaps many steps,
440 when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
441 in the $[[let]]\ [[rec]]$, the context is popped.
442 \item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
443 lists of arguments: two lists of types and a list of terms. The types passed
444 in are the universally and, respectively, existentially quantified type variables
445 to the constructor. The terms are the regular term arguments stored in an
446 algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
447 \item The rule \ottdrulename{S\_CasePush} is the most complex rule.
448 \begin{itemize}
449 \item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
450 \item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
451 extracts the two types (and their kind) from
452 a coercion. It does not require a typing context, as it does not \emph{check} the
453 coercion, just extracts its types.
454 \item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
455 constructor expressions, the parameters to the constructor are broken into three
456 groups: universally quantified types, existentially quantified types, and terms.
457 \item The substitutions in the last premise to the rule are unusual: they replace
458 \emph{type} variables with \emph{coercions}. This substitution is called lifting
459 and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
460 essentially a pun on the fact that types and coercions have such similar structure.
461 \item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
462 types---do not change during this step.
463 \end{itemize}
464 \end{itemize}
466 \end{document}