Alexander Vodomerov alex at sectorb.msk.ru
Tue Feb 20 05:35:18 EST 2007

```   Hi all!

I'm just started learning denotational semantics and have a simple question.

Suppose, we have simple language L (e.g. some form of lambda-calculus)
and have a semantic function: E : Term_L -> Value.

Now, suppose, we extended our language with some additional side-effects
(e.g. state or continuations). For this purpose we first add new
syntactic construct to language (e.g 'call/cc'), and then write semantic

We have:

L_ext = L + 'call/cc'

E_ext : Term_{L_ext} -> M (Value),

where M is some monad (Cont Value for our case).

Now, I want to proof statement that original and extended semantics are
coincide on expressions that don't use new constructs (call/cc). It
would be natural to formulate such "theorem":

"Theorem". If t is expression, that doesn't use new construct, then

E_orig(t) = E_ext(t).

Alas, this equation doesn't make any sense, because E_orig(t) and E_ext(t) are
elements of different domains: Value and M(Value).

The obvious "fix" it to use "unit" operation of monad ("return" in Haskell
syntax) to put both values into the same space. So we get:

"Theorem" (second try). For all t, bla-bla-bla..
unit_M(E_orig(t)) = E_ext(t).

However, this still doesn't work because Values are in fact different:

-- in original semantic we have (more source code available below)
data Value1 = Number Int
| Func (Value1 -> Value1)

-- in extended semantic we have
data Value2 = Number Int
| Func (Value2 -> M Value2)
^ note this M

The monad M seems to be "wired in" recursively in Value definition.

>From the mathematical point of view it is common to use projection or
injection when one need to compare functions to different sets. However,
I don't see any obvious injection Value1 -> Value2 or projection
Value2 -> Value1.

Some monads can be "removed", for example StateT can be eliminated with
runState with initial state and etc. However, some monads, for example
Error, Maybe, non-deteminism monad (powerdomain) don't have such
"removal function". What is needed is general definition that can be

The question is: how can this "theorem" be formulated (and prooved) in
mathematically precise way?

It seems that I missing something very trivial, so just reference to article
will be nice.

The more general question is: suppose original language already has
effects and use bigger monad M_2. The same question arises: how one can
compare elements in Value domain defined via M_1 and M_2?

With best regards,
Alexander.

PS. Some code I played with:

-- original semantic
import qualified Data.Map as Map

type Id = String
type Env = Map.Map String Value

stdops :: Map.Map String (Int -> Int -> Int)
stdops = Map.fromList [("+", (+)), ("-", (-)), ("*", (*))]

data Expr = Const Int
| Var String
| BinOp String Expr Expr
| Lambda Id Expr
| Appl Expr Expr deriving Show

data Value = Number Int
| Func (Value -> Value)

instance Show Value where
show (Number v) = show v
show (Func _) = "*func*"

eval :: Expr -> Reader Env Value
eval (Const c) = return (Number c)
eval (Var i) = do
return \$ env Map.! i
eval (BinOp op x y) = do
vx <- eval x
vy <- eval y
let opfun = stdops Map.! op
case (vx, vy) of
(Number a, Number b) -> return \$ Number (opfun a b)
_ -> error "standard operation on not-numbers"
eval (Lambda i expr) = do
let f = \v -> let newenv = Map.insert i v env in
return (Func f)
eval (Appl fun arg) = do
vfun <- eval fun
varg <- eval arg
case vfun of
Func f -> return \$ f varg
_ -> error "application of not-function"

do_eval :: Expr -> Value
do_eval expr = runReader (eval expr) Map.empty

-- extended semanic
import qualified Data.Map as Map

type Id = String
type Env = Map.Map String Value
type M = Cont Value

stdops :: Map.Map String (Int -> Int -> Int)
stdops = Map.fromList [("+", (+)), ("-", (-)), ("*", (*))]

data Expr = Const Int
| Var String
| BinOp String Expr Expr
| Lambda Id Expr
| Appl Expr Expr
| CallCC Expr deriving Show

data Value = Number Int
| Func (Value -> M Value)

instance Show Value where
show (Number v) = show v
show (Func _) = "*func*"

eval :: Expr -> ReaderT Env M Value
eval (Const c) = return (Number c)
eval (Var i) = do
return \$ env Map.! i
eval (BinOp op x y) = do
vx <- eval x
vy <- eval y
let opfun = stdops Map.! op
case (vx, vy) of
(Number a, Number b) -> return \$ Number (opfun a b)
_ -> error "standard operation on not-numbers"
eval (Lambda i expr) = do
let f = \v -> let newenv = Map.insert i v env in
return (Func f)
eval (Appl fun arg) = do
vfun <- eval fun
varg <- eval arg
case vfun of
Func f -> lift \$ f varg
_ -> error "application of not-function"
eval (CallCC expr) = do
f <- eval expr
case f of
Func vf -> lift \$ callCC (\k -> vf (Func k))
_ -> error "call/cc with not-function"

do_eval :: Expr -> Value
do_eval expr = runCont (runReaderT (eval expr) Map.empty) id

```