Improve Normalization chapter a bit.
authorMatthijs Kooijman <matthijs@stdin.nl>
Mon, 2 Nov 2009 13:53:21 +0000 (14:53 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Mon, 2 Nov 2009 13:53:21 +0000 (14:53 +0100)
Chapters/Normalization.tex

index d93717a..5647ae0 100644 (file)
     this notation are still a bit fuzzy, so comments are welcom.
 
     \subsection{General cleanup}
+      These transformations are general cleanup transformations, that aim to
+      make expressions simpler. These transformations usually clean up the
+       mess left behind by other transformations or clean up expressions to
+       expose new transformation opportunities for other transformations.
+
+       Most of these transformations are standard optimizations in other
+       compilers as well. However, in our compiler, most of these are not just
+       optimizations, but they are required to get our program into normal
+       form.
 
       \subsubsection{β-reduction}
         β-reduction is a well known transformation from lambda calculus, where it is
         sure that most lambda abstractions will eventually be reducable by
         β-reduction.
 
-        TODO: Define substitution syntax
-
         \starttrans
         (λx.E) M
         -----------------
 
         \transexample{β-reduction}{from}{to}
 
-      \subsubsection{Application propagation}
-        This transformation is meant to propagate application expressions downwards
-        into expressions as far as possible. This allows partial applications inside
-        expressions to become fully applied and exposes new transformation
-        possibilities for other transformations (like β-reduction).
-
-        \starttrans
-        let binds in E) M
-        -----------------
-        let binds in E M
-        \stoptrans
-
-        % And an example
-        \startbuffer[from]
-        ( let 
-            val = 1
-          in 
-            add val
-        ) 3
-        \stopbuffer
-
-        \startbuffer[to]
-        let 
-          val = 1
-        in 
-          add val 3
-        \stopbuffer
-
-        \transexample{Application propagation for a let expression}{from}{to}
-
-        \starttrans
-        (case x of
-          p1 -> E1
-          \vdots
-          pn -> En) M
-        -----------------
-        case x of
-          p1 -> E1 M
-          \vdots
-          pn -> En M
-        \stoptrans
-
-        % And an example
-        \startbuffer[from]
-        ( case x of 
-            True -> id
-            False -> neg
-        ) 1
-        \stopbuffer
-
-        \startbuffer[to]
-        case x of 
-          True -> id 1
-          False -> neg 1
-        \stopbuffer
-
-        \transexample{Application propagation for a case expression}{from}{to}
-
       \subsubsection{Empty let removal}
         This transformation is simple: It removes recursive lets that have no bindings
         (which usually occurs when let derecursification removes the last binding from
         M
         \stoptrans
 
-        \subsubsection{Simple let binding removal}
+      \subsubsection{Simple let binding removal}
         This transformation inlines simple let bindings (\eg a = b).
 
         This transformation is not needed to get into normal form, but makes the
         TODO
 
     \section{Program structure}
+      These transformations are aimed at normalizing the overall structure
+      into the intended form. This means ensuring there is a lambda abstraction
+      at the top for every argument (input port), putting all of the other
+      value definitions in let bindings and making the final return value a
+      simple variable reference.
 
       \subsubsection{η-abstraction}
         This transformation makes sure that all arguments of a function-typed
         expression are named, by introducing lambda expressions. When combined with
-        β-reduction and function inlining below, all function-typed expressions should
-        be lambda abstractions or global identifiers.
+        β-reduction and non-representable binding inlining, all function-typed
+        expressions should be lambda abstractions or global identifiers.
 
         \starttrans
         E                 \lam{E :: a -> b}
 
         \transexample{η-abstraction}{from}{to}
 
+      \subsubsection{Application propagation}
+        This transformation is meant to propagate application expressions downwards
+        into expressions as far as possible. This allows partial applications inside
+        expressions to become fully applied and exposes new transformation
+        opportunities for other transformations (like β-reduction and
+        specialization).
+
+        \starttrans
+        (let binds in E) M
+        -----------------
+        let binds in E M
+        \stoptrans
+
+        % And an example
+        \startbuffer[from]
+        ( let 
+            val = 1
+          in 
+            add val
+        ) 3
+        \stopbuffer
+
+        \startbuffer[to]
+        let 
+          val = 1
+        in 
+          add val 3
+        \stopbuffer
+
+        \transexample{Application propagation for a let expression}{from}{to}
+
+        \starttrans
+        (case x of
+          p1 -> E1
+          \vdots
+          pn -> En) M
+        -----------------
+        case x of
+          p1 -> E1 M
+          \vdots
+          pn -> En M
+        \stoptrans
+
+        % And an example
+        \startbuffer[from]
+        ( case x of 
+            True -> id
+            False -> neg
+        ) 1
+        \stopbuffer
+
+        \startbuffer[to]
+        case x of 
+          True -> id 1
+          False -> neg 1
+        \stopbuffer
+
+        \transexample{Application propagation for a case expression}{from}{to}
+
       \subsubsection{Let derecursification}
         This transformation is meant to make lets non-recursive whenever possible.
         This might allow other optimizations to do their work better. TODO: Why is
         Note that this transformation does not try to be smart when faced with
         recursive lets, it will just leave the lets recursive (possibly joining a
         recursive and non-recursive let into a single recursive let). The let
-        rederecursification transformation will do this instead.
+        dederecursification transformation will do this instead.
 
         \starttrans
         letnonrec x = (let bindings in M) in N
         \lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that
         is bound by \lam{x}. This might need some extra notes or something).
 
+        Note that the return value is not simplified if its not representable.
+        Otherwise, this would cause a direct loop with the inlining of
+        unrepresentable bindings, of course. If the return value is not
+        representable because it has a function type, η-abstraction should
+        make sure that this transformation will eventually apply. If the value
+        is not representable for other reasons, the function result itself is
+        not representable, meaning this function is not representable anyway!
+
         \starttrans
         x = E                            \lam{E} is representable
         ~                                \lam{E} is not a lambda abstraction
 
         \transexample{Case removal}{from}{to}
 
-  \subsection{Monomorphisation}
-    TODO: Better name for this section
-
+  \subsection{Removing polymorphism}
     Reference type-specialization (== argument propagation)
 
-  \subsubsection{Defunctionalization}
+    Reference polymporphic binding inlining (== non-representable binding
+    inlining).
+
+  \subsection{Defunctionalization}
+    These transformations remove most higher order expressions from our
+    program, making it completely first-order (the only exception here is for
+    arguments to builtin functions, since we can't specialize builtin
+    function. TODO: Talk more about this somewhere).
+
     Reference higher-order-specialization (== argument propagation)
 
       \subsubsection{Non-representable binding inlining}