[Haskell-cafe] newbie question about denotational semantics

[Alexander Vodomerov]

   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
via monadic approach.

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
used for _any_ monad M.

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
side-effects and was described using monad M_1. Now we add additional
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 Control.Monad.Reader
import Control.Monad.State
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
  env <- ask
  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
  env <- ask
  let f = \v -> let newenv = Map.insert i v env in
                runReader (eval expr) newenv
  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 Control.Monad.Reader
import Control.Monad.Cont
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
  env <- ask
  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
  env <- ask
  let f = \v -> let newenv = Map.insert i v env in
                runReaderT (eval expr) newenv
  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