[Haskell-cafe] Programming an Evaluation Context

[Claus Reinke]

> 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)