in structural operational semantics, an evaluation context is often used to decompose an expression into a redex and its context. In a formal semantics on paper, an expression can just be "pattern matched" over the grammar of an evaluation context. If one wants to implement such a semantics in the form of an interpreter, I could not come up with a similarly nice solution. I have declared two separate data types (one for expressions, and one for evaluation contexts) and explicit functions to convert an expression into a (evaluation context, redex) pair.

do you really need an explicit representation of evaluation contexts? yes, explicit representation of contexts through zippers makes for more efficient evaluation, but for small prototypes, that may not be necessary, and for larger prototypes, you may want to represent the optimizations implicit in zipper traversal explicitly by moving from interpreter to compiler+stack-based abstract machine.

Are there any tricks to mimick more closely what is going on in the formal semantics?

I tend to find MonadPlus and pattern-match failure as mzero very helpful, for almost direct translation of operational semantics represented in terms of evaluation contexts and reduction rules. See below for a sketch. Hth, Claus ------------------------------------------------------ import Control.Monad data Expr = Val Int | Plus Expr Expr deriving Show -- evaluation: stepwise reduction until done eval e = done e `mplus` (step e >>= eval) -- normal form done e = do { (Val i) <- return e; return (Val i) } -- reduction rule reduce e = do { (Plus (Val i) (Val j)) <- return e; return (Val (i+j)) } -- one-step reduction: apply reduction rule in evaluation context step e = ctxt reduce e -- evaluation contexts, parameterized by rule to apply ctxt rule e = rule e `mplus` left (ctxt rule) e `mplus` right (ctxt rule) e left act e = do { (Plus l r) <- return e; lv <- act l; return (Plus lv r) } right act e = do { (Plus lv@(Val _) r) <- return e; rv <- act r; return (Plus lv rv) } -- example main = do let e = (Val 1 `Plus` Val 2) `Plus` (Val 3 `Plus` Val 4) print e print (eval e :: Maybe Expr)