simply inline the let bindings that have a polymorphic type,
which should (eventually) make sure that the polymorphic
expression is applied to a type and/or dictionary, which can
- \refdef{beta-reduction}
- then be removed by β-reduction.
+ then be removed by β-reduction (\in{section}[sec:normalization:beta]).
Since both type and dictionary arguments are not representable,
\refdef{representable}
η-abstraction also introduces extra applications (the application of
the let expression to \lam{q} in the above example). These
applications can then propagated down by the application propagation
- transformation (\in{section}[sec:normalization:approp]). In our
+ transformation (\in{section}[sec:normalization:appprop]). In our
example, the \lam{q} and \lam{r} variable will be propagated into the
let expression and then into the case expression: