--- /dev/null
+% Andre:
+%
+% - I'd like the transformation rules to appear clearly-identified in
+% a box of some kind, so they can be distinguished from the examples.
+%
+
+
+
+\documentstyle[slpj,11pt]{article}
+
+\renewcommand{\textfraction}{0.2}
+\renewcommand{\floatpagefraction}{0.7}
+
+\begin{document}
+
+\title{How to simplify matters}
+
+\author{Simon Peyton Jones and Andre Santos\\
+Department of Computing Science, University of Glasgow, G12 8QQ \\
+ @simonpj@@dcs.gla.ac.uk@
+}
+
+\maketitle
+
+
+\section{Motivation}
+
+Quite a few compilers use the {\em compilation by transformation} idiom.
+The idea is that as much of possible of the compilation process is
+expressed as correctness-preserving transformations, each of which
+transforms a program into a semantically-equivalent
+program that (hopefully) executes more quickly or in less space.
+Functional languages are particularly amenable to this approach because
+they have a particularly rich family of possible transformations.
+Examples of transformation-based compilers
+include the Orbit compiler,[.kranz orbit thesis.]
+Kelsey's compilers,[.kelsey thesis, hudak kelsey principles 1989.]
+the New Jersey SML compiler,[.appel compiling with continuations.]
+and the Glasgow Haskell compiler.[.ghc JFIT.] Of course many, perhaps most,
+other compilers also use transformation to some degree.
+
+Compilation by transformation uses automatic transformations; that is, those
+which can safely be applied automatically by a compiler. There
+is also a whole approach to programming, which we might call {\em programming by transformation},
+in which the programmer manually transforms an inefficient specification into
+an efficient program. This development process might be supported by
+a programming environment in which does the book keeping, but the key steps
+are guided by the programmer. We focus exclusively on automatic transformations
+in this paper.
+
+Automatic program transformations seem to fall into two broad categories:
+\begin{itemize}
+\item {\bf Glamorous transformations} are global, sophisticated,
+intellectually satisfying transformations, sometimes guided by some
+interesting kind of analysis.
+Examples include:
+lambda lifting,[.johnsson lambda lifting.]
+full laziness,[.hughes thesis, lester spe.]
+closure conversion,[.appel jim 1989.]
+deforestation,[.wadler 1990 deforestation, marlow wadler deforestation Glasgow92, chin phd 1990 march, gill launchbury.]
+transformations based on strictness analysis,[.peyton launchbury unboxed.]
+and so on. It is easy to write papers about these sorts of transformations.
+
+\item {\bf Humble transformations} are small, simple, local transformations,
+which individually look pretty trivial. Here are two simple examples\footnote{
+The notation @E[]@ stands for an arbitrary expression with zero or more holes.
+The notation @E[e]@ denotes @E[]@ with the holes filled in by the expression @e@.
+We implicitly assume that no name-capture happens --- it's just
+a short-hand, not an algorithm.
+}:
+@
+ let x = y in E[x] ===> E[y]
+
+ case (x:xs) of ===> E1[x,xs]
+ (y:ys) -> E1[y,ys]
+ [] -> E2
+@
+Transformations of this kind are almost embarassingly simple. How could
+anyone write a paper about them?
+\end{itemize}
+This paper is about humble transformations, and how to implement them.
+Although each individual
+transformation is simple enough, there is a scaling issue:
+there are a large number of candidate transformations to consider, and
+there are a very large number of opportunities to apply them.
+
+In the Glasgow Haskell compiler, all humble transformations
+are performed by the so-called {\em simplifier}.
+Our goal in this paper is to give an overview of how the simplifier works, what
+transformations it applies, and what issues arose in its design.
+
+\section{The language}
+
+Mutter mutter. Important points:
+\begin{itemize}
+\item Second order lambda calculus.
+\item Arguments are variables.
+\item Unboxed data types, and unboxed cases.
+\end{itemize}
+Less important points:
+\begin{itemize}
+\item Constructors and primitives are saturated.
+\item if-then-else desugared to @case@
+\end{itemize}
+
+Give data type.
+
+\section{Transformations}
+
+This section lists all the transformations implemented by the simplifier.
+Because it is a complete list, it is a long one.
+We content ourselves with a brief statement of each transformation,
+augmented with forward references to Section~\ref{sect:composing}
+which gives examples of the ways in which the transformations can compose together.
+
+\subsection{Beta reduction}
+
+If a lambda abstraction is applied to an argument, we can simply
+beta-reduce. This applies equally to ordinary lambda abstractions and
+type abstractions:
+@
+ (\x -> E[x]) arg ===> E[arg]
+ (/\a -> E[a]) ty ===> E[ty]
+@
+There is no danger of duplicating work because the argument is
+guaranteed to be a simple variable or literal.
+
+\subsubsection{Floating applications inward}
+
+Applications can be floated inside a @let(rec)@ or @case@ expression.
+This is a good idea, because they might find a lambda abstraction inside
+to beta-reduce with:
+@
+ (let(rec) Bind in E) arg ===> let(rec) Bind in (E arg)
+
+ (case E of {P1 -> E1;...; Pn -> En}) arg
+ ===>
+ case E of {P1 -> E1 arg; ...; Pn -> En arg}
+@
+
+
+
+\subsection{Transformations concerning @let(rec)@}
+
+\subsubsection{Floating @let@ out of @let@}
+
+It is sometimes useful to float a @let(rec)@ out of a @let(rec)@ right-hand
+side:
+@
+ let x = let(rec) Bind in B1 ===> let(rec) Bind in
+ in B2 let x = B1
+ in B2
+
+
+ letrec x = let(rec) Bind in B1 ===> let(rec) Bind
+ in B2 x = B1
+ in B2
+@
+
+\subsubsection{Floating @case@ out of @let@}
+
+
+\subsubsection{@let@ to @case@}
+
+
+\subsection{Transformations concerning @case@}
+
+\subsubsection{Case of known constructor}
+
+If a @case@ expression scrutinises a constructor,
+the @case@ can be eliminated. This transformation is a real
+win: it eliminates a whole @case@ expression.
+@
+ case (C a1 .. an) of ===> E[a1..an]
+ ...
+ C b1 .. bn -> E[b1..bn]
+ ...
+@
+If none of the constructors in the alternatives match, then
+the default is taken:
+@
+ case (C a1 .. an) of ===> let y = C a1 .. an
+ ...[no alt matches C]... in E
+ y -> E
+@
+There is an important variant of this transformation when
+the @case@ expression scrutinises a {\em variable}
+which is known to be bound to a constructor.
+This situation can
+arise for two reasons:
+\begin{itemize}
+\item An enclosing @let(rec)@ binding binds the variable to a constructor.
+For example:
+@
+ let x = C p q in ... (case x of ...) ...
+@
+\item An enclosing @case@ expression scrutinises the same variable.
+For example:
+@
+ case x of
+ ...
+ C p q -> ... (case x of ...) ...
+ ...
+@
+This situation is particularly common, as we discuss in Section~\ref{sect:repeated-evals}.
+\end{itemize}
+In each of these examples, @x@ is known to be bound to @C p q@
+at the inner @case@. The general rules are:
+@
+ case x of {...; C b1 .. bn -> E[b1..bn]; ...}
+===> {x bound to C a1 .. an}
+ E[a1..an]
+
+ case x of {...[no alts match C]...; y -> E[y]}
+===> {x bound to C a1 .. an}
+ E[x]
+@
+
+\subsubsection{Dead alternative elimination}
+@
+ case x of
+ C a .. z -> E
+ ...[other alts]...
+===> x *not* bound to C
+ case x of
+ ...[other alts]...
+@
+We might know that @x@ is not bound to a particular constructor
+because of an enclosing case:
+@
+ case x of
+ C a .. z -> E1
+ other -> E2
+@
+Inside @E1@ we know that @x@ is bound to @C@.
+However, if the type has more than two constructors,
+inside @E2@ all we know is that @x@ is {\em not} bound to @C@.
+
+This applies to unboxed cases also, in the obvious way.
+
+\subsubsection{Case elimination}
+
+If we can prove that @x@ is not bottom, then this rule applies.
+@
+ case x of ===> E[x]
+ y -> E[y]
+@
+We might know that @x@ is non-bottom because:
+\begin{itemize}
+\item @x@ has an unboxed type.
+\item There's an enclosing case which scrutinises @x@.
+\item It is bound to an expression which provably terminates.
+\end{itemize}
+Since this transformation can only improve termination, even if we apply it
+when @x@ is not provably non-bottom, we provide a compiler flag to
+enable it all the time.
+
+\subsubsection{Case of error}
+
+@
+ case (error ty E) of Alts ===> error ty' E
+ where
+ ty' is type of whole case expression
+@
+
+Mutter about types. Mutter about variables bound to error.
+Mutter about disguised forms of error.
+
+\subsubsection{Floating @let(rec)@ out of @case@}
+
+A @let(rec)@ binding can be floated out of a @case@ scrutinee:
+@
+ case (let(rec) Bind in E) of Alts ===> let(rec) Bind in
+ case E of Alts
+@
+This increases the likelihood of a case-of-known-constructor transformation,
+because @E@ is not hidden from the @case@ by the @let(rec)@.
+
+\subsubsection{Floating @case@ out of @case@}
+
+Analogous to floating a @let(rec)@ from a @case@ scrutinee is
+floating a @case@ from a @case@ scrutinee. We have to be
+careful, though, about code size. If there's only one alternative
+in the inner case, things are easy:
+@
+ case (case E of {P -> R}) of ===> case E of {P -> case R of
+ Q1 -> S1 Q1 -> S1
+ ... ...
+ Qm -> Sm Qm -> Sm}
+@
+If there's more than one alternative there's a danger
+that we'll duplicate @S1@...@Sm@, which might be a lot of code.
+Our solution is to create a new local definition for each
+alternative:
+@
+ case (case E of {P1 -> R1; ...; Pn -> Rn}) of
+ Q1 -> S1
+ ...
+ Qm -> Sm
+===>
+ let s1 = \x1 ... z1 -> S1
+ ...
+ sm = \xm ... zm -> Sm
+ in
+ case E of
+ P1 -> case R1 of {Q1 -> s1 x1 ... z1; ...; Qm -> sm xm ... zm}
+ ...
+ Pn -> case Rn of {Q1 -> s1 x1 ... z1; ...; Qm -> sm xm ... zm}
+@
+Here, @x1 ... z1@ are that subset of
+variables bound by the pattern @Q1@ which are free in @S1@, and
+similarly for the other @si@.
+
+Is this transformation a win? After all, we have introduced @m@ new
+functions! Section~\ref{sect:join-points} discusses this point.
+
+\subsubsection{Case merging}
+
+@
+ case x of
+ ...[some alts]...
+ other -> case x of
+ ...[more alts]...
+===>
+ case x of
+ ...[some alts]...
+ ...[more alts]...
+@
+Any alternatives in @[more alts]@ which are already covered by @[some alts]@
+should first be eliminated by the dead-alternative transformation.
+
+
+\subsection{Constructor reuse}
+
+
+\subsection{Inlining}
+
+The inlining transformtion is simple enough:
+@
+ let x = R in B[x] ===> B[R]
+@
+Inlining is more conventionally used to describe the instantiation of a function
+body at its call site, with arguments substituted for formal parameters. We treat
+this as a two-stage process: inlining followed by beta reduction. Since we are
+working with a higher-order language, not all the arguments may be available at every
+call site, so separating inlining from beta reduction allows us to concentrate on
+one problem at a time.
+
+The choice of exactly {\em which} bindings to inline has a major impact on efficiency.
+Specifically, we need to consider the following factors:
+\begin{itemize}
+\item
+Inlining a function at its call site, followed by some beta reduction,
+very often exposes opportunities for further transformations.
+We inline many simple arithmetic and boolean operators for this reason.
+\item
+Inlining can increase code size.
+\item
+Inlining can duplicate work, for example if a redex is inlined at more than one site.
+Duplicating a single expensive redex can ruin a program's efficiency.
+\end{itemize}
+
+
+Our inlining strategy depends on the form of @R@:
+
+Mutter mutter.
+
+
+\subsubsection{Dead code removal}
+
+If a @let@-bound variable is not used the binding can be dropped:
+@
+ let x = E in B ===> B
+ x not free in B
+@
+A similar transformation applies for @letrec@-bound variables.
+Programmers seldom write dead code, of course, but bindings often become dead when they
+are inlined.
+
+
+
+
+\section{Composing transformations}
+\label{sect:composing}
+
+The really interesting thing about humble transformations is the way in which
+they compose together to carry out substantial and useful transformations.
+This section gives a collection of motivating examples, all of which have
+shown up in real application programs.
+
+\subsection{Repeated evals}
+\label{sect:repeated-evals}
+
+Example: x+x, as in unboxed paper.
+
+
+\subsection{Lazy pattern matching}
+
+Lazy pattern matching is pretty inefficient. Consider:
+@
+ let (x,y) = E in B
+@
+which desugars to:
+@
+ let t = E
+ x = case t of (x,y) -> x
+ y = case t of (x,y) -> y
+ in B
+@
+This code allocates three thunks! However, if @B@ is strict in {\em either}
+@x@ {\em or} @y@, then the strictness analyser will easily spot that
+the binding for @t@ is strict, so we can do a @let@-to-@case@ transformation:
+@
+ case E of
+ (x,y) -> let t = (x,y) in
+ let x = case t of (x,y) -> x
+ y = case t of (x,y) -> y
+ in B
+@
+whereupon the case-of-known-constructor transformation
+eliminates the @case@ expressions in the right-hand side of @x@ and @y@,
+and @t@ is then spotted as being dead, so we get
+@
+ case E of
+ (x,y) -> B
+@
+
+\subsection{Join points}
+\label{sect:join-points}
+
+One motivating example is this:
+@
+ if (not x) then E1 else E2
+@
+After desugaring the conditional, and inlining the definition of
+@not@, we get
+@
+ case (case x of True -> False; False -> True}) of
+ True -> E1
+ False -> E2
+@
+Now, if we apply our case-of-case transformation we get:
+@
+ let e1 = E1
+ e2 = E2
+ in
+ case x of
+ True -> case False of {True -> e1; False -> e2}
+ False -> case True of {True -> e1; False -> e2}
+@
+Now the case-of-known constructor transformation applies:
+@
+ let e1 = E1
+ e2 = E2
+ in
+ case x of
+ True -> e2
+ False -> e1
+@
+Since there is now only one occurrence of @e1@ and @e2@ we can
+inline them, giving just what we hoped for:
+@
+ case x of {True -> E2; False -> E1}
+@
+The point is that the local definitions will often disappear again.
+
+\subsubsection{How join points occur}
+
+But what if they don't disappear? Then the definitions @s1@ ... @sm@
+play the role of ``join points''; they represent the places where
+execution joins up again, having forked at the @case x@. The
+``calls'' to the @si@ should really be just jumps. To see this more clearly
+consider the expression
+@
+ if (x || y) then E1 else E2
+@
+A C compiler will ``short-circuit'' the
+evaluation of the condition if @x@ turns out to be true
+generate code, something like this:
+@
+ if (x) goto l1;
+ if (y) {...code for E2...}
+ l1: ...code for E1...
+@
+In our setting, here's what will happen. First we desguar the
+conditional, and inline the definition of @||@:
+@
+ case (case x of {True -> True; False -> y}) of
+ True -> E1
+ False -> E2
+@
+Now apply the case-of-case transformation:
+@
+ let e1 = E1
+ e2 = E2
+ in
+ case x of
+ True -> case True of {True -> e1; False -> e2}
+ False -> case y of {True -> e1; False -> e2}
+@
+Unlike the @not@ example, only one of the two inner case
+simplifies, and we can therefore only inline @e2@, because
+@e1@ is still mentioned twice\footnote{Unless the
+inlining strategy decides that @E1@ is small enough to duplicate;
+it is used in separate @case@ branches so there's no concern about duplicating
+work. Here's another example of the way in which we make one part of the
+simplifier (the inlining strategy) help with the work of another (@case@-expression
+simplification.}
+@
+ let e1 = E1
+ in
+ case x of
+ True -> e1
+ False -> case y of {True -> e1; False -> e2}
+@
+The code generator produces essentially the same code as
+the C code given above. The binding for @e1@ turns into
+just a label, which is jumped to from the two occurrences of @e1@.
+
+\subsubsection{Case of @error@}
+
+The case-of-error transformation is often exposed by the case-of-case
+transformation. Consider
+@
+ case (hd xs) of
+ True -> E1
+ False -> E2
+@
+After inlining @hd@, we get
+@
+ case (case xs of [] -> error "hd"; (x:_) -> x) of
+ True -> E1
+ False -> E2
+@
+(I've omitted the type argument of @error@ to save clutter.)
+Now doing case-of-case gives
+@
+ let e1 = E1
+ e2 = E2
+ in
+ case xs of
+ [] -> case (error "hd") of { True -> e1; False -> e2 }
+ (x:_) -> case x of { True -> e1; False -> e2 }
+@
+Now the case-of-error transformation springs to life, after which
+we can inline @e1@ and @e2@:
+@
+ case xs of
+ [] -> error "hd"
+ (x:_) -> case x of {True -> E1; False -> E2}
+@
+
+\subsection{Nested conditionals combined}
+
+Sometimes programmers write something which should be done
+by a single @case@ as a sequence of tests:
+@
+ if x==0::Int then E0 else
+ if x==1 then E1 else
+ E2
+@
+After eliminating some redundant evals and doing the case-of-case
+transformation we get
+@
+ case x of I# x# ->
+ case x# of
+ 0# -> E0
+ other -> case x# of
+ 1# -> E1
+ other -> E2
+@
+The case-merging transformation puts these together to get
+@
+ case x of I# x# ->
+ case x# of
+ 0# -> E0
+ 1# -> E1
+ other -> E2
+@
+Sometimes the sequence of tests cannot be eliminated from the source
+code because of overloading:
+@
+ f :: Num a => a -> Bool
+ f 0 = True
+ f 3 = True
+ f n = False
+@
+If we specialise @f@ to @Int@ we'll get the previous example again.
+
+\subsection{Error tests eliminated}
+
+The elimination of redundant alternatives, and then of redundant cases,
+arises when we inline functions which do error checking. A typical
+example is this:
+@
+ if (x `rem` y) == 0 then (x `div` y) else y
+@
+Here, both @rem@ and @div@ do an error-check for @y@ being zero.
+The second check is eliminated by the transformations.
+After transformation the code becomes:
+@
+ case x of I# x# ->
+ case y of I# y# ->
+ case y of
+ 0# -> error "rem: zero divisor"
+ _ -> case x# rem# y# of
+ 0# -> case x# div# y# of
+ r# -> I# r#
+ _ -> y
+@
+
+\subsection{Atomic arguments}
+
+At this point it is possible to appreciate the usefulness of
+the Core-language syntax requirement that arguments are atomic.
+For example, suppose that arguments could be arbitrary expressions.
+Here is a possible transformation:
+@
+ f (case x of (p,q) -> p)
+===> f strict in its second argument
+ case x of (p,q) -> f (p,p)
+@
+Doing this transformation would be useful, because now the
+argument to @f@ is a simple variable rather than a thunk.
+However, if arguments are atomic, this transformation becomes
+just a special case of floating a @case@ out of a strict @let@:
+@
+ let a = case x of (p,q) -> p
+ in f a
+===> (f a) strict in a
+ case x of (p,q) -> let a=p in f a
+===>
+ case x of (p,q) -> f p
+@
+There are many examples of this kind. For almost any transformation
+involving @let@ there is a corresponding one involving a function
+argument. The same effect is achieved with much less complexity
+by restricting function arguments to be atomic.
+
+\section{Design}
+
+Dependency analysis
+Occurrence analysis
+
+\subsection{Renaming and cloning}
+
+Every program-transformation system has to worry about name capture.
+For example, here is an erroneous transformation:
+@
+ let y = E
+ in
+ (\x -> \y -> x + y) (y+3)
+===> WRONG!
+ let y = E
+ in
+ (\y -> (y+3) + y)
+@
+The transformation fails because the originally free-occurrence
+of @y@ in the argument @y+3@ has been ``captured'' by the @\y@-abstraction.
+There are various sophisticated solutions to this difficulty, but
+we adopted a very simple one: we uniquely rename every locally-bound identifier
+on every pass of the simplifier.
+Since we are in any case producing an entirely new program (rather than side-effecting
+an existing one) it costs very little extra to rename the identifiers as we go.
+
+So our example would become
+@
+ let y = E
+ in
+ (\x -> \y -> x + y) (y+3)
+===> WRONG!
+ let y1 = E
+ in
+ (\y2 -> (y1+3) + y2)
+@
+The simplifier accepts as input a program which has arbitrary bound
+variable names, including ``shadowing'' (where a binding hides an
+outer binding for the same identifier), but it produces a program in
+which every bound identifier has a distinct name.
+
+Both the ``old'' and ``new'' identifiers have type @Id@, but when writing
+type signatures for functions in the simplifier we use the types @InId@, for
+identifiers from the input program, and @OutId@ for identifiers from the output program:
+@
+ type InId = Id
+ type OutId = Id
+@
+This nomenclature extends naturally to expressions: a value of type @InExpr@ is an
+expression whose identifiers are from the input-program name-space, and similarly
+@OutExpr@.
+
+
+\section{The simplifier}
+
+The basic algorithm followed by the simplifier is:
+\begin{enumerate}
+\item Analyse: perform occurrence analysis and dependency analysis.
+\item Simplify: apply as many transformations as possible.
+\item Iterate: perform the above two steps repeatedly until no further transformations are possible.
+(A compiler flag allows the programmer to bound the maximum number of iterations.)
+\end{enumerate}
+We make a effort to apply as many transformations as possible in Step
+2. To see why this is a good idea, just consider a sequence of
+transformations in which each transformation enables the next. If
+each iteration of Step 2 only performs one transformation, then the
+entire program will to be re-analysed by Step 1, and re-traversed by
+Step 2, for each transformation of the sequence. Sometimes this is
+unavoidable, but it is often possible to perform a sequence of
+transformtions in a single pass.
+
+The key function, which simplifies expressions, has the following type:
+@
+ simplExpr :: SimplEnv
+ -> InExpr -> [OutArg]
+ -> SmplM OutExpr
+@
+The monad, @SmplM@ can quickly be disposed of. It has only two purposes:
+\begin{itemize}
+\item It plumbs around a supply of unique names, so that the simplifier can
+easily invent new names.
+\item It gathers together counts of how many of each kind of transformation
+has been applied, for statistical purposes. These counts are also used
+in Step 3 to decide when the simplification process has terminated.
+\end{itemize}
+
+The signature can be understood like this:
+\begin{itemize}
+\item The environment, of type @SimplEnv@, provides information about
+identifiers bound by the enclosing context.
+\item The second and third arguments together specify the expression to be simplified.
+\item The result is the simplified expression, wrapped up by the monad.
+\end{itemize}
+The simplifier's invariant is this:
+$$
+@simplExpr@~env~expr~[a_1,\ldots,a_n] = expr[env]~a_1~\ldots~a_n
+$$
+That is, the expression returned by $@simplExpr@~env~expr~[a_1,\ldots,a_n]$
+is semantically equal (although hopefully more efficient than)
+$expr$, with the renamings in $env$ applied to it, applied to the arguments
+$a_1,\ldots,a_n$.
+
+\subsection{Application and beta reduction}
+
+The arguments are carried ``inwards'' by @simplExpr@, as an accumulating parameter.
+This is a convenient way of implementing the transformations which float
+arguments inside a @let@ and @case@. This list of pending arguments
+requires a new data type, @CoreArg@, along with its ``in'' and ``out'' synonyms,
+because an argument might be a type or an atom:
+@
+data CoreArg bindee = TypeArg UniType
+ | ValArg (CoreAtom bindee)
+
+type InArg = CoreArg InId
+type OutArg = CoreArg OutId
+@
+The equations for applications simply apply
+the environment to the argument (to handle renaming) and put the result
+on the argument stack, tagged to say whether it is a type argument or value argument:
+@
+ simplExpr env (CoApp fun arg) args
+ = simplExpr env fun (ValArg (simplAtom env arg) : args)
+ simplExpr env (CoTyApp fun ty) args
+ = simplExpr env fun (TypeArg (simplTy env ty) : args)
+@
+
+
+
+
+
+
+\end{document}
projects / ghc-hetmet.git / blobdiff