[Haskell-cafe] Displaying steps in my interpreter

[Victor Nazarov]

Hello,
I have little practice in Haskell. And I look forward for suggestions on how
to improve the code. Code is not working: some definitions are missed.

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

Binder class is used to generate new unique binders and to compare binders
>
> class (Eq bndr) => Binder bndr
>   where {- ... -}
>

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

We refactor the original definition to perform this:

>
> whnfGen :: (Maybe String -> Bool) -> Term bndr -> Term bndr
> whnfGen isFinal = runSteps isFinal $ reduce' []
>
>   where reduce' (a:as) (Lam b i) = markStep "beta" >> reduce as $ subst b a i
>         reduce' as (App f a) = reduce (a:as) f
>         reduce' as term = unwind as term
>
>         reduce as term =
>           do final <- checkFinal
>              if final
>                then unwind as term
>                else reduce' as term
>
>         unwind as term = return $ foldl term App as
>

Steps is the monad:

>
> newtype Steps mark a =
>  Steps { unSteps :: StateT (Maybe mark) (Reader (Maybe mark -> Bool)) a }
>
> instance Monad (Steps mark)
>  where (Steps a) >>= f = Steps $ a >>= \x -> unSteps (f x)
>       return a = Steps $ return a
>
> runSteps :: (Maybe mark -> Bool) -> Steps a -> (Maybe mark, a)
> runSteps isFinal act = runReader (runStateT (unSteps act) Nothing) isFinal
>
> checkFinal :: Steps mark Bool
> checkFinal =
>   do st <- Steps $ get
>      isFinal <- Steps $ lift $ ask
>      return $ isFinal st
>
> markStep :: mark -> Steps mark ()
> markStep = Steps . put . Just
>

Normal whnf can be written as follows:

>
> whnf = whnfGen (const False)
>

To print the reduction steps we can use the following code

>
> printReductions t =
>   do t' <- whnfGen isJust t
>      print t'
>      printReductions t'
>

Is there any better ways to implement printReductions? Is there a way to
abstract out this steps pattern? For example if I want to show the process
of converting lambda-terms to combinatory logic terms (I, K, S basis).
I'll have to implement the same pattern. I can reuse Steps monad, but, I'll
have to use markStep, checkFinal and special version of recursion. Is there
a way to abstract this?

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?

Thanx for reading this :)
-- 
vir
http://vir.comtv.ru/