+++ /dev/null
-\documentclass[10pt]{article}
-\usepackage{a4wide}
-\usepackage{code}
-
-
-\sloppy
-\setlength{\parskip}{0.5\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip}
-\setlength{\parsep}{\parskip}
-\setlength{\topsep}{0cm}
-\setlength{\parindent}{0cm}
-%\oddsidemargin -0.5 in
-%\evensidemargin -0.5 in
-%\textwidth 7.375 in
-
-\newcommand{\derives}{\mbox{$\rightarrow$}}
-\newcommand{\orderives}{\mbox{$\mid$}}
-\newcommand{\many}[1]{\{ {#1} \}}
-\newcommand{\oneormore}[1]{\{ {#1} \}$^{+}$}
-\newcommand{\optional}[1]{[ {#1} ]}
-
-\newcommand{\at}{\texttt{@}}
-\newcommand{\att}{@}
-\newcommand{\lam}{\texttt{\char`\\}}
-
-\newcommand{\workingnote}[1]%
- {\begin{quote}
- \framebox{\parbox{.8 \linewidth}
- {\textbf{\textsl{Working note:}} \textsl{#1}}}
- \end{quote}}
-
-\begin{document}
-
-\title{An External Representation for the GHC Core Language (DRAFT for GHC5.02)}
-\author{Andrew Tolmach ({\tt apt@cs.pdx.edu})\\and The GHC Team}
-
-\maketitle
-\makeatactive
-
-\abstract{
-This document provides a precise definition for the GHC Core language,
-so that it can be used to communicate between GHC and new stand-alone
-compilation tools such as back-ends or optimizers.
-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.
-
-Note: This is a draft document, which attempts to describe GHC's current
-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.
-}
-
-\section{Introduction}
-
-The Glasgow Haskell Compiler (GHC) uses an intermediate language, called
-``Core,'' as its internal program representation during
-several key stages of compiling.
-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
-well-typed Core, which is then repeatedly rewritten by the GHC optimizer.
-Ultimately, GHC translates Core into STG-machine code and then into
-C or native code. The rationale for the design of Core and its use are discussed
-in existing papers~\cite{ghc-inliner,comp-by-trans-scp}, although the (two different)
-idealized versions of Core described therein differ in significant ways
-from the actual Core language in current GHC.
-
-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
-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.
-Currently, they can only do this by linking their code into the
-GHC executable, which is an arduous process (and essentially requires
-the new code to be written in Haskell). It would be much easier for
-external developers if GHC could be made to produce Core files in
-an agreed-upon external format. To allow the widest range of interoperability,
-the external format should be text-based; pragmatically, it should
-also be human-readable. (It may ultimately be desirable to use a
-standard interchange base format such as ASDL or XML.)
-
-In the past, Core has had no rigorously defined external representation, although
-by setting certain compiler flags, one can get a (rather ad-hoc) textual
-representation to be printed at various points in the compilation process;
-this is usually done to help debug the compiler. To make Core fully useable
-a bi-directional communication format, it will be necssary to
-
-\begin{enumerate}
-\item define precisely the external format of Core;
-
-\item modify GHC to produce external Core files, if so requested, at one or more
-useful points in the compilation sequence -- e.g., just before optimization,
-or just after;
-
-\item modify GHC to accept external Core files in place of Haskell
-source files, again at one or more useful points.
-
-\end{enumerate}
-
-The first two facilities will let one couple GHC's front-end (parser,
-type-checker, etc.), and optionally its optimizer, with new back-end tools.
-Adding the last facility will let one implement new Core-to-Core
-transformations in an external tool and integrate them into GHC. It will also
-allow new front-ends to generate Core that can be fed into GHC's optimizer or
-back end; however, because there are many (undocumented)
-idiosynracies in the way GHC produces Core from source Haskell, it will be hard
-for an external tool to produce Core that can be integrated with GHC-produced core
-(e.g., for the Prelude), and we don't aim to support this.
-
-This document addresses the first requirement, a formal Core definition,
-by proposing a formal grammar for an external representation of Core
-(Section~\ref{sec:external}, and
-an informal semantics (Section~\ref{sec:informal}.
-
-Beginning in GHC5.02, external Core (post-optimization) adhering to this definition
-can be generated using the compiler flag @-fext-core@.
-
-Formal static and dynamic semantics in the form of an executable typechecker and interpreter
-are available separately in the GHC source tree under @fptools/ghc/utils/ext-core@.
-
-\section{External Grammar of Core}
-\label{sec:external}
-
-In designing the external grammar, we have tried to strike a balance among
-a number of competing goals, including easy parseability by machines,
-easy readability by humans, and adequate structural simplicity to
-allow straightforward presentations of the semantics. This has inevitably
-led to certain compromise. In particular:
-
-\begin{itemize}
-\item In order to avoid explosion of parentheses, various standard precedences
-and short-cuts are supported for expressions, types, and kinds; this led to the introduction
-of multiple non-terminals for each of these syntactic categories, which
-makes the concrete grammar longer and more complex than the underlying abstract syntax.
-
-\item On the other hand, the grammar has been kept simpler by avoiding special syntax for
-tuple types and terms; tuples (both boxed and unboxed) are treated
-as ordinary constructors.
-
-\item All type abstractions and applications are given in full, even though
-some of them (e.g., for tuples) could be reconstructed; this permits Core to
-be parsed without the necessity of performing any type reconstruction.
-
-\item The syntax of identifiers is heavily restricted (essentially to just
-alphanumerics); this again makes Core easier to parse but harder to read.
-\end{itemize}
-
-\workingnote{These choices are certainly debatable. In particular, keeping
-type applications on tuples and case arms considerably increases the size of core files and
-makes them less human-readable, though it allows a Core parser to be simpler.}
-
-We use the following notational conventions for syntax:
-
-\begin{tabular}{ll}
-{\it [ pat ]} & optional \\
-{\it \{ pat \}} & zero or more repetitions \\
-{\it \{ pat \}$^{+}$} & one or more repetitions \\
-{\it pat$_1$ \orderives\ pat$_2$} & choice \\
-@fibonacci@ & terminal syntax in typewriter font \\
-\end{tabular}
-
-{\it
-\begin{tabular}{lrclr}
-{\rm Module} & module & \derives &
- \multicolumn{2}{l}{@\%module@ mident \many{tdef @;@} \many{\optional{@\%local@} vdefg @;@}} \\
-\\
-{\rm Type defn.} & tdef & \derives & @%data@ qtycon \many{tbind} @=@ @{@ cdef \many{@;@ cdef} @}@ & {\rm algebraic type}\\
- & & \orderives & @%newtype@ qtycon \many{tbind} \optional{@=@ ty} & {\rm newtype} \\
-\\
-{\rm Constr. defn.} & cdef & \derives & qdcon \many{@\at@ tbind} \many{aty} \\
-\\
-{\rm Value defn.} & vdefg & \derives & @%rec@ @{@ vdef \many{@;@ vdef} @}@ & {\rm recursive} \\
- & & \orderives & vdef & {\rm non-recursive} \\
- & vdef & \derives & qvar @::@ ty @=@ exp & \\
-\\
-{\rm Atomic expr.} & aexp & \derives & qvar & {\rm variable} \\
- & & \orderives & qdcon & {\rm data constructor}\\
- & & \orderives & lit & {\rm literal} \\
- & & \orderives & @(@ exp @)@ & {\rm nested expr.}\\
-\\
-{\rm Expression} & exp & \derives & aexp & {\rm atomic expresion}\\
- & & \orderives & aexp \oneormore{arg} & {\rm application}\\
- & & \orderives & @\@ \oneormore{binder} @->@ exp & {\rm abstraction}\\
- & & \orderives & @%let@ vdefg @%in@ exp & {\rm local definition}\\
- & & \orderives & @%case@ exp @%of@ vbind @{@ alt \many{@;@ alt} @}@ & {\rm case expression}\\
- & & \orderives & @%coerce@ aty exp & {\rm type coercion}\\
- & & \orderives & @%note@ @"@ \many{char} @"@ exp & {\rm expression note}\\
- & & \orderives & @%external@ @"@ \many{char} @"@ aty & {\rm external reference}\\
-\\
-{\rm Argument} & arg & \derives & \at\ aty & {\rm type argument}\\
- & & \orderives & aexp & {\rm value argument} \\
-\\
-{\rm Case alt.} & alt & \derives & qdcon \many {@\at@ tbind} \many{vbind} @->@ exp &{\rm constructor alternative}\\
- & & \orderives & lit @->@ exp & {\rm literal alternative} \\
- & & \orderives & @%_@ @->@ exp & {\rm default alternative} \\
-\\
-{\rm Binder} & binder & \derives & \at\ tbind & {\rm type binder}\\
- & & \orderives & vbind & {\rm value binder}\\
-\\
-{\rm Type binder} & tbind & \derives & tyvar & {\rm implicitly of kind @*@} \\
- & & \orderives & @(@ tyvar @::@ kind @)@ & {\rm explicitly kinded} \\
-\\
-{\rm Value binder} & vbind & \derives & @(@ var @::@ ty @)@ \\
-\\
-{\rm Literal} & lit & \derives & @(@ [@-@] \oneormore{digit} @::@ ty @)@ & {\rm integer} \\
- & & \orderives & @(@ [@-@] \oneormore{digit} @.@ \oneormore{digit} @::@ ty @)@ & {\rm rational} \\
- & & \orderives & @(@ @'@ char @'@ @::@ ty @)@ & {\rm character} \\
- & & \orderives & @(@ @"@ \many{char} @"@ @::@ ty @)@ & {\rm string} \\
-\\
-{\rm Character} & char & \derives & \multicolumn{2}{l}{any ASCII character in range 0x20-0x7E except 0x22,0x27,0x5c}\\
- & & \orderives & @\x@ hex hex & {\rm ASCII code escape sequence} \\
- & hex & \derives & @0@ \orderives \ldots \orderives @9@ \orderives @a@ \orderives \ldots \orderives @f@ \\
-\end{tabular}
-
-\begin{tabular}{lrclr}
-{\rm Atomic type} & aty & \derives & tyvar & {\rm type variable} \\
- & & \orderives & qtycon & {\rm type constructor}\\
- & & \orderives & @(@ ty @)@ & {\rm nested type}\\
-\\
-{\rm Basic type} & bty & \derives & aty & {\rm atomic type}\\
- & & \orderives & bty aty & {\rm type application}\\
-\\
-{\rm Type} & ty & \derives & bty & {\rm basic type}\\
- & & \orderives & @%forall@ \oneormore{tbind} @.@ ty & {\rm type abstraction}\\
- & & \orderives & bty @->@ ty & {\rm arrow type construction} \\
-\\
-{\rm Atomic kind} & akind & \derives & @*@ & {\rm lifted kind}\\
- & & \orderives & @#@ & {\rm unlifted kind}\\
- & & \orderives & @?@ & {\rm open kind}\\
- & & \orderives & @(@ kind @)@& {\rm nested kind}\\
-\\
-{\rm Kind} & kind & \derives & akind & {\rm atomic kind}\\
- & & \orderives & akind @->@ kind & {\rm arrow kind} \\
-\\
-{\rm Identifier} & mident & \derives &uname & {\rm module} \\
- & tycon & \derives & uname & {\rm type constr.} \\
- & qtycon & \derives & mident @.@ tycon & {\rm qualified type constr.} \\
- & tyvar & \derives & lname & {\rm type variable} \\
- & dcon & \derives & uname & {\rm data constr.} \\
- & qdcon & \derives & mident @.@ dcon & {\rm qualified data constr.} \\
- & var & \derives & lname & {\rm variable} \\
- & qvar & \derives & [ mident @.@ ] var & {\rm optionally qualified variable} \\
-\\
-{\rm Name} & lname & \derives & lower \many{namechar} \\
- & uname & \derives & upper \many{namechar} & \\
- & namechar & \derives & lower \orderives\ upper \orderives\ digit \orderives\ @'@ \\
- & 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@ \\
-\\
-\end{tabular}
-}
-
-\workingnote{Should add some provision for comments.}
-
-\section{Informal Semantics}
-\label{sec:informal}
-
-Core resembles a explicitly-typed polymorphic lambda calculus (F$_\omega$), with the addition
-of local @let@ bindings, algebraic type definitions, constructors, and @case@ expressions,
-and primitive types, literals and operators.
-It is hoped that this makes it easy to obtain an informal understanding of Core programs
-without elaborate description. This section therefore concentrates on the less obvious points.
-
-\subsection{Program Organization and Modules}
-
-Core programs are organized into {\em modules}, corresponding directly to source-level Haskell modules.
-Each module has a identifying name {\it mident}.
-
-Each module may contain the following kinds of top-level declarations:
-\begin{itemize}
-\item Algebraic data type declarations, each defining a type constructor and one or more data constructors;
-\item Newtype declarations, corresponding to Haskell @newtype@ declarations, each defining a type constructor; and
-\item Value declarations, defining the types and values of top-level variables.
-\end{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.
-
-Identifiers defined in top-level declarations may be {\it external} or {\it internal}.
-External identifiers can be referenced from any other module in
-the program, using conventional dot notation (e.g., @PrelBase.Bool@, @PrelBase.True@).
-Internal identifiers are visible only within the defining module.
-All type and data constructors are external, and are always defined and referenced using
-fully qualified names (with dots). A top-level value is external if it is defined and referenced
-using a fully qualified name with a dot (e.g., @MyModule.foo = ...@); otherwise, it is internal
-(e.g., @bar = ...@).
-Note that the notion of external identifier does not necessarily coincide with that of ``exported''
-identifier in a Haskell source module: all constructors are external, even if not exported, and
-non-exported values may be external if they are referenced from potentially in-lineable exported values.
-Core modules have no explicit import or export lists.
-Modules may be mutually recursive.
-
-\workingnote{But in the presence of inter-module recursion, is there much point in
-keeping track of recursive groups within modules? Options: (1) don't worry about it;
-(2) put all declarations in module (indeed whole program) into one huge recursive pot;
-(3) abandon general module recursion, and introduce some kind of import declaration to define the
-types (only) of things from external modules that currently introduce module recursion.}
-
-There is also an implicitly-defined module @PrelGHC@, which exports the ``built-in'' types and values
-that must be provided by any implementation of Core (including GHC). Details of this
-module are in Section~\ref{sec:prims}.
-
-A Core {\em program} is a collection of distinctly-named modules that includes a module
-called @Main@ having an exported value called @main@ of type @PrelIOBase.IO a@ (for some type @a@).
-
-Many modules of interest derive from library modules, such as @PrelBase@, which implement parts of
-the Haskell basis library. In principle, these modules have no special status. In practice, the
-requirement on the type of @Main.main@ implies that every program will contain a large subset of
-the Prelude library modules.
-
-\subsection{Namespaces}
-
-There are five distinct name spaces:
-\begin{enumerate}
-\item module identifiers (@mident@),
-\item type constructors (@tycon@),
-\item type variables (@tyvar@),
-\item data constructors (@dcon@),
-\item term variables (@var@).
-\end{enumerate}
-Spaces (1), (2+3), and (4+5) can be distinguished from each other by context.
-To distinguish (2) from (3) and (4) from (5), we require that
-(both sorts of) constructors begin with an upper-case character
-and that (both sorts of) variables begin with a lower-case character (or @_@).
-Primitive types and operators are not syntactically distinguished.
-
-A given variable (type or term) may have multiple (local) definitions within a module.
-However, definitions never ``shadow'' one another; that is, the scope of the definition
-of a given variable never contains a redefinition of the same variable. The only exception
-to this is that (necessarily closed) types labelling @%external@ expressions may contain
-@tyvar@ bindings that shadow outer bindings.
-
-Core generated by GHC makes heavy use of encoded names, in which the characters @Z@ and @z@ are
-used to introduce escape sequences for non-alphabetic characters such as dollar sign @$@ (@zd@),
-hash @#@ (@zh@), plus @+@ (@zp@), etc. This is the same encoding used in @.hi@ files and in the
-back-end of GHC itself, except that we sometimes change an initial @z@ to @Z@, or vice-versa,
-in order to maintain case distinctions.
-
-\subsection{Types and Kinds}
-
-In Core, all type abstractions and applications are explicit. This make it easy to
-typecheck any (closed) fragment. An full executable typechecker is available separately.
-
-Types are described by type expressions, which
-are built from named type constructors and type variables
-using type application and universal quantification.
-Each type constructor has a fixed arity $\geq 0$.
-Because it is so widely used, there is
-special infix syntax for the fully-applied function type constructor (@->@).
-(The prefix identifier for this constructor is @PrelGHC.ZLzmzgZR@; this should
-only appear in unapplied or partially applied form.)
-There are also a number of other primitive type constructors (e.g., @Intzh@) that
-are predefined in the @PrelGHC@ module, but have no special syntax.
-Additional type constructors are
-introduced by @%data@ and @%newtype@ declarations, as described below.
-Type constructors are distinguished solely by name.
-
-As described in the Haskell definition, it is necessary to distinguish
-well-formed type-expressions by classifying them into different {\it kinds}.
-In particular, Core explicitly records the kind of every bound type variable.
-Base kinds (@*@,@#@, and @?@) represent actual types, i.e., those that can be assigned
-to term variables; all the nullary type constructors have one of these kinds.
-Non-nullary type constructors have higher kinds of the form $k_1 @->@ k_2$,
-where $k_1$ and $k_2$ are kinds. For example, the function type constructor
-@->@ has kind @* -> (* -> *)@. Since Haskell allows abstracting over type
-constructors, it is possible for type variables to have higher kinds; however,
-it is much more common for them to have kind @*@, so this is the default if
-the kind is omitted in a type binder.
-
-The three base kinds distinguish the {\it liftedness} of the types they classify:
-@*@ represents lifted types; @#@ represents unlifted types; and @?@ represents
-``open'' types, which may be either lifted or unlifted. Of these, only @*@ ever
-appears in Core code generated from user code; the other two are needed to describe
-certain types in primitive (or otherwise specially-generated) code.
-Semantically, a type is lifted if and only if it has bottom as an element.
-Operationally, lifted types may be represented by closures; hence, any unboxed
-value is necessarily unlifted.
-In particular, no top-level identifier (except in @PrelGHC@) has a type of kind @#@ or @?@.
-Currently, all the primitive types are unlifted
-(including a few boxed primitive types such as @ByteArrayzh@).
-The ideas behind the use of unboxed and unlifted types are described in ~\cite{pj:unboxed}.
-
-There is no mechanism for defining type synonyms (corresponding to
-Haskell @type@ declarations).
-Type equivalence is just syntactic equivalence on type expressions
-(of base kinds) modulo:
-
-\begin{itemize}
-\item alpha-renaming of variables bound in @%forall@ types;
-\item the identity $a$ @->@ $b$ $\equiv$ @PrelGHC.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}
-
-Each @data@ declaration introduces a new type constructor and a set of one or
-more data constructors, normally corresponding directly to a source Haskell @data@ declaration.
-For example, the source declaration
-\begin{code}
-data Bintree a =
- Fork (Bintree a) (Bintree a)
-| Leaf a
-\end{code}
-might induce the following Core declaration
-\begin{code}
-%data Bintree a = {
- Fork (Bintree a) (Bintree a);
- Leaf a)}
-\end{code}
-which introduces the unary type constructor @Bintree@ of kind @*->*@ and two data constructors with types
-\begin{code}
-Fork :: %forall a . Bintree a -> Bintree a -> Bintree a
-Leaf :: %forall a . a -> Bintree a
-\end{code}
-We define the {\it arity} of each data constructor to be the number of value arguments it takes;
-e.g. @Fork@ has arity 2 and @Leaf@ has arity 1.
-
-For a less conventional example illustrating the possibility of higher-order kinds, the Haskell source declaration
-\begin{code}
-data A f a = MkA (f a)
-\end{code}
-might induce the core declaration
-\begin{code}
-%data A (f::*->*) (a::*) = { MkA (f a) }
-\end{code}
-which introduces the constructor
-\begin{code}
-MkA :: %forall (f::*->*) (a::*) . (f a) -> (A f) a
-\end{code}
-
-
-GHC (like some other Haskell implementations) supports an extension to Haskell98
-for existential types such as
-\begin{code}
-data T = forall a . MkT a (a -> Bool)
-\end{code}
-This is represented by the Core declaration
-\begin{code}
-%data T = {MkT @a a (a -> Bool)}
-\end{code}
-which introduces the nullary type constructor @T@ and the data constructor
-\begin{code}
-MkT :: %forall a . a -> (a -> Bool) -> T
-\end{code}
-In general, existentially quantified variables appear as extra univerally
-quantified variables in the data contructor types.
-An example of how to construct and deconstruct values of type @T@ is shown in
-Section~\ref{sec:exprs}.
-
-\subsection{Newtypes}
-\label{sec:newtypes}
-
-
-Each Core @%newtype@ declaration introduces a new type constructor and (usually) an associated
-representation type, corresponding to a source Haskell @newtype@
-declaration. However, unlike in source Haskell, no data constructors are introduced.
-In fact, newtypes seldom appear in value types
-in Core programs, because GHC usually replaces them with their representation type.
-For example, the Haskell fragment
-\begin{code}
-newtype U = MkU Bool
-u = MkU True
-v = case u of
- MkU b -> not b
-\end{code}
-might induce the Core fragment
-\begin{code}
-%newtype U = Bool;
-u :: Bool = True;
-v :: Bool =
- %let b :: Bool = u
- %in not b;
-\end{code}
-The main purpose of including @%newtype@ declarations in Core is to permit checking of
-type expressions in which partially-applied newtype constructors are used to instantiate higher-kinded
-type variables. For example:
-\begin{code}
-newtype W a = MkW (Bool -> a)
-data S k = MkS (k Bool)
-a :: S W = MkS (MkW(\x -> not x))
-\end{code}
-might generate this Core:
-\begin{code}
-%newtype W a = Bool -> a;
-%data S (k::(*->*)) = MkS (k Bool);
-a :: S W = MkS @ W (\(x::Bool) -> not x)
-\end{code}
-The type application @(S W)@ cannot be checked without a definition for @W@.
-
-Very rarely, source @newtype@ declarations may be (directly or indirectly) recursive. In such
-cases, it is not possible to subsitute the representation type for the new type;
-in fact, the representation type is omitted from the corresponding Core @%newtype@ declaration.
-Elements of the new
-type can only be created or examined by first explicitly coercing them from/to
-the representation type, using a @%coerce@ expression. For example, the silly
-Haskell fragment
-\begin{code}
-newtype U = MkU (U -> Bool)
-u = MkU (\x -> True)
-v = case u of
- MkU f -> f u
-\end{code}
-might induce the Core fragment
-\begin{code}
-%newtype U;
-u :: U = %coerce U (\ (x::U) -> True);
-v :: Bool =
- %let f :: U -> Bool = %coerce (U -> Bool) u
- %in f u;
-\end{code}
-
-\workingnote{The treatment of newtypes is still very unattractive: acres of explanation for
-very rare phenomena.}
-
-\subsection{Expression Forms}
-\label{sec:exprs}
-
-Variables and data constructors are straightforward.
-
-Literal ({\it lit}) expressions consist of a literal value, in one of four different formats,
-and a (primitive) type annotation. Only certain combinations of format and type
-are permitted; see Section~\ref{sec:prims}. The character and string formats can describe only
-8-bit ASCII characters. Moreover, because strings are interpreted as C-style null-terminated
-strings, they should not contain embedded nulls.
-
-Both value applications and type applications are made explicit, and similarly
-for value and type abstractions. To tell them apart, type arguments in applications
-and formal type arguments in abstractions are preceded by an \at\ symbol. (In abstractions,
-the \at\ plays essentially the same role as the more usual $\Lambda$ symbol.)
-For example, the Haskell source declaration
-\begin{code}
-f x = Leaf (Leaf x)
-\end{code}
-might induce the Core declaration
-\begin{code}
-f :: %forall a . a -> BinTree (BinTree a) =
- \ @a (x::a) -> Leaf @(Bintree a) (Leaf @a x)
-\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).
-
-Note that the arguments of type applications are not always of kind @*@. For example,
-given our previous definition of type @A@:
-\begin{code}
-data A f a = MkA (f a)
-\end{code}
-the source code
-\begin{code}
-MkA (Leaf True)
-\end{code}
-becomes
-\begin{code}
-(MkA @Bintree @Bool) (Leaf @Bool True)
-\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.
-
-By far the most complicated expression form is @%case@.
-@%case@ expressions are permitted over values of any type, although they will normally
-be algebraic or primitive types (with literal values).
-Evaluating a @%case@ forces the evaluation of the expression being
-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).
-
-In an algebraic @%case@, all the case alternatives must be
-labeled with distinct data constructors from the algebraic type, followed by
-any existential type variable bindings (see below), and
-typed term variable bindings corresponding to the data constructor's
-arguments. The number of variables must match the data constructor's arity.
-
-For example, the following Haskell source expression
-\begin{code}
-case g x of
- Fork l r -> Fork r l
- t@(Leaf v) -> Fork t t
-\end{code}
-might induce the Core expression
-\begin{code}
-%case g x %of (t::Bintree a)
- Fork (l::Bintree a) (r::Bintree a) ->
- Fork @a r l
- Leaf (v::a) ->
- Fork @a t t
-\end{code}
-
-When performing a @%case@ over a value of an existentially-quantified algebraic
-type, the alternative must include extra local type bindings
-for the existentially-quantified variables. For example, given
-\begin{code}
-data T = forall a . MkT a (a -> Bool)
-\end{code}
-the source
-\begin{code}
-case x of
- MkT w g -> g w
-\end{code}
-becomes
-\begin{code}
-%case x %of (x'::T)
- MkT @b (w::b) (g::b->Bool) -> g w
-\end{code}
-
-In a @%case@ over literal alternatives,
-all the case alternatives must be distinct literals of the same primitive type.
-
-The list of alternatives may begin with a
-default alternative labeled with an underscore (@%_@), which will be chosen if
-none of the other alternative match. The default is optional except for 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, the default alternative is the {\it only}
-one that can appear.
-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 @%coerce@ expression is primarily used in conjunction with manipulation of
-newtypes, as described in Section~\ref{sec:newtypes}.
-However, @%coerce@ is sometimes used for
-other purposes, e.g. to coerce the return type of a function (such as @error@)
-that is guaranteed never to return. By their natures, uses of @%coerce@ cannot
-be independently justified, and must be taken on faith by a type-checker for Core.
-
-A @%note@ expression is used to carry arbitrary internal information of interest to
-GHC. The information must be 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).
-\workingnote{The present syntax is sufficient for describing C functions and labels.
-Interfacing to other languages may require additional information or a different interpretation
-of the name string.}
-
-
-\subsection{Expression Evaluation}
-
-The dynamic semantics of Core are defined on the type-erasure of the program;
-ie. we ignore all type abstractions and applications. The denotational semantics
-the resulting type-free program are just the conventional ones for a call-by-name
-language, in which expressions are only evaluated on demand.
-But Core is intended to be a call-by-{\it{need}} language, in which
-expressions are only evaluated {\it once}. To express the sharing behavior
-of call-by-need, we give an operational model in the style of Launchbury.
-This section describes the model informally; a more formal semantics is
-separately available in the form of an executable interpreter.
-
-To simplify the semantics, we consider only ``well-behaved'' Core programs in which
-constructor and primitive applications are fully saturated, and in which
-non-trivial expresssions of unlifted kind (@#@) appear only as scrutinees
-in @%case@ expressions. Any program can easily be put into this form;
-a separately available executable preprocessor illustrates how.
-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.
-Evaluation of a program is evaluation of the expression @Main.main@.
-
-To make sure that expression evaluation is shared, we
-make use of a {\it heap}, which can contain
-\begin{itemize}
-\item {\em Thunks} representing suspended (i.e., as yet unevaluated) expressions.
-
-\item {\em WHNF}s representing the result of evaluating such thunks. Computations over
-primitive types are never suspended, so these results are always closures (representing
-lambda abstractions) or data constructions.
-\end{itemize}
-Thunks are allocated when it
-is necessary to suspend a computation whose result may be shared.
-This occurs when evaluating three different kinds of expressions:
-\begin{itemize}
-\item Value definitions at top-level or within a local @let@ expression.
-Here, the defining expressions are suspended and the defined names
-are bound to heap pointers to the suspensions.
-
-\item User function applications. Here, the actual argument expression is
-suspended and the formal argument is bound to a heap pointer to the suspension.
-
-\item Constructor applications. Here, the actual argument expression is
-suspended and a heap pointer to the suspension is embedded in the constructed value.
-\end{itemize}
-
-As computation proceeds, copies of the heap pointer propagate.
-When the computation is eventually forced, the heap entry is overwritten with the resulting
-WHNF, so all copies of the pointer now point to this WHNF. Forcing occurs
-only in the context of
-\begin{itemize}
-\item evaluating the operator expression of an application;
-
-\item evaluating the ``scrutinee'' of a @case@ expression; or
-
-\item evaluating an argument to a primitive or external function application
-\end{itemize}
-
-Ultimately, if there are no remaining pointers to the heap entry (whether suspended or evaluated),
-the entry can be garbage-collected; this is assumed to happen implicitly.
-
-With the exception of functions, arrays, and mutable variables, the intention is that values of all primitive types
-should be held {\it unboxed}, i.e., not heap-allocated. This causes no problems for laziness because all
-primitive types are {\it unlifted}. Unboxed tuple types are not heap-allocated either.
-
-Certain primitives and @%external@ functions cause side-effects to state threads or to the real world.
-Where the ordering of these side-effects matters, Core already forces this order
-by means of data dependencies on the psuedo-values representing the threads.
-
-The @raisezh@ and @handlezh@ primitives requires special support in an implementation, such as a handler stack;
-again, real-world threading guarantees that they will execute in the correct order.
-
-\section{Primitive Module}
-\label{sec:prims}
-
-This section describes the contents and informal semantics of the primitive module @PrimGHC@.
-Nearly all the primitives are required in order to cover GHC's implementation of the Haskell98
-standard prelude; the only operators that can be completely omitted are those supporting the byte-code interpreter,
-parallelism, and foreign objects. Some of the concurrency primitives are needed, but can be
-given degenerate implementations if it desired to target a purely sequential backend; see Section~\ref{sec:sequential}.
-
-In addition to these primitives, a large number of C library functions are required to implement
-the full standard Prelude, particularly to handle I/O and arithmetic on less usual types.
-% We list these separately in section~\ref{sec:ccalls}.
-
-\subsection{Types}
-
-\begin{tabular}{|l|l|l|}
-\hline
-Type & Kind & Description \\
-\hline
-@ZLzmzgZR@ & @* -> * -> *@ & functions (@->@) \\
-@Z1H@ & @? -> #@ & unboxed 1-tuple \\
-@Z2H@ & @? -> ? -> #@ & unboxed 2-tuple \\
-\ldots & \ldots & \ldots \\
-@Z100H@ & @? -> ? -> ? -> ... -> ? -> #@ & unboxed 100-tuple \\
-@Addrzh@ & @#@ & machine address (pointer) \\
-@Charzh@ & @#@ & unicode character (31 bits) \\
-@Doublezh@ & @#@ & double-precision float \\
-@Floatzh@ & @#@ & float \\
-@Intzh@ & @#@ & int (30+ bits) \\
-@Int32zh@ & @#@ & int (32 bits) \\
-@Int64zh@ & @#@ & int (64 bits) \\
-@Wordzh@ & @#@ & unsigned word (30+ bits) \\
-@Word32zh@ & @#@ & unsigned word (32 bits) \\
-@Word64zh@ & @#@ & unsigned word (64 bits) \\
-@RealWorld@ & @*@ & pseudo-type for real world state \\
-@Statezh@ & @* -> #@ & mutable state \\
-@Arrayzh@ & @* -> #@ & immutable arrays \\
-@ByteArrayzh@ & @#@ & immutable byte arrays \\
-@MutableArrayzh@ & @* -> * -> #@ & mutable arrays \\
-@MutableByteArrayzh@ & @* -> #@ & mutable byte arrays \\
-@MutVarzh@ & @* -> * -> #@ & mutable variables \\
-@MVarzh@ & @* -> * -> #@ & synchronized mutable variables \\
-@Weakzh@ & @* -> #@ & weak pointers \\
-@StablePtrzh@ & @* -> #@ & stable pointers \\
-@ForeignObjzh@ & @#@ & foreign object \\
-@ThreadIdzh@ & @#@ & thread id \\
-@ZCTCCallable@ & @? -> *@ & dictionaries for CCallable pseudo-class \\
-@ZCTCReturnable@ & @? -> *@ & dictionaries for CReturnable pseudo-class \\
-\hline
-\end{tabular}
-
-In addition, the types @PrelBase.Bool@ and @PrelBase.Unit@, which are non-primitive
-and are defined as ordinary algebraic types in module @PrelBase@, are used in
-the types of some operators in @PrelGHC@.
-
-The unboxed tuple types are quite special: they hold sets of values in an unlifted
-context, i.e., to be manipulated directly rather than being stored in the heap. They can only
-appear in limited contexts in programs; in particular, they cannot be bound by a
-lambda abstraction or case alternative pattern. Note that they can hold either lifted
-or unlifted values. The limitation to 100-tuples is an arbitrary one set by GHC.
-
-The type of arbitrary precision integers (@Integer@) is not primitive; it is made
-up of an ordinary primitive integer (@Intzh@) and a byte array (@ByteArrzh@).
-The components of an @Integer@ are passed to primitive operators as two separate
-arguments and returned as an unboxed pair.
-
-The @Statezh@ type constructor takes a dummy type argument that is used only
-to distinguish different state {\it threads}~\cite{Launchbury94}.
-The @RealWorld@ type is used only as an argument to @Statezh@, and represents
-the thread of real-world state; it contains just the single value @realWorldzh@.
-The mutable data types @MutableArrayzh@,@MutableByteArrayzh@,@MutVarzh@
-take an initial type argument of the form @(Statezh@ $t$@)@ for some thread $t$.
-The synchronized mutable variable type constructor @MVarzh@ always takes an argument of type
-@Statezh RealWorld@.
-
-@Weakzh@ is the type of weak pointers.
-
-@StablePtrzh@ is the type of stable pointers, which are guaranteed not to move
-during garbage collections; these are useful in connection with foreign functions.
-
-@ForeignPtrzh@ is the type of foreign pointers.
-
-The dictionary types @ZCTCCallable@ and @ZCTCReturnable@ are just placeholders
-which can be represented by a void type;
-any code they appear in should be unreachable.
-
-\subsubsection{Non-concurrent Back End}
-\label{sec:sequential}
-
-The Haskell98 standard prelude doesn't include any concurrency support, but GHC's
-implementation of it relies on the existence of some concurrency primitives. However,
-it never actually forks multiple threads. Hence, the concurrency primitives can
-be given degenerate implementations that will work in a non-concurrent setting,
-as follows:
-\begin{itemize}
-\item @ThreadIdzh@ can be represented
-by a singleton type, whose (unique) value is returned by @myThreadIdzh@.
-
-\item @forkzh@ can just die with an ``unimplemented'' message.
-
-\item @killThreadzh@ and @yieldzh@ can also just die ``unimplemented'' since
-in a one-thread world, the only thread a thread can kill is itself, and
-if a thread yields the program hangs.
-
-\item @MVarzh a@ can be represented by @MutVarzh (Maybe a)@;
-where a concurrent implementation would block, the sequential implementation can
-just die with a suitable message (since no other thread exists to unblock it).
-
-\item @waitReadzh@ and @waitWritezh@ can be implemented using a @select@ with no timeout.
-\end{itemize}
-
-\subsection{Literals}
-
-Only the following combination of literal forms and types are permitted:
-
-\begin{tabular}{|l|l|l|}
-\hline
-Literal form & Type & Description \\
-\hline
-integer & @Intzh@ & Int \\
-% & @Int32zh@ & Int32 \\
-% & @Int64zh@ & Int64 \\
- & @Wordzh@ & Word \\
-% & @Word32zh@ & Word32 \\
-% & @Word64zh@ & Word64 \\
- & @Addrzh@ & Address \\
- & @Charzh@ & Unicode character code \\
-rational & @Floatzh@ & Float \\
- & @Doublezh@ & Double \\
-character & @Charzh@ & Unicode character specified by ASCII character\\
-string & @Addrzh@ & Address of specified C-format string \\
-\hline
-\end{tabular}
-
-\subsection{Data Constructors}
-
-The only primitive data constructors are for unboxed tuples:
-
-\begin{tabular}{|l|l|l|}
-\hline
-Constructor & Type & Description \\
-\hline
-@ZdwZ1H@ & @%forall (a::?).a -> Z1H a@ & unboxed 1-tuple \\
-@ZdwZ2H@ & @%forall (a1::?) (a2::?).a1 -> a2 -> Z2H a1 a2@ & unboxed 2-tuple \\
-\ldots & \ldots & \ldots \\
-@ZdwZ100H@ & @%forall (a1::?) (a2::?)... (a100::?) .@ & \\
-& \ \ \ @a1 -> a2 -> ... -> a100 -> Z100H a1 a2 ... a100@ & unboxed 100-tuple \\
-\hline
-\end{tabular}
-
-\subsection{Values}
-
-Operators are (roughly) divided into collections according to the primary
-type on which they operate.
-
-\workingnote{How do primitives fail, e.g., on division by zero or
-attempting an invalid narrowing coercion?}
-
-\workingnote{The following primop descriptions are automatically generated.
-The exact set of primops and their types presented here
-depends on the underlying word size at the time of generation; these
-were done for 32 bit words. This is a bit stupid.
-More importantly, the word size has a big impact on just what gets produced
-in a Core file, but this isn't documented anywhere in the file itself.
-Perhaps there should be a global flag in the file?}
-
-\newcommand{\primoptions}[7]{{#1} {#2} {#3} {#4} {#5}}
-
-\newcommand{\primopsection}[2]{\subsubsection{#1}{#2}\vspace*{0.1in}}
-\newcommand{\primopdefaults}[1]{Unless otherwise noted, each primop has the following default characteristics: {#1}}
-
-\newcommand{\primopdesc}[8]{
-\par\noindent{\texttt{{{#3} :: {#6}}}}
-\\{#7} {#8}\\}
-
-\input{prims.tex}
-
-\subsubsection{RealWorld}
-
-There is just one value of type @RealWorld@, namely @realWorldzh@. It is used
-only for dependency threading of side-effecting operations.
-
-\begin{thebibliography}{}
-
-\bibitem[Launchbury and {Peyton~Jones}, 1994]{Launchbury94}
-Launchbury, J. and {Peyton~Jones}, S. (1994).
-\newblock Lazy functional state threads.
-\newblock Technical report FP-94-05, Department of Computing Science,
- University of Glasgow.
-
-\bibitem[{Peyton~Jones} and Launchbury, 1991]{pj:unboxed}
-{Peyton~Jones}, S. and Launchbury, J. (1991).
-\newblock Unboxed values as first class citizens.
-\newblock In {\em ACM Conference on Functional Programming and Computer
- Architecture (FPCA'91)}, pages 636--666, Boston. ACM.
-
-\bibitem[{Peyton~Jones} and Marlow, 1999]{ghc-inliner}
-{Peyton~Jones}, S. and Marlow, S. (1999).
-\newblock Secrets of the {Glasgow Haskell Compiler} inliner.
-\newblock In {\em Workshop on Implementing Declarative Languages}, Paris,
- France.
-
-\bibitem[Peyton~Jones and Santos, 1998]{comp-by-trans-scp}
-Peyton~Jones, S. and Santos, A. (1998).
-\newblock A transformation-based optimiser for {Haskell}.
-\newblock {\em Science of Computer Programming}, 32(1-3):3--47.
-
-\end{thebibliography}
-
-\end{document}
projects / ghc-hetmet.git / blobdiff