Eval of a syntax tree for reduction
I'm working through Pierce's Types and Programming Languages on my own. I'm attempting to write the typecheckers in Haskell, instead of ML. However, when it comes to his eval function, I'm a little stuck. The original is let rec eval t = try let t' = eval1 t in eval t' with NoRuleApplies -> t Where eval1 is a single step evaluation of the abstract syntax tree, and NoRuleApplies is an exception that's raised if there are no rules that can reduce the expression. Now, there's a footnote that it isn't good style in ML. It seems even less natural in Haskell, at least to me, but I still don't know the language that well. The natural equivalent to what Pierce has in ML is something along the lines of data ArithExpr = TmTrue | TmFalse | TmIfExpr ArithExpr ArithExpr ArithExpr | TmZero | TmSucc ArithExpr | TmPred ArithExpr | TmIsZero ArithExpr deriving (Show, Eq) eval1 :: ArithExpr -> ArithExpr eval1 (TmIfExpr TmTrue t _) = t eval1 (TmIfExpr TmFalse _ t) = t eval1 (TmIfExpr t1 t2 t3) = let t1' = eval1 t1 in TmIfExpr t1' t2 t3 -- and so on But, how to terminate the recursion in the full eval? I'm considering changing eval1 to be ArithExpr->Maybe ArithExpr If the expression is reducible, then I return Just t, and if it's not reducible, then Nothing It makes eval1 a bit more complicated, and not as straightforward translation from the type system being described, though. e.g reducing If looks more like eval1 (TmIfExpr t1 t2 t3) = let t1' = eval1 t1 in case t1' of { Just t1'' -> Just $ TmIfExpr t1'' t2 t3 ; Nothing -> Nothing } and eval then looks like eval t = let t' = eval1 t in case t' of { Just t'' -> eval t'' ; Nothing -> t' } I'm looking for some suggestions on the direction to proceed.
Steve Downey wrote:
It makes eval1 a bit more complicated, and not as straightforward translation from the type system being described, though. e.g reducing If looks more like
eval1 (TmIfExpr t1 t2 t3) = let t1' = eval1 t1 in case t1' of { Just t1'' -> Just $ TmIfExpr t1'' t2 t3 ; Nothing -> Nothing }
You should use the fact that Maybe is a monad: eval1 (TmIfExpr t1 t2 t3) = do t1' <- eval1 t1 return $ TmIfExpr t1' t2 t3
and eval then looks like eval t = let t' = eval1 t in case t' of { Just t'' -> eval t'' ; Nothing -> t' }
(In the above, I suspect you need Nothing -> t, no prime.) BTW, there's no need to use let here: eval t = case eval1 t of Just t' -> eval t' Nothing -> t
Steve Downey wrote: ] I'm considering changing eval1 to be ArithExpr->Maybe ArithExpr ] ] If the expression is reducible, then I return Just t, and if it's not ] reducible, then Nothing ] ] It makes eval1 a bit more complicated, and not as straightforward ] translation from the type system being described, though. ] e.g reducing If looks more like ] ] eval1 (TmIfExpr t1 t2 t3) = ] let t1' = eval1 t1 ] in case t1' of ] { Just t1'' -> Just $ TmIfExpr t1'' t2 t3 ] ; Nothing -> Nothing ] } ] ] I'm looking for some suggestions on the direction to proceed. If you are looking to get rid of the noise caused by Maybe, you could package up all of the "case" and "Just" stuff into a few reusable functions. In fact, its already been done for you, since Maybe is a monad... http://www.nomaware.com/monads/html/maybemonad.html ...You could try something like...
import Control.Monad -- for liftM3, etc.
eval1_ :: ArithExpr -> Maybe ArithExpr eval1_ (TmIfExpr TmTrue t _) = return t eval1_ (TmIfExpr TmFalse _ t) = return t eval1_ (TmIfExpr t1 t2 t3) = liftM3 TmIfExpr (eval1_ t1) (return t2) (return t3)
...and if it turns out you don't like the resulting "Maybeified" program, you can get the original functionality back by changing the type signature to use the Identity monad instead of Maybe. Greg Buchholz
participants (3)
-
Antti-Juhani Kaijanaho -
Greg Buchholz -
Steve Downey