[Haskell-cafe] Displaying steps in my interpreter
Victor Nazarov
asviraspossible at gmail.com
Thu Jan 10 06:47:13 EST 2008
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/
More information about the Haskell-Cafe
mailing list