[Haskell-cafe] Re: Displaying steps in my interpreter

[apfelmus]

Victor Nazarov wrote:
> The goal of the code is to implement the evaluator for untyped lambda-calculus.
> The main problem is how to display each step of reduction? More
> detailed questions follows in the end of the code.
> 
> Terms of lambda-calculus is the following data-type:
>> data (Binder bndr) =>
>>   Term bndr =
>>     Var bndr
>>     | Lam bndr (Term bndr)
>>     | App (Term bndr) (Term bndr)
>>
> 
> Next we'll define the evaluator. Evaluator returns the WHNF for each
> well-formed term, or _|_ if there is no WHNF
> 
> Straight forward version:
> 
> whnf :: Term bndr -> Term bndr
> whnf = reduce []
>  where reduce (a:as) (Lam b i) = reduce as $ subst b a i
>        reduce as (App f a) = reduce (a:as) f
>        reduce as term = foldl term App as
>
> But our goal is to perform only one step of reduction. And to display term
> after each reduction

> Is there a more effective way to perform this? In printReductions I have
> to rescan the syntax tree over and over again to find the redex. Is there a
> way to save the position in the tree, to print the tree and then to resume
> from saved position?

Yes, there is: you can use a zipper

   http://en.wikibooks.org/wiki/Haskell/Zippers

Here's how:

   data Branch v = AppL (Term v)
                 | AppR (Term v)
                 | Lamb v
   type Context v = [Branch v]
   type Zipper v  = (Context v, Term v)

   whnf :: Term v -> Term v
   whnf t = whnf' ([],t)
      where
      whnf' (AppL e':cxt, Lam x e) = whnf' (cxt       , subst x e' e)
      whnf' (cxt        , App f e) = whnf' (AppL e:cxt, f)
      whnf' z                      = unwind z

   unwind :: Zipper v -> Term v
   unwind ([]        , t) = t
   unwind (AppL e:cxt, f) = unwind (cxt, App f e)
   unwind (AppR f:cxt, e) = unwind (cxt, App f e)
   unwind (Lamb x:cxt, e) = unwind (cxt, Lam x e)

Note how this  whnf  and your  whnf  are pretty much exactly the same. 
In fact, your stack of pending applications (the  as  in  reduce' as ) 
is already a zipper. The only difference here is that we are no longer 
limited to only walk down the left spine and can now implement other 
reduction strategies like  nf  or  wnf  too.


Concerning the problem of printing intermediate steps, I don't quite 
understand your approach. I'd simply use a Writer monad to keep track of 
intermediate terms

   import Control.Monad.Writer

      -- use a difference list or something for better performance
   type Trace v = [Zipper v]

   whnf :: Term v -> Writer (Trace v) (Term v)
   whnf t = whnf' ([],t)
      where
      whnf' (AppL e':cxt, Lam x e) = tell  (cxt, App (Lam x e) e') >>
                                     whnf' (cxt       , subst x e' e)
      whnf' (cxt        , App f e) = whnf' (AppL e:cxt, f)
      whnf' z                      = return $ unwind z

The definition of  whnf  is basically left unchanged, except that a 
redex is recorded via  tell  whenever a beta-reduction is about to be 
performed. The recorded terms can be printed afterwards

   printTrace :: Writer (Trace v) (Term v) -> IO ()
   printTrace w = let (t, ts) = runWriter t ts
     putStrLn . unlines . map show $ ts

Note that "zipped" terms are recorded, i.e. the redex enclosed in its 
context and you can even highlight the redex while printing.


Last but not least, there is a nice introductory paper about the many 
possible reduction strategies for lambda calculus

   http://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf


Regards,
apfelmus