sdiehl
diff --git a/‎000_introduction.md
+100-55 b/‎000_introduction.md
+100-55
diff --git a/‎001_basics.md
+36-27 b/‎001_basics.md
+36-27
@@ -1,14 +1,19 @@
+<div class="pagetitle">
 ![](img/titles/introduction.png)
+</div>
 
-******
+<p class="halfbreak">
+</p>
 
-> When the limestone of imperative programming is worn away, the granite of
-> functional programming will be observed.
+<!--
+> *When the limestone of imperative programming is worn away, the granite of
+> functional programming will be observed.*
 > 
 > <cite>— Simon Peyton Jones</cite>
 
 <p class="halfbreak">
 </p>
+-->
 
 Introduction
 ============
@@ -151,42 +156,71 @@ refines the space of allowable behavior and degree of expressible programs for
 the language.  Types are the world's most popular formal method for analyzing
 programs.
 
-$$
-\begin{aligned}
-1 &: \t{Nat} \\
-(\lambda x . x) &: \forall a. a \to a \\
-(\lambda x y . x) &: \forall a b. a \to b \to a \\
-\end{aligned}
-$$
+In a language like Python all expressions have the same type at compile time,
+and all syntactically valid programs can be evaluated. In the case where the
+program is nonsensical the runtime will bubble up exceptions at runtime. The
+Python interpreter makes no attempt to analyze the given program for soundness
+at all before running it.
+
+```bash
+>>> True & "false"
+Traceback (most recent call last):
+  File "<stdin>", line 1, in <module>
+TypeError: unsupported operand type(s) for &: 'bool' and 'str'
+```
 
-In more sophisticated languages types and terms will commingle either with
-explicit annotations on binders, or even as first class values themselves.
+By comparison Haskell will do quite a bit of work to try to ensure that the
+program is well-defined before running it. The language that we use to
+predescribe and analyze static semantics of the program is that of *static
+types*.
 
-$$
-\t{Pair} \ u \ v = \Lambda X . \lambda x^{U \rightarrow V \rightarrow X} . x u v
-$$
+```bash
+Prelude> True && "false"
+
+<interactive>:2:9:
+    Couldn't match expected type `Bool' with actual type `[Char]'
+    In the second argument of `(&&)', namely `"false"'
+    In the expression: True && "false"
+    In an equation for `it': it = True && "false"
+```
 
-In all the languages which we will implement the types present during compilation are
-*erased*. Although they are present in the evaluation semantics, the runtime
-cannot dispatch on types of values at runtime. Types by definition only exist at
-compile-time in the static semantics of the language.
+Catching minor type mismatch errors is the simplest example of usage, although
+they occur extremely frequently as we humans are quite fallible in our reasoning
+about even the simplest of program constructions! Although this just the tip of
+the iceberg, the gradual trend over the last 20 years toward more *expressive
+types* in modern type systems; which are capable of guaranteeing a large variety
+of program correctness properties.
+
+* Preventing resource allocation errors.
+* Enforcing security access for program logic.
+* Side effect management.
+* Preventing buffer overruns.
+* Ensuring cryptographic properties for network protocols.
+* Modeling and verify theorems in mathematics and logic.
+* Preventing data races and deadlocks in concurrent systems.
+
+Type systems can never capture all possible behavior of the program. Although
+more sophisticated type systems are increasingly able to model a large space of
+behavior and is one of the most exciting areas of modern computer science
+research. Put most bluntly, **static types let you be dumb** and offload the
+checking that you would otherwise have to do in your head to a system that can
+do the reasoning for you and work with you to interactively build your program.
 
 Functional Compilers
 --------------------
 
-A compiler is typically divided into parts, a *frontend* and a *backend*. These
-are loose terms but the frontend typically deals with converting the human
-representation of the code into some canonicalized form while the backend
-converts the canonicalized form into another form that is suitable for
-evaluation.
+A *compiler* is a program for turning high-level representation of ideas in a
+human readable language into another form. A compiler is typically divided into
+parts, a *frontend* and a *backend*. These are loose terms but the frontend
+typically deals with converting the human representation of the code into some
+canonicalized form while the backend converts the canonicalized form into
+another form that is suitable for evaluation.
 
 The high level structure of our functional compiler is described by the
 following *block diagram*. Each describes a *phase* which is a sequence of
 transformations composed to transform the input program.
 
-<p class="center">
 ![](img/pipeline1.png)
-</p>
 
 * **Source**            - The frontend textual source language.
 * **Parsing**           - Source is parsed into an abstract syntax tree.
@@ -200,15 +234,13 @@ A *pass* may transform the input program from one form into another or alter the
 internal state of the compiler context. The high level description of the forms
 our final compiler will go through is the following sequence:
 
-<p class="center">
 ![](img/pipeline2.png)
-</p>
 
 Internal forms used during compilation are *intermediate representations* and
 typically any non-trivial language will involve several.
 
-Lexing
-------
+Parsing
+-------
 
 The source code is simply the raw sequence of text that specifies the program.
 Lexing splits the text stream into a sequence of *tokens*. Only the presence of
@@ -222,22 +254,22 @@ let f x = x + 1
 For instance the previous program might generate a token stream like the
 following:
 
-Token      Value
------      -----
-reserved   let
-var        f
-var        x
-reservedOp =
-var        x
-reservedOp +
-integer    1
-
-Parsing
--------
+```haskell
+[
+  TokenLet,
+  TokenSym "f",
+  TokenSym "x",
+  TokenEq,
+  TokenSym "x",
+  TokenAdd,
+  TokenNum 1
+]
+```
 
-A datatype for the *abstract syntax tree* (AST) is constructed by traversal of
-the input stream and generation of the appropriate syntactic construct using a
-parser.
+We can then scan the token stream via and dispatch on predefined patterns of
+tokens called *productions* and recursively build up a datatype for the
+*abstract syntax tree* (AST) by traversal of the input stream and generation of
+the appropriate syntactic.
 
 ```haskell
 type Name = String
@@ -319,6 +351,19 @@ Let "f" []
       (Lit (LitInt 1))))
 ```
 
+Transformation
+--------------
+
+The type core representation is often suitable for evaluation, but quite often
+different intermediate representations are more amenable to certain
+optimizations and make explicit semantic properties of the language explicit.
+These kind of intermediate forms will often attach information about free
+variables, allocations, and usage information directly onto the AST to make it 
+
+The most important form we will use is called the *Spineless Tagless G-Machine*
+( STG ), an abstract machine that makes many of the properties of lazy
+evaluation explicit directly in the AST.
+
 Code Generation
 ---------------
 
@@ -356,11 +401,11 @@ resulting module.
 
 ```perl
 f:
-	movl	%edi, -4(%rsp)
-	movl	-4(%rsp), %edi
-	addl	$1, %edi
-	movl	%edi, %eax
-	ret
+        movl    %edi, -4(%rsp)
+        movl    -4(%rsp), %edi
+        addl    $1, %edi
+        movl    %edi, %eax
+        ret
 
 ```
 
@@ -370,11 +415,11 @@ instructions defined by the processor specification.
 
 ```perl
 0000000000000000 <f>:
-   0:	89 7c 24 fc          	mov    %edi,-0x4(%rsp)
-   4:	8b 7c 24 fc          	mov    -0x4(%rsp),%edi
-   8:	81 c7 01 00 00 00    	add    $0x1,%edi
-   e:	89 f8                	mov    %edi,%eax
-  10:	c3                   	retq
+   0:   89 7c 24 fc             mov    %edi,-0x4(%rsp)
+   4:   8b 7c 24 fc             mov    -0x4(%rsp),%edi
+   8:   81 c7 01 00 00 00       add    $0x1,%edi
+   e:   89 f8                   mov    %edi,%eax
+  10:   c3                      retq
 ```
 
 \pagebreak
@@ -1,6 +1,6 @@
+<div class="pagetitle">
 ![](img/titles/basics.png)
-
-******
+</div>
 
 <!--
 <blockquote>
@@ -33,14 +33,12 @@ add :: Integer -> Integer -> Integer
 add x y =  x + y
 ```
 
-```haskell
-add (x,y) = x + y
-```
+In Haskell all functions are pure, the only thing a function may do is return a
+value.
 
-In Haskell all functions are pure, the only thing a function may do is return a value.
-
-All functions in Haskell are curried, for example a function of three arguments takes up to three arguments and for
-anything less than three it yields a partially applied function which when given additional arguments yields a
+All functions in Haskell are curried, for example a function of three arguments
+takes up to three arguments and for anything less than three it yields a
+partially applied function which when given additional arguments yields a
 another function or the resulting value if saturated.
 
 ```haskell
@@ -51,7 +49,8 @@ h :: Int -> Int
 h = g 2 3
 ```
 
-Haskell supports higher-order functions, functions which take functions and yield other functions.
+Haskell supports higher-order functions, functions which take functions and
+yield other functions.
 
 ```haskell
 compose f g = \x -> f (g x)
@@ -86,10 +85,7 @@ constructors also generates special set of functions known as *selectors* which
 extract the values of a specific field from the record.
 
 ```haskell
-data Prod = Prod
-  { a :: Int
-  , b :: Bool
-  }
+data Prod = Prod { a :: Int , b :: Bool }
 
 -- a :: Prod -> Int
 -- b :: Prod -> Bool
@@ -158,7 +154,7 @@ Tuples are allowed (with compiler support) up to 15 fields in GHC.
 Pattern matching
 ----------------
 
-Pattern matching allows us to discriminate on the constructor(s) of a datatype,
+Pattern matching allows us to discriminate on the constructors of a datatype,
 mapping separate cases to separate code paths.
 
 ```haskell
@@ -216,12 +212,17 @@ Recursion
 In Haskell all iteration over data structures is performed by recursion.
 Entering a function in Haskell does not create a new stack frame, the logic of
 the function is simply entered with the arguments on the stack and yields result
-to the register. The resulting logic is compiled identically to ``while`` loops
-in other languages, via a ``jmp`` instruction instead of a ``call``.
+to the register. In the case where a function returns a invocation of itself
+invoked in the *tail position* the resulting logic is compiled identically to
+``while`` loops in other languages, via a ``jmp`` instruction instead of a
+``call``.
 
 ```haskell
-factorial 0 = 1
-factorial n = n * factorial (n - 1)
+sum :: [Int] -> [Int]
+sum ys = go ys 0
+  where
+    go (x:xs) i = go xs (i+x)
+    go [] i = i
 ```
 
 Functions can be defined to recurse mutually on each other.
@@ -421,29 +422,29 @@ all monad instances must satisfy.
 **Law 1**
 
 ```haskell
-return a >>= f ≡ f a
+return a >>= f = f a
 ```
 
 **Law 2**
 
 ```haskell
-m >>= return ≡ m
+m >>= return = m
 ```
 
 **Law 3**
 
 ```haskell
-(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
+(m >>= f) >>= g = m >>= (\x -> f x >>= g)
 ```
 
 Haskell has a level of syntactic sugar for monads known as do-notation. In this
 form binds are written sequentially in block form which extract the variable
 from the binder.
 
 ```haskell
-do { a <- f ; m } ≡ f >>= \a -> do { m }
-do { f ; m } ≡ f >> do { m }
-do { m } ≡ m
+do { a <- f ; m } = f >>= \a -> do { m }
+do { f ; m } = f >> do { m }
+do { m } = m
 ```
 
 So for example the following are equivalent.
@@ -504,6 +505,16 @@ discards the left while ``<*`` discards the right. For example in a monadic
 parser combinator library the ``*>`` would parse with first parser argument but
 return the second.
 
+Monoids
+-------
+
+```haskell
+class Monoid a where
+  mempty :: a
+  mappend :: a -> a -> a
+  mconcat :: [a] -> a
+```
+
 Deriving
 --------
 
@@ -638,9 +649,7 @@ evalStack m = execWriterT (evalStateT (unStack m) 0)
 
 As illustrated by the following stack diagram:
 
-<p class="center">
 ![](img/stack.png)
-</p>
 
 Using mtl and ``GeneralizedNewtypeDeriving`` we can produce the same stack but with
 a simpler forward facing interface to the transformer stack. Under the hood mtl