behavior as precisely as possible. Working notes scattered throughout indicate
areas where further work is needed. Constructive comments are very welcome,
both on the presentation, and on ways in which GHC could be improved in order
-to simplify the Core story.} The definition includes a formal grammar and an informal semantics.
+to simplify the Core story.
+
+Support for generating external Core (post-optimization) was originally introduced in
+GHC 5.02. The definition of external Core in this document reflects the version of
+external Core generated by the HEAD (unstable) branch of GHC as of May 3, 2008 (version 6.9), , using the compiler flag
+@-fext-core@. We expect that GHC 6.10 will be consistent with this definition.}} The definition includes a formal grammar and an informal semantics.
An executable typechecker and interpreter (in Haskell),
which formally embody the static and dynamic semantics,
are available separately.
Core resembles a subset of Haskell, but with explicit type annotations
in the style of the polymorphic lambda calculus (F$_\omega$).
-GHC's front-end translates full Haskell 98 (plus some extensions) into Core. The GHC optimizer then repeatedly transforms Core programs while preserving their meaning. A ``Core Lint'' pass in GHC typechecks Core in between transformation passes (at least when the user enables linting by setting a compiler flag), verifying that transformations preserve type-correctness.\footnote{At least for source programs that do not use unsafe language extensions.} Finally, GHC's back-end translates Core into STG-machine code~\citep{stg-machine} and then into
+GHC's front-end translates full Haskell 98 (plus some extensions) into Core. The GHC optimizer then repeatedly transforms Core programs while preserving their meaning. A ``Core Lint'' pass in GHC typechecks Core in between transformation passes (at least when the user enables linting by setting a compiler flag), verifying that transformations preserve type-correctness. Finally, GHC's back-end translates Core into STG-machine code~\citep{stg-machine} and then into
C or native code.
Two existing papers discuss the original rationale for the design and use of Core~\citep{ghc-inliner,comp-by-trans-scp}, although the (two different)
Researchers interested in writing just {\it part} of a Haskell compiler,
-such as a new back-end or a new optimizer pass, might like to make
-use of GHC to provide the other parts of the compiler. For example, they
+such as a new back-end or a new optimizer pass, might like to use GHC to provide the other parts of the compiler. For example, they
might like to use GHC's front-end to parse, desugar, and type-check source Haskell,
-then feeding the resulting code to their own back-end tool. As another example, they might like to use Core as the target language for a front-end compiler of their own design, feeding externally synthesized Core into GHC in order to take advantage of GHC's optimizer, code generator, and run-time system. Without external Core, there are two ways to do this: link their code into the
-GHC executable, which is an arduous process (and essentially requires
-the new code to be written in Haskell), or use the GHC API~\citep{ghc-api}, which is a cleaner way of doing the same thing (but also requires new code to be written in Haskell).
+then feeding the resulting code to their own back-end tool. As another example, they might like to use Core as the target language for a front-end compiler of their own design, feeding externally synthesized Core into GHC in order to take advantage of GHC's optimizer, code generator, and run-time system. Without external Core, there are two ways for compiler writers to do this: they can link their code into the
+GHC executable, which is an arduous process, or they can use the GHC API~\citep{ghc-api} to do the same task more cleanly. Both ways require new code to be written in Haskell.
-Toward the goal of making it easier for external developers to use GHC in a modular way, we present a precisely specified external format for Core files. The external format is text-based and human-readable, to promote interoperability and ease of use.
+We present a precisely specified external format for Core files. The external format is text-based and human-readable, to promote interoperability and ease of use. We hope this format will make it easier for external developers to use GHC in a modular way.
-In the past, Core has had no rigorously defined external representation, though GHC will print out an ad-hoc textual representation of Core if you set certain compiler flags; this representation is intended to be read by people who are debugging the compiler, not by other programs. Making Core into a machine-readable, bi-directional communication format requires:
+It has long been true that GHC prints an ad-hoc textual representation of Core if you set certain compiler flags. But this representation is intended to be read by people who are debugging the compiler, not by other programs. Making Core into a machine-readable, bi-directional communication format requires:
\begin{enumerate}
\item precisely specifying the external format of Core;
(Section~\ref{sec:external}), and
an informal semantics (Section~\ref{sec:informal}).
-Support for generating external Core (post-optimization) was introduced in
-GHC 5.02. The definition of external Core in this document reflects the version of
-external Core generated by the HEAD (unstable) branch of GHC as of April 21, 2008 (version 6.9), using the compiler flag
-@-fext-core@. We expect that GHC 6.10 will be consistent with this definition.
-
-GHC supports many type system extensions; the External Core printer built into GHC only supports some of them. However, External Core should be capable of representing any Haskell 98 program, and may be able to represent programs that require certain type system extensions as well.
+GHC supports many type system extensions; the External Core printer built into GHC only supports some of them. However, External Core should be capable of representing any Haskell 98 program, and may be able to represent programs that require certain type system extensions as well. If a program uses unsupported features, GHC may fail to compile it to Core when the @-fext-core@ flag is set, or GHC may successfully compile it to Core, but the external tools will not be able to typecheck or interpret it.
Formal static and dynamic semantics in the form of an executable typechecker and interpreter
are available separately in the GHC source tree\footnote{\url{http://darcs.haskell.org/ghc}} under @utils/ext-core@.
\multicolumn{2}{l}{@\%module@ mident \many{tdef @;@} \many{vdefg @;@}} \\
\\
{\rm Type defn.} & tdef & \derives & @%data@ qtycon \many{tbind} @=@ @{@ \optional{cdef \many{@;@ cdef}} @}@ & {\rm algebraic type}\\
- & & \orderives & @%newtype@ qtycon qtycon \many{tbind} \optional{@=@ ty} & {\rm newtype} \\
+ & & \orderives & @%newtype@ qtycon qtycon \many{tbind} @=@ ty & {\rm newtype} \\
\\
{\rm Constr. defn.} & cdef & \derives & qdcon \many{@\at@ tbind} \oneormore{aty} \\
\\
\\
{\rm Basic type} & bty & \derives & aty & {\rm atomic type}\\
& & \orderives & bty aty & {\rm type application}\\
- & & \orderives & @ghczmprim:GHCziPrim.trans@ aty aty & {\rm transitive coercion} \\
- & & \orderives & @ghczmprim:GHCziPrim.sym@ aty & {\rm symmetric coercion} \\
- & & \orderives & @ghczmprim:GHCziPrim.CoUnsafe@ aty aty & {\rm unsafe coercion} \\
- & & \orderives & @ghczmprim:GHCziPrim.left@ aty & {\rm left coercion} \\
- & & \orderives & @ghczmprim:GHCziPrim.right@ aty & {\rm right coercion} \\
- & & \orderives & @ghczmprim:GHCziPrim.inst@ aty aty & {\rm instantiation coercion} \\
+ & & \orderives & @%trans@ aty aty & {\rm transitive coercion} \\
+ & & \orderives & @%sym@ aty & {\rm symmetric coercion} \\
+ & & \orderives & @%unsafe@ aty aty & {\rm unsafe coercion} \\
+ & & \orderives & @%left@ aty & {\rm left coercion} \\
+ & & \orderives & @%right@ aty & {\rm right coercion} \\
+ & & \orderives & @%inst@ aty aty & {\rm instantiation coercion} \\
\\
{\rm Type} & ty & \derives & bty & {\rm basic type}\\
& & \orderives & @%forall@ \oneormore{tbind} @.@ ty & {\rm type abstraction}\\
{\rm Name} & lname & \derives & lower \many{namechar} \\
& uname & \derives & upper \many{namechar} & \\
& pname & \derives & \oneormore{namechar} & \\
- & namechar & \derives & lower \orderives\ upper \orderives\ digit \orderives\ @'@ \\
+ & namechar & \derives & lower \orderives\ upper \orderives\ digit \\
& lower & \derives & @a@ \orderives\ @b@ \orderives\ \ldots \orderives\ @z@ \orderives\ @_@ \\
& upper & \derives & @A@ \orderives\ @B@ \orderives\ \ldots \orderives\ @Z@ \\
& digit & \derives & @0@ \orderives\ @1@ \orderives\ \ldots \orderives\ @9@ \\
of local @let@ bindings, algebraic type definitions, constructors, and @case@ expressions,
and primitive types, literals and operators. Its type system is richer than that of System F, supporting explicit type equality coercions and type functions.~\citep{system-fc}
-We hope no further elaboration is necessary to informally understand Core programs. Therefore, in this section we concentrate on the less obvious points.
+In this section we concentrate on the less obvious points about Core.
\subsection{Program Organization and Modules}
\label{sec:modules}
Core programs are organized into {\em modules}, corresponding directly to source-level Haskell modules.
-Each module has a identifying name {\it mident}. A module identifier consists of a {\it package name} followed by a module name, which may be hierarchical: for example, @base:GHC.Base@ is the module identifier for GHC's Base module. Its name is @Base@, and it lives in the @GHC@ hierarchy within the @base@ package. Section 5.8 of the GHC users' guide explains package names~\citep{ghc-user-guide}. In particular, note that a Core program may contain multiple modules with the same (possibly hierarchical) module name that differ in their package names. In some of the code examples that follow, we will omit package names and possibly full hierarchical module names from identifiers for brevity, but be aware that they are always required.
-
-A possible improvement to the Core syntax would be to add explicit import lists to Core modules, which could be used to specify abbrevations for long qualified names. This would make the code more human-readable.
+Each module has a identifying name {\it mident}. A module identifier consists of a {\it package name} followed by a module name, which may be hierarchical: for example, @base:GHC.Base@ is the module identifier for GHC's Base module. Its name is @Base@, and it lives in the @GHC@ hierarchy within the @base@ package. Section 5.8 of the GHC users' guide explains package names~\citep{ghc-user-guide}. In particular, note that a Core program may contain multiple modules with the same (possibly hierarchical) module name that differ in their package names. In some of the code examples that follow, we will omit package names and possibly full hierarchical module names from identifiers for brevity, but be aware that they are always required.\footnote{A possible improvement to the Core syntax would be to add explicit import lists to Core modules, which could be used to specify abbrevations for long qualified names. This would make the code more human-readable.}
Each module may contain the following kinds of top-level declarations:
\begin{itemize}
No type constructor, data constructor, or top-level value may be declared more than once within a given module.
All the type declarations are (potentially) mutually recursive. Value declarations must be
-in dependency order, with explicit grouping of mutually recursive declarations.
+in dependency order, with explicit grouping of potentially mutually recursive declarations.
Identifiers defined in top-level declarations may be {\it external} or {\it internal}.
\subsubsection{Coercions}
-A type may also be built using one of the primitive coercion operators, as described in Section~\ref{sec:namespaces}. For details on the meanings of these operators, see the System FC paper~\citep{system-fc}.
+A type may also be built using one of the primitive coercion operators, as described in Section~\ref{sec:namespaces}. For details on the meanings of these operators, see the System FC paper~\citep{system-fc}. Also see Section~\ref{sec:newtypes} for examples of how GHC uses coercions in Core code.
\subsubsection{Kinds}
As described in the Haskell definition, it is necessary to distinguish
-well-formed type-expressions by classifying them into different {\it kinds}~\citep[41]{haskell98}.
+well-formed type-expressions by classifying them into different {\it kinds}~\citep[p. 41]{haskell98}.
In particular, Core explicitly records the kind of every bound type variable.
In addition, Core's kind system includes equality kinds, as in System FC~\citep{system-fc}. An application of a built-in coercion, or of a user-defined coercion as introduced by a newtype declaration, has an equality kind.
\begin{itemize}
\item alpha-renaming of variables bound in @%forall@ types;
\item the identity $a$ @->@ $b$ $\equiv$ @ghc-prim:GHC.Prim.ZLzmzgZR@ $a$ $b$
-\item the substitution of representation types for {\it fully applied} instances of newtypes
-(see Section~\ref{sec:newtypes}).
\end{itemize}
\subsection{Algebraic data types}
\subsection{Newtypes}
\label{sec:newtypes}
-Each Core @%newtype@ declaration introduces a new type constructor and (usually) an associated
+Each Core @%newtype@ declaration introduces a new type constructor and an associated
representation type, corresponding to a source Haskell @newtype@
declaration. However, unlike in source Haskell, a @%newtype@ declaration does not introduce any data constructors.
\begin{code}
%newtype U ZCCoU = Bool;
u :: U = %cast (True)
- ((sym ZCCoU));
+ ((%sym ZCCoU));
v :: Bool = not (%cast (u) ZCCoU);
\end{code}
-The newtype declaration implies that the types {\tt U} and {\tt Bool} have equivalent representations, and the coercion axiom {\tt ZCCoU} provides evidence. Notice that in the body of {\tt u}, the boolean value {\tt True} is cast to type {\tt U} using the primitive symmetry rule applied to {\tt ZCCoU}: that is, using a coercion of kind {\tt Bool :=: U}. And in the body of {\tt v}, {\tt u} is cast back to type {\tt Bool} using the axiom {\tt ZCCoU}.
+The newtype declaration implies that the types {\tt U} and {\tt Bool} have equivalent representations, and the coercion axiom {\tt ZCCoU} provides evidence that {\tt U} is equivalent to {\tt Bool}. Notice that in the body of {\tt u}, the boolean value {\tt True} is cast to type {\tt U} using the primitive symmetry rule applied to {\tt ZCCoU}: that is, using a coercion of kind {\tt Bool :=: U}. And in the body of {\tt v}, {\tt u} is cast back to type {\tt Bool} using the axiom {\tt ZCCoU}.
-Very rarely, source @newtype@ declarations may be (directly or indirectly) recursive. In such
-cases, it is not possible to substitute the representation type for the new type;
-in fact, the representation type is omitted from the corresponding Core @%newtype@ declaration. Otherwise, recursive newtypes are handled in the same way as non-recursive newtypes.
+Notice that the {\tt case} in the Haskell source code above translates to a {\tt cast} in the corresponding Core code. That is because operationally, a {\tt case} on a value whose type is declared by a {\tt newtype} declaration is a no-op. Unlike a {\tt case} on any other value, such a {\tt case} does no evaluation: its only function is to coerce its scrutinee's type.
+Also notice that unlike in a previous draft version of External Core, there is no need to handle recursive newtypes specially.
\subsection{Expression Forms}
\label{sec:exprs}
\end{code}
Value applications may be of user-defined functions, data constructors, or primitives.
-None of these sorts of applications are necessarily saturated (although previously published variants
-of Core did require the latter two sorts to be).
+None of these sorts of applications are necessarily saturated.
Note that the arguments of type applications are not always of kind @*@. For example,
given our previous definition of type @A@:
\end{code}
Local bindings, of a single variable or of a set of mutually recursive variables,
-are represented by @%let@ expressions in the usual way. In Core, @%let@ is also significant it maps directly on to the STG language's @let@ construct: in STG, evaluating a @%let@ allocates closures for the variable(s) being bound~\citep[29]{stg-machine}.
+are represented by @%let@ expressions in the usual way.
By far the most complicated expression form is @%case@.
@%case@ expressions are permitted over values of any type, although they will normally
tested (the ``scrutinee''). The value of the scrutinee is bound to the variable
following the @%of@ keyword, which is in scope in all alternatives;
this is useful when the scrutinee is a non-atomic
-expression (see next example). The scrutinee is preceded by the type of the entire @%case@ expression: that is, the result type that all of the @%case@ alternatives have (this is intended to make type reconstruction in the presence of type equality coercions easier).
+expression (see next example). The scrutinee is preceded by the type of the entire @%case@ expression: that is, the result type that all of the @%case@ alternatives have (this is intended to make type reconstruction easier in the presence of type equality coercions).
In an algebraic @%case@, all the case alternatives must be
labeled with distinct data constructors from the algebraic type, followed by
none of the other alternatives match. The default is optional except for in a case
over a primitive type, or when there are no other alternatives.
If the case is over neither an
-algebraic type nor a primitive type, then the list of alternative must contain a default alternative and nothing else.
+algebraic type nor a primitive type, then the list of alternatives must contain a default alternative and nothing else.
For algebraic cases, the set of alternatives
need not be exhaustive, even if no default is given; if alternatives are missing,
this implies that GHC has deduced that they cannot occur.
-The @%cast@ expression takes an expression and a coercion:
+@%cast@ is used to manipulate newtypes, as described in Section~\ref{sec:newtypes}. The @%cast@ expression takes an expression and a coercion:
syntactically, the coercion is an arbitrary type, but it must have an
equality kind. In an expression @(cast e co)@, if @e :: T@ and @co@
has kind @T :=: U@, then the overall expression has type
-@U@~\citep{ghc-fc-commentary}. If @co@ has a non-coercion kind or a
-coercion whose left-hand side is not @T@, that is a type error.
+@U@~\citep{ghc-fc-commentary}. Here, @co@ must be a coercion whose left-hand side is @T@.
Note
that unlike the @%coerce@ expression that existed in previous versions
argument provides evidence that can be verified by a
typechecker. There are still unsafe @%cast@s, corresponding to the
unsafe @%coerce@ construct that existed in old versions of Core,
-because there is a primitive @ghc-prim:GHC.Prim.CoUnsafe@ coercion type that
+because there is a primitive unsafe coercion type that
can be used to cast arbitrary types to each other. GHC uses this for
such purposes as coercing the return type of a function (such as
error) which is guaranteed to never return:
becomes:
\begin{code}
%cast (error @ Bool (ZMZN @ Char))
- (GHC.Prim.CoUnsafe Bool Integer);
+ (%unsafe Bool Integer);
\end{code}
@%cast@ has no operational meaning and is only used in typechecking.
-@%cast@ is also used to manipulate newtypes, as described in Section~\ref{sec:newtypes}.
+
A @%note@ expression carries arbitrary internal information that GHC finds interesting. The information is encoded as a string. Expression notes currently generated by GHC
include the inlining pragma (@InlineMe@) and cost-center labels for profiling.
A @%external@ expression denotes an external identifier, which has
-the indicated type (always expressed in terms of Haskell primitive types).\footnote{External Core supports two kinds of external calls: \%external and \%dynexternal. Only the former is supported by the current set of stand-alone Core tools. In addition, there is a \%label construct which GHC may generate but which the Core tools do not support.}
+the indicated type (always expressed in terms of Haskell primitive types). External Core supports two kinds of external calls: @%external@ and @%dynexternal@. Only the former is supported by the current set of stand-alone Core tools. In addition, there is a @%label@ construct which GHC may generate but which the Core tools do not support.
The present syntax for externals is sufficient for describing C functions and labels.
Interfacing to other languages may require additional information or a different interpretation
In the remainder of this section, we use ``Core'' to mean ``well-behaved'' Core.
Evaluating a Core expression means reducing it to {\it weak-head normal form (WHNF)},
-i.e., a primitive value, lambda abstraction, or fully-applied data constructor. To evaluate a program means evaluating the expression @Main.main@.
+i.e., a primitive value, lambda abstraction, or fully-applied data constructor. Evaluating a program means evaluating the expression @main:ZCMain.main@.
To make sure that expression evaluation is shared, we
make use of a {\it heap}, which contains {\it heap entries}. A heap entry can be:
\item A {\em WHNF}, representing an evaluated expression. The result of evaluating a thunk is a WHNF. A WHNF is always a closure (corresponding to a lambda abstraction in the source program) or a data constructor application: computations over primitive types are never suspended.
\end{itemize}
-{\it Heap pointers} point to heap entries: the same heap pointer can point to either a thunk or a WHNF, because the run-time system overwrites thunks with WHNFs as computation proceeds.
+{\it Heap pointers} point to heap entries: at different times, the same heap pointer can point to either a thunk or a WHNF, because the run-time system overwrites thunks with WHNFs as computation proceeds.
The suspended computation that a thunk represents might represent evaluating one of three different kinds of expression. The run-time system allocates a different kind of thunk depending on what kind of expression it is:
\begin{itemize}
\end{itemize}
As computation proceeds, copies of the heap pointer for a given thunk propagate through the executing program.
-When another computation demands the result of that thunk, the run-time system computes the thunk's result, yielding a WHNF, and overwrites the heap entry for the thunk with the WHNF. Now, all copies of the heap pointer point to the new heap entry: a WHNF. Forcing occurs
+When another computation demands the result of that thunk, the thunk is {\it forced}: the run-time system computes the thunk's result, yielding a WHNF, and overwrites the heap entry for the thunk with the WHNF. Now, all copies of the heap pointer point to the new heap entry: a WHNF. Forcing occurs
only in the context of
\begin{itemize}
\item evaluating the operator expression of an application;
projects / ghc-hetmet.git / commitdiff