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<br>
<br>let rec eval t = <br> try let t' = eval1 t<br> in eval t'<br> with NoRuleApplies -> t<br><br>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.
<br><br>The natural equivalent to what Pierce has in ML is something along the lines of<br><br>data ArithExpr <br> = TmTrue<br> | TmFalse<br> | TmIfExpr ArithExpr ArithExpr ArithExpr<br> | TmZero <br> | TmSucc ArithExpr
<br> | TmPred ArithExpr<br> | TmIsZero ArithExpr<br> deriving (Show, Eq)<br><br>eval1 :: ArithExpr -> ArithExpr<br><br>eval1 (TmIfExpr TmTrue t _) = t<br><br>eval1 (TmIfExpr TmFalse _ t) = t<br><br>eval1 (TmIfExpr t1 t2 t3) =
<br> let t1' = eval1 t1<br> in TmIfExpr t1' t2 t3<br>-- and so on<br><br>But, how to terminate the recursion in the full eval?<br><br>I'm considering changing eval1 to be ArithExpr->Maybe ArithExpr<br><br>If the expression is reducible, then I return Just t, and if it's not reducible, then Nothing
<br><br>It makes eval1 a bit more complicated, and not as straightforward translation from the type system being described, though.<br>e.g reducing If looks more like<br><br>eval1 (TmIfExpr t1 t2 t3) = <br> let t1' = eval1 t1
<br> in case t1' of<br> { Just t1'' -> Just $ TmIfExpr t1'' t2 t3<br> ; Nothing -> Nothing <br> }<br><br>and eval then looks like<br>eval t = <br> let t' = eval1 t <br> in case t' of
<br> { Just t'' -> eval t'' <br> ; Nothing -> t'<br> }<br><br><br>I'm looking for some suggestions on the direction to proceed. <br>