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

27 Mar 2006

      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.

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

Steve Downey