- function position. In the same way the transformation does not apply to both
- components of this expression (\lam{case opcode of Low -> (+); High -> (-)}
- and \lam{a}), so we'll skip to the components of the case expression: The
- scrutinee and both alternatives. Since the opcode is not a function, it does
- not apply here, and we'll leave both alternatives as an exercise to the
- reader. The final function, after all these transformations becomes:
+ function position (which makes the second condition false). In the same
+ way the transformation does not apply to both components of this
+ expression (\lam{case opcode of Low -> (+); High -> (-)} and \lam{a}), so
+ we'll skip to the components of the case expression: The scrutinee and
+ both alternatives. Since the opcode is not a function, it does not apply
+ here.
+
+ The first alternative is \lam{(+)}. This expression has a function type
+ (the operator still needs two arguments). It does not occur in function
+ position of an application and it is not a lambda expression, so the
+ transformation applies.
+
+ We look at the \lam{<original expression>} pattern, which is \lam{E}.
+ This means we bind \lam{E} to \lam{(+)}. We then replace the expression
+ with the \lam{<transformed expression>}, replacing all occurences of
+ \lam{E} with \lam{(+)}. In the \lam{<transformed expression>}, the This gives us the replacement expression:
+ \lam{λx.(+) x} (A lambda expression binding \lam{x}, with a body that
+ applies the addition operator to \lam{x}).
+
+ The complete function then becomes:
+ \startlambda
+ (case opcode of Low -> λa1.(+) a1; High -> (-)) a
+ \stoplambda
+
+ Now the transformation no longer applies to the complete first alternative
+ (since it is a lambda expression). It does not apply to the addition
+ operator again, since it is now in function position in an application. It
+ does, however, apply to the application of the addition operator, since
+ that is neither a lambda expression nor does it occur in function
+ position. This means after one more application of the transformation, the
+ function becomes:
+
+ \startlambda
+ (case opcode of Low -> λa1.λb1.(+) a1 b1; High -> (-)) a
+ \stoplambda
+
+ The other alternative is left as an exercise to the reader. The final
+ function, after applying η-abstraction until it does no longer apply is: