[Haskell-cafe] Programming an Evaluation Context
Claus Reinke
claus.reinke at talk21.com
Thu Feb 15 07:15:59 EST 2007
> 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)
More information about the Haskell-Cafe
mailing list