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/
Victor Nazarov wrote:
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)
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
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?
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) whnf :: Term v -> Term v whnf t = whnf' ([],t) where whnf' (AppL e':cxt, Lam x e) = whnf' (cxt , subst x e' e) whnf' (cxt , App f e) = whnf' (AppL e:cxt, f) whnf' z = unwind z 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) Note how this whnf and your whnf are pretty much exactly the same. In fact, your stack of pending applications (the as in reduce' as ) is already a zipper. The only difference here is that we are no longer limited to only walk down the left spine and can now implement other reduction strategies like nf or wnf too. 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 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 Note that "zipped" terms are recorded, i.e. the redex enclosed in its context and you can even highlight the redex while printing. 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 Regards, apfelmus
On Jan 10, 2008 8:39 PM, apfelmus
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/
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
participants (2)
-
apfelmus -
Victor Nazarov