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

[Victor Nazarov]

On Jan 10, 2008 8:39 PM, apfelmus <apfelmus at quantentunnel.de> wrote:
> Victor Nazarov wrote:
> >
> 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)
>
>    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)
>

Thanks. Zippers seemed very cool when I first encountered them in some
text about xmonad. But I've never used them in my own code.

> 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
>

My version just return when the state in State monad is not Nothing,
so we can print result and start over again.

>    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
>

Is this function lazy? Can I run this code on term without nf and
print n-first steps:

>    printTraceN :: Int -> Writer (Trace v) (Term v) -> IO ()
>    printTraceN n w =
>      let (t, ts) = runWriter t ts
>      in putStrLn . unlines . map show $ take n ts
>

Will this work:

> printTraceN 5 (read "(\x. x x x) (\x. x x x)")

?

>
> 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
>

Thank you.

-- 
vir
http://vir.comtv.ru/