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
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
\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
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
-----------------
\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