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

[apfelmus]

Victor Nazarov wrote:
>>    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)")

Yes, it should (you can just try, right? :). That's because

    tell w >> something

is basically

    let (w', x) = something in (w ++ w', x)

Now,  something  may loop forever, but  w ++ w' doesn't care, it 
prepends  w  no matter what  w'  is. Of course, asking for  x  (the 
normal form in our case) instead of  w ++ w'  won't succeed when 
something  loops forever.

(Cave: this is only true for the writer monad in 
Control.Monad.Writer.Lazy  which is imported by default. The writer 
monad in  Control.Monad.Writer.Strict  intentionally behaves differently.)


Regards,
apfelmus