Normalize optimize/optimizing a bit

chapters/c2.lhs

@@ -7,7 +7,7 @@ short, we discuss linear types, the Haskell programming language, linear types
 as they exist in Haskell (dubbed Linear Haskell), evaluation strategies,
 Haskell's main intermediate language (Core) and its formal foundation (System
 $F_C$) and, finally, an overview of GHC's pipeline with explanations of crucial
-Core-to-Core optimizing transformations that we'll try to validate.
+Core-to-Core optimising transformations that we'll try to validate.
 
 \section{Linear Types\label{sec:linear-types}}
 
@@ -829,7 +829,7 @@ compiler.
 
 \begin{itemize}
 \item Core allows us to reason about the entirety of Haskell in a much smaller
-functional language. Performing analysis, optimizing transformations, and code
+functional language. Performing analysis, optimising transformations, and code
 generation is done on Core, not Haskell. The implementation of these compiler passes is
 significantly simplified by the minimality of Core.
 
@@ -839,8 +839,8 @@ type-checking Core serves as an internal consistency check for the desugaring
 and optimization passes.
 %
 The Core typechecker provides a verification layer for the correctness of
-desugaring and optimizing transformations (and their implementations) because
-both desugaring and optimizing transformations must produce well-typed Core.
+desugaring and optimising transformations (and their implementations) because
+both desugaring and optimising transformations must produce well-typed Core.
 
 \item Finally, Core's expressiveness serves as a sanity-check for
 all the extensions to the source language -- if we can desugar a
@@ -955,7 +955,7 @@ compilation strategy, we highlight the inherent incompatibility of
 linearity with Core / System~$F_C$ as a current flaw in GHC that
 invalidates all the benefits of Core wrt linearity.  Thus, we must
 extend System $F_C$ (and, therefore, Core) with linearity in order to
-adequately validate the desugaring and optimizing transformations as
+adequately validate the desugaring and optimising transformations as
 linearity preserving, ensuring we can reason about Linear Haskell in
 its Core representation.
 
@@ -1037,12 +1037,12 @@ constructors are transformed into coercions).
 % TODO: Split worker/wrapper into its own section?
 
 The Core-to-Core transformations are the most important set of
-optimizing transformations that GHC performs during compilation. By design, the
+optimising transformations that GHC performs during compilation. By design, the
 frontend of the pipeline (parsing, renaming, typechecking and desugaring) does
 not include any optimizations -- all optimizations are done in Core.
 The transformational approach focused on Core, known as \emph{compilation by
   transformation}, allows transformations to be both modular and simple.
-Each transformation focuses on optimizing a specific set of
+Each transformation focuses on optimising a specific set of
 constructs, where applying a transformation often exposes opportunities for
 other transformations to fire. Since transformations are modular, they
 can be chained and iterated in order to maximize the optimization potential (as
@@ -1053,21 +1053,21 @@ shown in Figure~\ref{fig:eg:transformations}).
 % I know this paragraph is useless :)
 However, due to the destructive nature of transformations (i.e. applying a
 transformation is not reversible), the order in which transformations
-are applied determines how well the resulting program is optimized.
+are applied determines how well the resulting program is optimised.
 As such, certain orderings of optimizations can hide 
 optimization opportunities and block them from firing. This phase-ordering
-problem is present in most optimizing compilers.
+problem is present in most optimising compilers.
 
 % Techniques such as
 % equality saturation~\cite{} bypass the phase-ordering problem because all
-% optimizing transformations are applied non-destructively; however, it's a much
+% optimising transformations are applied non-destructively; however, it's a much
 % more expensive technique that has not been .
 %
 % transformation based approach to optimization allows each producing a Core
-% program fed to the next optimizing transformation.
+% program fed to the next optimising transformation.
 
 Foreshadowing the fact that Core is the main object of our study, we want to type-check
-linearity in Core before \emph{and} after each optimizing transformation is
+linearity in Core before \emph{and} after each optimising transformation is
 applied (Section~\ref{sec:core}).
 %
 In light of it, we describe below some of the individual Core-to-Core
@@ -1076,7 +1076,7 @@ the literature, the first set of Core-to-Core optimizations was described
 in~\cite{santos1995compilation,peytonjones1997a}. These were subsequently
 refined and
 expanded~\cite{peytonjones2002secrets,baker-finch2004constructed,maurer2017compiling,Breitner2016_1000054251,sergey_vytiniotis_jones_breitner_2017}.
-In Figure~\ref{fig:eg:transformations} we present an example that is optimized
+In Figure~\ref{fig:eg:transformations} we present an example that is optimised
 by multiple transformations to highlight how the compilation by transformation
 process produces performant programs.
 
@@ -1472,7 +1472,7 @@ The code generation needn't be changed to account for the work we will do in
 the context of this thesis, so we only briefly describe it.
 
 After the core-to-core pipeline is run on the Core program and produces
-optimized Core, the program is translated down to the Spineless Tagless
+optimised Core, the program is translated down to the Spineless Tagless
 G-Machine (STG) language~\cite{jones_1992}. STG language is a small functional
 language that serves as the abstract machine code for the STG abstract machine
 that ultimately defines the evaluation model and compilation of Haskell through

chapters/c7.lhs

@@ -142,9 +142,9 @@ optimising compiler $\dots$}
 %system, not Core. Nonetheless, in practice, Core is linearity-aware.
 %
 %We want Core and its type system to give us guarantees about desugaring and
-%optimizing transformations with regard to linearity just as Core does for types
+%optimising transformations with regard to linearity just as Core does for types
 %-- a linearly typed Core ensures that linearly-typed programs remain correct
-%both after desugaring and across all GHC optimizing transformations,
+%both after desugaring and across all GHC optimising transformations,
 %i.e.~linearity is preserved when desugaring and optimisations should not
 %destroy linearity.
 %
@@ -234,12 +234,12 @@ optimising compiler $\dots$}
 %produced by Core transformations.
 %
 %% Therefore, the Core linear type-checker rejects various valid programs after
-%% desugaring and optimizing transformations, because linearity is seemingly
+%% desugaring and optimising transformations, because linearity is seemingly
 %% violated.
 %%
 %The current solution to valid programs being rejected by Core's linear
 %type-checker is to effectively disable the linear type-checker since,
-%alternatively, disabling optimizing transformations which violate linearity
+%alternatively, disabling optimising transformations which violate linearity
 %incurs significant performance costs.
 %%
 %However, we believe that GHC's transformations are correct, and it is the
@@ -915,7 +915,7 @@ resources are consumed to be able to use the case binder unrestrictedly. This
 one doesn't typecheck, but is still semantically linear}
 This particular example has a known constructor being scrutinized which might
 seem like an unrealistic example, but we recall that during the transformations
-programs undergo in an optimizing compiler, many programs such as this
+programs undergo in an optimising compiler, many programs such as this
 naturally occur (e.g. if the definition of a function were inlined in the scrutinee).
 
 Moreover, in a branch of a constructor without linear fields we also know the
@@ -1080,7 +1080,7 @@ programs (highlighted with \colorbox{notyet}{\notyetcolorname})
 from Section~\ref{sec:semantic-linearity-examples}, which Core currently
 rejects.
 %
-Besides type safety, we prove that multiple optimizing Core-to-Core
+Besides type safety, we prove that multiple optimising Core-to-Core
 transformations preserve linearity in Linear Core. These same transformations
 don't preserve linearity under Core's current type system. As far as we know,
 we are the first to prove optimisations preserve types in a non-strict linear
@@ -2197,11 +2197,11 @@ The proofs for preservation, progress, irrelevance, and for the substitution lem
 \subsection{Optimisations preserve linearity\label{sec:optimisations-preserve-types-meta}}
 
 One of the primary goals of the Linear Core type system is being suitable for
-intermediate representations of optimizing compilers for lazy languages with
-linear types. In light of this goal, we prove that \emph{multiple optimizing
+intermediate representations of optimising compilers for lazy languages with
+linear types. In light of this goal, we prove that \emph{multiple optimising
 transformations} are type preserving in Linear Core, and thus preserve linearity.
 
-The optimizing transformations proved sound wrt Linear Core in this section
+The optimising transformations proved sound wrt Linear Core in this section
 have been previously explained and motivated in
 Section~\ref{sec:core-to-core-transformations}.
 %

chapters/c8.lhs

@@ -123,7 +123,7 @@ accounts for linearity. In this context, we intend to introduce a linearly typed
 System $F_C$ with multiplicity annotations and typing rules to serve
 as a basis for a linear Core. Critically, this Core linear language
 must account for call-by-need evaluation semantics and be valid in
-light of Core-to-Core optimizing transformations.
+light of Core-to-Core optimising transformations.
 
 % \parawith{System FC}
 
@@ -177,7 +177,7 @@ which presents its own challenges.
 Nonetheless, while the Linear Haskell work keeps Core unchanged, its
 implementation in GHC does modify and extend Core with linearity/multiplicity
 annotations, and said extension of Core with linear types does not account for
-optimizing transformations and the non-strict semantics of Core.
+optimising transformations and the non-strict semantics of Core.
 
 Our work on linear Core intends to overcome the limitations of linear types as
 they exist in Core, i.e. integrating call-by-need semantics and validating the
@@ -214,11 +214,11 @@ benefit from linearity analysis and, in order to improve those transformation,
 linear-type-inspired systems were created specifically for the purpose of the
 transformation.
 
-By fully supporting linear types in Core, these optimizing transformations
+By fully supporting linear types in Core, these optimising transformations
 could be informed by the language inherent linearity, and, consequently, avoid
 an ad-hoc or incomplete linear-type inference pass custom-built for
 optimizations. Additionally, the linearity information may potentially be used
-to the benefit of optimizing transformations that currently don't take any
+to the benefit of optimising transformations that currently don't take any
 linearity into account.
 
 % \begin{itemize}
@@ -229,7 +229,7 @@ linearity into account.
 % \item Ser ad-hoc incompleto ou nao feito de todo
 % \end{itemize}
 
-% \parawith{A transformation based optimizer for Haskell}
+% \parawith{A transformation based optimiser for Haskell}
 % They discuss a cardinality analysis based on a linear type system but create (an
 % ad-hoc?) one suited. Comparison in the measure of creating optimizations based
 % on linearity.

report.lhs

@@ -115,13 +115,13 @@ which is used as an internal consistency tool to validate the transformations a
 Haskell program undergoes during compilation.
 %
 However, the current Core type-checker rejects many linearly valid programs
-that originate from Core-to-Core optimizing transformations. As such, linearity
+that originate from Core-to-Core optimising transformations. As such, linearity
 typing is effectively disabled, for otherwise disabling optimizations would be
 far more devastating.
 %
 % This dissertation presents an extension to Core's type system that accepts a
 The goal of our proposed dissertation is to develop an extension to Core's type
-system that accepts a larger amount of programs and verifies that optimizing
+system that accepts a larger amount of programs and verifies that optimising
 transformations applied to well-typed linear Core produce well-typed linear
 Core.
 %
@@ -283,11 +283,11 @@ due to the following reasons:
         intermediate language into which Haskell is
         translated. Core is a minimal, explicitly typed,
         functional language, to which multiple
-        Core-to-Core optimizing transformations are
+        Core-to-Core optimising transformations are
         applied during compilation. Due to Core's minimal design, typechecking
         Core programs is very efficient and doing so serves as a sanity check to the
-        correction of the source transformations. If the resulting optimized
-        Core program fails to typecheck, the optimizing
+        correction of the source transformations. If the resulting optimised
+        Core program fails to typecheck, the optimising
         transformations (are very likely to) have introduced an error
         in the resulting program. We present Core (and its formal
         basis, System~$F_C$~\cite{cite:systemfc}) in Section~\ref{sec:core}.
@@ -324,7 +324,7 @@ due to the following reasons:
 % extending Core with linear types.
 %
 Much like a typed Core ensures that the translation from Haskell (dubbed
-\emph{desugaring}) and the subsequent optimizing transformations applied to
+\emph{desugaring}) and the subsequent optimising transformations applied to
 Core are correctly implemented, a \emph{linearly typed} Core guarantees that
 linear resource usage in the source language is not violated by the translation
 process and the compiler optimization passes.
@@ -337,18 +337,18 @@ duplicated a pointer to heap-allocated memory that was previously just used
 once and then freed in the original program.
 %TODO: linearidade pode informar otimizacoes
 %
-Even more, linearity in Core can inform Core-to-Core optimizing
+Even more, linearity in Core can inform Core-to-Core optimising
 transformations~\cite{cite:let-floating,peytonjones1997a,cite:linearhaskell},
 such as inlining and $\beta$-reduction, to produce more performant programs.
 
 % Linear core actually not so good
 % Additionally, while not yet a reality, linearity in Core could be used to inform
 % certain program optimizations, i.e. having linear types in Core could be used to
-% further optimize certain programs and, therefore, benefit the runtime
+% further optimise certain programs and, therefore, benefit the runtime
 % performance characteristics of our programs. For example, Linear Haskell\cite{}
 % describes as future work an improvement to the inlining optimization: Inlining
 % is a centerpiece program optimization primarily because of the subsequent
-% optimizing opportunities unlocked by inlining. However, it relies on a heuristic
+% optimising opportunities unlocked by inlining. However, it relies on a heuristic
 % process known as \emph{cardinality analysis} to discover safe inlining
 % opportunities. Unfortunately, heuristics can be volatile and fail in identifying
 % crucial inlining opportunities resulting in programs that fall short of their
@@ -359,7 +359,7 @@ such as inlining and $\beta$-reduction, to produce more performant programs.
 % While the current version of Core is linearity-aware (i.e.,~Core has so-called
 % multiplicity annotations in variable binders), its type system does not (fully)
 % validate the linearity constraints in the desugared program and essentially
-% fails to type-check programs resulting from several optimizing transformations
+% fails to type-check programs resulting from several optimising transformations
 % that are necessary to produce efficient object code. The reason for this latter
 % point is not evidently clear:
 % %
@@ -378,7 +378,7 @@ if we can typecheck linearity in the surface level Haskell why do we fail to do
 so in Core?
 
 The desugaring process from surface level Haskell to Core, and the subsequent
-Core-to-Core optimizing transformations, eliminate and rearrange most of the
+Core-to-Core optimising transformations, eliminate and rearrange most of the
 syntactic constructs through which linearity checking is performed -- often
 resulting in programs completely different from the original, especially due to
 the flexibility laziness provides a compiler in the optimisations it may
@@ -397,7 +397,7 @@ f :: a ⊸ a
 f x = let y = use x in x
 \end{code}
 
-The Core optimizing transformations expose a fundamental limitation of Core's
+The Core optimising transformations expose a fundamental limitation of Core's
 current linear type system -- it does not account for Core's call-by-need
 evaluation model, and thus a whole class of programs that are linear under the
 lens of lazy evaluation are rejected by Core's current linear type system.
@@ -446,7 +446,7 @@ transformations in linearity-heavy Haskell libraries, such as
 % In fact, we are not aware of any linear type system which
 % understands linearity in the presence of laziness.
 
-% \todo[inline]{In reality, the Core optimizing transformations only expose a
+% \todo[inline]{In reality, the Core optimising transformations only expose a
 % more fundamental issue in the existing linear types in Haskell -- its mismatch
 % with the evaluation model. In call-by-need languages a mention of a variable
 % might not entail using that variable - it depends on it being required or not.
@@ -456,8 +456,8 @@ transformations in linearity-heavy Haskell libraries, such as
 % annotations such that we can desugar all of Linear Haskell and validate it
 % accross transformations taking into consideration Core's call-by-need
 % semantics, we can validate the surface level linear type's implementation, we
-% can guarantee optimizing transformations do not destroy linearity, and we might
-% be able to inform optimizing transformations with linearity.
+% can guarantee optimising transformations do not destroy linearity, and we might
+% be able to inform optimising transformations with linearity.
 
 % Consider the following recursive let
 % definition, where $x$ is a linear variable that must be used exactly once, would
@@ -472,12 +472,12 @@ transformations in linearity-heavy Haskell libraries, such as
 % \end{code}
 
 % Alternatively, one might imagine Haskell being desugared into an intermediate
-% representation to which multiple different optimizing transformations are
+% representation to which multiple different optimising transformations are
 % applied but on which no integrity checks are done
 
 % Despite \emph{want} a linearly-typed core
 % because a linearly-typed Core ensures that desugaring
-% Haskell and optimizing transformations don't destroy linearity.
+% Haskell and optimising transformations don't destroy linearity.
 
 % In theory, because the Core language must also know about linearity, we should
 
@@ -487,7 +487,7 @@ transformations in linearity-heavy Haskell libraries, such as
 % In theory, we should typecheck \emph{linearity} in \textbf{Core} just the same
 % as the typechecking verification we had with the existing type annotations prior
 % to the addition of linear types, that is, our Core program with linearity
-% annotations should be typechecked after the optimizing transformations...
+% annotations should be typechecked after the optimising transformations...
 
 \todo[inline]{We should discuss the alternative motivation of figuring out how
 to typecheck linearity in the presence of laziness on its own, why its hard and
@@ -505,7 +505,7 @@ the programmer so much}
 
 \todo[inline]{Saying, finally, what we are going to do, and that our system is
 capable of seeing linearity in all of these programs, and more -- it is capable
-of typechecking almost all optimizing transformations we studied}
+of typechecking almost all optimising transformations we studied}
 
 \todo[inline]{Conclude by explaining that the document is structured in such a
 way that the payload starts in chapter 3 after delivering the background