[TYPES] rewriting of typed combinator expressions

[Claus Reinke]

> One reason to prefer the big-step as interpreter semantics is that it
> is directly executable (which brings lots of benefits: easy
> experimentation, test suites, etc etc). Of course, and perhaps in
> support of Matthias's point, the one-step semantics is just as
> executable. So, let me take this chance and to plug PLT Redex, one tool
> that takes such semantics and executes them:
> 
>   http://people.cs.uchicago.edu/~robby/pubs/papers/rta2004-mfff.pdf

Thanks for that reference. I, too, find one-step semantics more useful
when looking at operational aspects of programming language designs
(big-step hides those details, which is fine when your focus is on other
things). And yes, it is easy to get such rules wrong. 

Even non-language-designers tend to appreciate the chance to experience 
the reduction semantics of their language step-by-step, if they ever get that 
chance (mainly for learning, but occasionally also for debugging, and to get
a better feeling for resource usage). As someone who was taught functional 
programming with reduction systems in the Berkling/Kluge tradition, I can 
only say that mainstream fp systems skip over some difficult but interesting 
aspects of fpl implementation, and that mainstream functional programmers 
are worse off because of this, especially when they want to understand the
interactions with their languages' i/o or concurrency features. It is nice that 
PLT Scheme tries to fight that trend.

(to react to an earlier remark in this thread: if one takes programming with 
functions seriously, one often finds the "do not ever reduce under lambdas"
mantra of conventional implementations somewhat limiting)

Btw, you can actually come quite close to writing interpreters using 
context-based rewrite rules in plain Haskell. Modulo the usual errors, 
the attached code outlines the idea for normal-order and applicative-order 
reduction in the lambda calculus.

Cheers,
Claus

*Main> redNor ikik
0: App (App (Lam "x" (Var "x")) (Lam "x" (Lam "y" (Var "x")))) (App (Lam "x" (Var "x")) (Lam "x" (Lam "y" (Var "x"))))
1: App (Lam "x" (Lam "y" (Var "x"))) (App (Lam "x" (Var "x")) (Lam "x" (Lam "y" (Var "x"))))
2: Lam "y" (App (Lam "x" (Var "x")) (Lam "x" (Lam "y" (Var "x"))))
*Main> redAor ikik
0: App (App (Lam "x" (Var "x")) (Lam "x" (Lam "y" (Var "x")))) (App (Lam "x" (Var "x")) (Lam "x" (Lam "y" (Var "x"))))
1: App (Lam "x" (Lam "y" (Var "x"))) (App (Lam "x" (Var "x")) (Lam "x" (Lam "y" (Var "x"))))
2: App (Lam "x" (Lam "y" (Var "x"))) (Lam "x" (Lam "y" (Var "x")))
3: Lam "y" (Lam "x" (Lam "y" (Var "x")))