[Haskell-cafe] Re: Displaying steps in my interpreter
Victor Nazarov
asviraspossible at gmail.com
Fri Jan 11 04:58:01 EST 2008
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/
More information about the Haskell-Cafe
mailing list