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/