[Haskell-cafe] Eval of a syntax tree for reduction

[Steve Downey]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org//pipermail/haskell-cafe/attachments/20060327/1fe97580/attachment.htm