A tiny bit of denotational semantics

All languages and assignments in this blog post are (C) 2011 Ralf Lämmel.

This is actually an assignment for my paradigms/semantics class.

Consider the following super-trivial interpreter written in Haskell and in the direct style of denotational semantics:

data Exp = Const Int
    | Add Exp Exp

eval :: Exp -> Int
eval (Const i) = i
eval (Add x y) = eval x + eval y

It's time to test:

> eval (Add (Const 20) (Const 22))
42

This incredible language handles integer constants and addition. Now assume that we are adding an "exit" form of expression. The intended semantics of a term "Exit e" is to define the final result of expression evaluation as the value of e. Hence, if an exit expression occurs inside an addition, then the addition is effectively cancelled. Thus:

data Exp = Const Int
    | Add Exp Exp
    | Exit Exp

For instance:

• Add (Const 20) (Const 22) should evaluate to 42.


• Add (Exit (Const 88)) (Const 42) should evaluate to 88.

A particularly clumsy way of writing an interpreter for the extended language is to stubbornly stick to direct style of denotational semantics. That is, we may use, for example, the result type to encode whether we are returning from a normal evaluation or whether we are supposed to exit. In such a case, we have to systematically check intermediate results to propagate exit. In our simple language, we need to propagate in the equation for addition. Thus:

-- Result type for clumsy direct style:
-- The sum serves for tagging.
-- Left tags normal result values.
-- Right tags exit values.
type R = Either Int Int

-- Standard combinator for sum processing
(\/) :: (a -> c) -> (b -> c) -> Either a b -> c
(f \/ g) (Left x)  = f x
(f \/ g) (Right y) = g y

-- Tag removal
toInt :: Either Int Int -> Int
toInt = id \/ id

-- Clumsy semantic function
eval :: Exp -> R
eval (Const i) = con i
eval (Add x y) = add (eval x) (eval y)
eval (Exit x) = exit (eval x)

-- Algebra for denotations
con :: Int -> R
con = Left

add :: R -> R -> R
add x y = ((\x' -> ((Left . (x'+)) \/ Right) y) \/ Right) x

exit :: R -> R
exit = Right . toInt

The clumsy interpreter can indeed be tested as follows:

> toInt (eval (Add (Const 20) (Const 22)))
42
> toInt (eval (Add (Exit (Const 88)) (Const 42)))
88

Here are two trivial assignments that make you understand a) the basics of continuations and b) the relationship between analysis and denotational semantics. 1st assignment: Design an alternative semantics for the extended language so that you exploit continuation style instead of direct style. 2nd assignment: Revise the direct style semantics to derive a program analysis determining the purity of an expression; an expression is pure if it does not contain any reference to the Exit form of expression. Thus, we would like to be able to run tests as follows:

> eval (Add (Const 20) (Const 22)) id
42
> eval (Add (Exit (Const 88)) (Const 42)) id
88
> pure (Add (Const 20) (Const 22))
True
> pure (Add (Exit (Const 88)) (Const 42))
False

(We pass the identity continuation to the applications of eval.)

Regards,

PF