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