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:

It's time to test:

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

For instance:

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:

The clumsy interpreter can indeed be tested as follows:

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:

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

Regards,

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