X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=c42aa3a72031c7e52d4123a6b452c3e8e58ebeef;hp=55e00577e393dc0c3933ecb708ad4c394d95ca5c;hb=ae83e3ad02886b6ca5e836b8f1d0fc3ae6321adb;hpb=222070c846ebc49b0b569386fe906edb617bda0b

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 55e0057..c42aa3a 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -230,7 +230,7 @@
       let
         -- Unpack the state by coercion (\eg, cast from
         -- State (Word, Word) to (Word, Word))
-        s = sp :: (Word, Word)
+        s = sp ▶ (Word, Word)
         -- Extract both registers from the state
         r1 = case s of (a, b) -> a
         r2 = case s of (a, b) -> b
@@ -250,7 +250,7 @@
         s' = (,) r1' r2'
         -- pack the state by coercion (\eg, cast from
         -- (Word, Word) to State (Word, Word))
-        sp' = s' :: State (Word, Word)
+        sp' = s' ▶ State (Word, Word)
         -- Pack our return value
         res = (,) sp' out
       in
@@ -334,8 +334,8 @@
       \italic{toplet} = letrec [\italic{binding}...] in var (representable(varvar))
       \italic{binding} = var = \italic{rhs} (representable(rhs))
                        -- State packing and unpacking by coercion
-                       | var0 = var1 :: State ty (lvar(var1))
-                       | var0 = var1 :: ty (var0 :: State ty) (lvar(var1))
+                       | var0 = var1 ▶ State ty (lvar(var1))
+                       | var0 = var1 ▶ ty (var0 :: State ty) (lvar(var1))
       \italic{rhs} = userapp
                    | builtinapp
                    -- Extractor case
@@ -812,6 +812,11 @@
         sure that most lambda abstractions will eventually be reducable by
         β-reduction.
 
+        Note that β-reduction also works on type lambda abstractions and type
+        applications as well. This means the substitution below also works on
+        type variables, in the case that the binder is a type variable and teh
+        expression applied to is a type.
+
         \starttrans
         (λx.E) M
         -----------------
@@ -829,6 +834,17 @@
 
         \transexample{beta}{β-reduction}{from}{to}
 
+        \startbuffer[from]
+        (λt.λa::t. a) @Int
+        \stopbuffer
+
+        \startbuffer[to]
+        (λa::Int. a)
+        \stopbuffer
+
+        \transexample{beta-type}{β-reduction for type abstractions}{from}{to}
+
+
       \subsubsection{Empty let removal}
         This transformation is simple: It removes recursive lets that have no bindings
         (which usually occurs when unused let binding removal removes the last