[Haskell-cafe] Re: Displaying steps in my interpreter
apfelmus
apfelmus at quantentunnel.de
Thu Jan 10 12:39:28 EST 2008
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
More information about the Haskell-Cafe
mailing list