{-
  Extensible Denotational Semantics


 This work is a generalization of 
      Extensible Denotational Language Specifications
      Robert Cartwright, Matthias Felleisen
      Theor. Aspects of Computer Software, 1994
      http://citeseer.ist.psu.edu/69837.html

 to be referred to as EDLS.

We implement the enhanced EDLS in Haskell and add delimited control.
To be precise, we implement the Base interpreter (whose sole
operations are Loop and Error) and the following extensions: CBV
lambda-calculus, Arithmetic, Storage, Control. The extensions can be
added to the Base interpreter in any order and in any combination.

Our implementation has the following advantages over EDLS:
 -- support for delimited control
 -- support for a local storage (including `thread-local' storage
    and general delimited dynamic binding)
 -- extensions do not have to be composed explicitly, and so the
    composition order truly does not matter.  In the original EDLS, one
    had to write interpreter composition explicitly. In our approach, an
    extension is pulled in automatically if the program includes the
    corresponding syntactic forms. For example, if a program contains
    storage cell creation and dereference operations, the Storage extension
    will automatically be used to interpret the program.

Our main departure from EDLS is is the removal of the `central
authority'. There is no semantic `admin' function. Rather, admin is
part of the source language and can be used at any place in the
code. The `central authority' of EDLS must be an extensible function,
requiring meta-language facilities to implement (such as quite
non-standard Scheme modules). We do not have central
authority. Rather, we have bureaucracy: each specific effect handler
interprets its own effects as it can, throwing the rest `upstairs' for
higher-level bureaucrats to deal with. Extensibility arises
automatically.

We take the meaning of a program to be the union of Values and
(unfulfilled) Actions. If the meaning of the program is a (non-bottom)
value, the program is terminating. If the meaning of the program is an
Action -- the program finished with an error, such as an action to
access a non-existing storage cell, or shift without reset, or a
user-raised error.

Incidentally, EDLS stresses on p. 2 (the last full paragraph) that
their schema critically relies on the distinction between a complete
program and a nested program phrase. Our contribution (which is the
consequence of removing the central admin, making it first-class) is
eliminating such a distinction! EDLS says, at the very top of p. 3,
that the handle in the effect message ``is roughly a conventional
continuation.'' Because the admin of EDLS is `outside' of the program
(at the point of infinity, so to speak), its continuation indeed
appears undelimited. By making our `admin' a part of the source
language, we recognize the handle in the effect message for what it
is: a _delimited_ continuation.

As we see below, the Control aspect is orthogonal to the CBV
aspect. So, we can just as easily replace the CBV extension with the
CBN extension, which will give us the denotation of delimited control
in CBN.


We shall be using Haskell to express denotations, taking advantage of
the fact that Haskell values are `lifted'. See also the remark on p21
of EDLS: someone (ref. [4]) showed that sets and partial functions can
suffice...


Our program denotations are stable: they have the same form regardless
of a particular composition of modular interpreters.  See Section 3.5
of EDLS for precise formulation (and the last paragraph of Section 3.4
for concise informal statement of stability). Also see the comparison
with the monads on p. 20: different monads assign numeral radically
different meanings, depending on the monad. But in EDLS, a numeral has
exactly the same denotation.

The meaning of an expression is also the same and stable, no matter
what the interpreter is: it is a function from Env to Computations
(the latter being the union of values and unfulfilled effects -- the
same union mentioned above).

However, by using handlers, some effect messages can be subtracted:
so, strictly speaking, the denotation of a fragment is V +
effect-message-issued - effect-messages handled.  There seem to be a
connection with effect systems.


Additional notes on EDLS:

The abstract and p. 2 (especially the last full paragraph) are
so well-written!

p. 5, bottom: ``It [ref \x.x, where ref means what it does in ML] 
is a closed expression that does not diverge, is not a value, and
cannot be reduced to a value without affecting the context. We refer
to such results as _effects_.''

Beginning of Section 3 and App A give a very good introduction
to the denotational semantics.

p. 6: ``Algebraically speaking, the interpreter is (roughly) a
homomorphism from syntax to semantics''

``A straightforward representation of an evaluation context is a
function from values to computations, which directly corresponds to
its operational usage as a function from syntactic values to
expressions.'' (p. 8). EDLS then notices that the `handle' has
the same type as the denotation of a context. Footnote 6 notes that
handler is roughly the composition combinator for functions from values
to computations [contexts!] and it superficially relates to [bind]
but does not satisfy all monad laws.

The last of EDLS Sec 3.5, p. 15: ``Informally speaking, this property
[stable denotations] asserts that in the framework of extensible
semantics, the addition of a programming construct corresponds to the
addition of a new ``dimension'' to the space of meaning. [The
equations, featuring injection and projection functions, make that
precise and clear.] The reader may want to contrast this general
statement with the numerous papers on the relationship between direct
and continuation semantics.''

The practical consequence of the lack of stability of denotations for
monads is that monadic transformers put layers upon layers of thunks,
which have to be carried over _in full_ from one sub-expression into
the other, even if no single subexpression uses all of the features.

The present code is not written in idiomatic Haskell and does not take
advantage of types at all. The ubiquitous projections from the
universal domain tantamount to ``dynamic typing.''  The code is
intentionally written to be close to the EDLS paper, emphasizing
denotational semantics (whose domains are untyped). One can certainly
do better, for example, employ user-defined datatypes for tagged
values, avoiding the ugly string-tagged VT.
-}

module ExtensibleDS where

import Maybe

------------------------------------------------------------------------
-- The base interpreter


-- The universal domain
-- Yes, it is untyped... But Denot semantics is like this anyway...
-- Bottom is the implicit member of this domain.
data Value = VI Int			-- integers
	   | VS String			-- strings
	   | VP Value Value		-- pairs
	   | VF (Value -> Value)	-- functions
	   | VT Tag Value		-- tagged value

type Tag = String

type Action = Value 			-- only differently tagged

instance Show Value where
    show (VI x) = show x
    show (VS x) = show x
    show (VT tag v) = "{"++show tag++" "++show v++"}"
    show (VP x1 x2) = show (x1,x2)
    show (VF _)  = "<procedure>"



-- Computations: just like in EDLS
-- The strictness of inV guarantees that inV bottom = bottom, as
-- on Fig. 3 of EDLS
-- Error is always a part of the computation

data Comp = InV !Value | InFX (Value -> Comp) Action

instance Show Comp where
    show (InV v) = show v
    show (InFX _ a) = "Effect: " ++ show a


-- Auxiliary functions
newtype V = V String deriving (Eq, Show) -- Variables
type Env v = V -> v
empty_env x = error $ "impossible: an open program? var " ++ show x
ext_env env x v y | x == y = v
ext_env env x v y = env y


-- Note that inV is essentially the identity `partial' continuation
inAC action = InFX InV action

-- The error `raise' action and its tag
tagErr = "Err"
raise err = inAC $ VT tagErr (VS err)

-- The universal handler of actions
-- It propagates the action request InFX up.
-- Since we do case-analysis on the first argument, v, the handler
-- is strict in that argument. That is, handler bottom ==> bottom,
-- as required by Fig. 3 of EDLS.
-- The last clause is essentially the denotation of a `control channel'
handler (InV v) k = k v
handler (InFX ka a) k = InFX (\v -> handler (ka v) k) a


-- Expressions and their interpretations
-- This is an open data type and an open function. Haskell typeclasses
-- are ideal for that.

-- This is the function \curlyM of EDLS
class Interpretor exp where
    interpret ::  exp -> Env Value -> Comp

-- The base language has only two expressions: omega and error
-- See Fig. 3 (p. 7) of EDLS

data BE_err   = BE_err
data BE_omega = BE_omega

instance Interpretor BE_omega where
    interpret _ _ = InV undefined

instance Interpretor BE_err where
    interpret _ _  = raise "error action"

-- The meaning of a program
prog p = interpret p empty_env


-- ----------------------------------------------------------------------
-- Extension: Call-by-Value: see a part Fig. 4 of EDLS (or, Fig. 8)

-- We add closures (procedures) to the Base
type Proc = Value -> Comp

class PV u where			-- and the corresponding injection/
  inP :: Proc -> u			-- projection functions
  prP :: u -> Maybe (Proc)


type Var = V
data Lam e = Lam V e
data App e1 e2 = e1 :@ e2
infixl 1 :@

instance Interpretor V where
    interpret v env = InV (env v)

instance Interpretor e => Interpretor (Lam e) where
    interpret (Lam x e) env = InV (inP (\d -> interpret e (ext_env env x d)))

instance (Interpretor e1, Interpretor e2) => Interpretor (App e1 e2) where
    interpret (e1 :@ e2) env =
	handler (interpret e1 env) $
		\f -> handler (interpret e2 env) $
		      \a -> maybe (raise "InP expected") (\g -> g a)
			          (prP f)


-- Create a few variables for use in examples
vx, vy, vr, vf :: Var
(vx,vy,vr,vf) = (V "x", V "y", V "r", V "f")

-- Test of the extension
-- Instantiate this extension on the top of the base language

-- Denotations of the new actions (inj/proj to/from the Universal Domain)
tagProc  = "Proc"
tagCompV = "CompV"
tagCompE = "CompE"

-- inject and project computations
inComp :: Comp -> Value
inComp (InV v) = VT tagCompV v
inComp (InFX k a) = VT tagCompE (VP (VF (inComp . k)) a)

prComp :: Value -> Maybe Comp
prComp (VT tag v) | tag == tagCompV = Just (InV v)
prComp (VT tag v) | tag == tagCompE = pr v
   where pr (VP (VF k) a) = Just $ InFX (fromJust . prComp . k) a
	 pr _ = Nothing
prComp _ = Nothing


instance PV Value where
    inP f = VT tagProc (VF (inComp . f))
    prP (VT tag (VF k)) | tag == tagProc = Just $ fromJust . prComp . k
    prP _ = Nothing

test1 = Lam vx (vx :@ BE_err)

test1e = prog test1
-- {"Proc" <procedure>}


------------------------------------------------------------------------
-- Extension: Arithmetic: see a part Fig. 4 of EDLS 

class PN u where			-- inj/proj for numbers
  inN :: Int -> u
  prN :: u -> Maybe Int

data IntC = IntC Int			-- an integer constant
data Add1 = Add1

instance Interpretor IntC where
    interpret (IntC v) _ = InV (inN v)

instance Interpretor Add1 where
    interpret Add1 _ = InV (inP $
			       \v -> maybe (raise "InN expected")
				     (InV . inN . succ)
				     (prN v))


add1 x = Add1 :@ x

-- Test of the extension
-- Instantiate this extension on the top of the CBV evaluator

instance PN Value where
    inN n = VI n
    prN (VI n) = Just n
    prN _ = Nothing


test2 = (Lam vx $ add1 vx) :@ (IntC 1)
test2e = prog test2
-- 2

------------------------------------------------------------------------
-- Extension: State: see Fig. 5 of EDLS 

newtype Loc = Loc Int deriving (Eq, Show) -- locations

class PL u where
  inL :: Loc -> u
  prL :: u -> Maybe Loc

-- a better idea is Loc -> Maybe Value, so that when lookup fails,
-- we can re-throw that Deref or Set message. That would make the
-- storage extensible...
-- The first component of the pair is the allocation counter
type Sto = (Int, Loc -> Value) 

tagSto = "Storage"

inSto :: Sto -> Value
inSto (cnt, st) = VT tagSto (VP (VI cnt) (VF (st . fromJust . prL)))
prSto :: Value -> Maybe Sto
prSto (VT tag (VP (VI cnt) (VF k))) | tag == tagSto = Just (cnt, k . inL)
prSto _ = Nothing

init_sto :: Sto
init_sto  = (0,\l->undefined)


-- data StoAct v = InRef v | InDer Loc | InSet Loc v

-- new expressions
data Ref e = Ref e
data Deref e = Deref e
data Set e1 e2 = Set e1 e2

-- Denotations of the new actions (inj/proj to/from the Universal Domain)
tagInRef = "Ref"
tagInDer = "Deref"
tagInSet = "Set"

inRef v = VT tagInRef v
prRef (VT tag v) | tag == tagInRef = Just v
prRef _ = Nothing

inDer v = VT tagInDer (inL v)
prDer (VT tag v) | tag == tagInDer = prL v
prDer _ = Nothing

inSet l v = VT tagInSet (VP (inL l) v)
prSet (VT tag (VP l v)) | tag == tagInSet = fmap (\l -> (l,v)) (prL l)
prSet _ = Nothing



instance Interpretor e => Interpretor (Ref e) where
    interpret (Ref e) env = handler (interpret e env) $
			      \v -> inAC(inRef v)


instance Interpretor e => Interpretor (Deref e) where
    interpret (Deref e) env = handler (interpret e env) $
			      \v -> maybe (raise "InL expected")
				    (inAC . inDer)
				    (prL v)

instance (Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2) where
    interpret (Set e1 e2) env = handler (interpret e1 env) $
			      \l -> handler (interpret e2 env) $
				 \v -> maybe (raise "InL expected")
				             (\l -> inAC (inSet l v))
					     (prL l)


-- Now we need a storage admin
-- It is treated as an expression in the source language!

data StoAdmin e = StoAdmin Sto e

instance Interpretor e => Interpretor (StoAdmin e) where
    interpret (StoAdmin sto e) env = sto_handler sto (interpret e env) InV


sto_handler (cnt,st) (InFX k a) f | Just v <- prRef a = 
   let l = Loc cnt
       sto = (cnt+1, \l' -> if l' == l then v else st l')
   in sto_handler sto (k (inL l)) f
sto_handler sto@(cnt,st) (InFX k a) f | Just l <- prDer a = 
   sto_handler sto (k (st l)) f
sto_handler (cnt,st) (InFX k a) f | Just (l,v) <- prSet a = 
   sto_handler (cnt, \l' -> if l' == l then v else st l') (k (inL l)) f

sto_handler sto (InV v) f = f (VP v (inSto sto)) -- normal return
-- Propagate everything else
sto_handler sto (InFX k a) f = InFX (\v -> sto_handler sto (k v) f) a

				       
tagLoc = "Loc"

instance PL Value where
    inL (Loc l) = VT tagLoc (VI l)
    prL (VT tag (VI l)) | tag == tagLoc = Just (Loc l)
    prL _ = Nothing


-- Test of the extension
-- Note that we can use several local storages!


test3 = (Lam vr $ Lam vf $ vf :@ (Deref vr)) :@
	  (Ref (IntC 1)) :@ (Lam vx $ add1 vx)

-- we forgot the Admin..., so the program terminates with an effect
test31 = prog test3 
-- Effect: {"Ref" 1}

test32 = prog (StoAdmin init_sto test3)
-- (2,{"Storage" (1,<procedure>)})

test33 = prog (StoAdmin init_sto 
	       ((Lam vr $ (Lam (V "_") (Deref vr)) :@ (Deref (Set vr (IntC 2))))
		:@ (Ref (IntC 1))))
-- (2,{"Storage" (1,<procedure>)})

------------------------------------------------------------------------
-- Extension: Delimited continuation
-- That is new compared to EDLS

-- new effect message: Control ((Value->Comp)->Comp)
tagControl = "Control"

inControl :: (Value->Comp) -> Value
inControl f = VT tagControl (VF (inComp . f))
prControl :: Value -> Maybe (Value->Comp)
prControl (VT tag (VF f)) | tag == tagControl = Just (fromJust . prComp . f)
prControl _ = Nothing


data Control e = Control e

instance Interpretor e => Interpretor (Control e) where
    interpret (Control e) env = handler (interpret e env) $
		      \a -> maybe (raise "InP expected")
			          (\f -> inAC(inControl f))
			          (prP a)

-- The administrator here is prompt, quite unsurprisingly

data ControlAdmin e = ControlAdmin e

instance Interpretor e => Interpretor (ControlAdmin e) where
    interpret (ControlAdmin e) env = ctl_handler (interpret e env) InV


ctl_handler (InFX k a) f | Just e <- prControl a = 
   ctl_handler (e (inP k)) f

ctl_handler (InV v) f = f v -- normal return
-- Propagate everything else
ctl_handler (InFX k a) f = InFX (\v -> ctl_handler (k v) f) a

-- Ken's tests

control v e = Control (Lam (V v) e)
prompt e = ControlAdmin e
succ0 = (add1 (IntC 0))

-- if we forget Reset...
test41 = prog $ add1 (Control (Lam vf succ0))
-- Effect: {"Control" <procedure>}

test42 = prog $ prompt (add1 (control "f" succ0))
-- 1

test43 = prog $ prompt (add1 (control "f" (vf :@ succ0)))
--2

test44 = prog $ prompt (add1 (add1 (control "f" (vf :@ succ0))))
-- 3

test45 = prog $ prompt (add1 (add1 (control "f" 
				    (vf :@ (vf :@ succ0)))))
-- 5

test46 = prog $ prompt (add1 ((Lam vx (add1 vx)) :@
			      (control "f" (vf :@ (vf :@ succ0)))))

-- 5
test47 = prog $ prompt (add1 ((Lam vx (control "f" (IntC 0))) :@
			      (control "f" (vf :@ (vf :@ succ0)))))
-- 0

test48 = prog $ add1 (prompt ((Lam vx (control "f" (IntC 0))) :@
			      (control "f" (vf :@ (vf :@ succ0)))))
-- 1