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.
- data Value
- type Tag = String
- type Action = Value
- data Comp
- newtype V = V String
- type Env v = V -> v
- class Interpretor exp where
- data BE_err = BE_err
- data BE_omega = BE_omega
- type Proc = Value -> Comp
- class PV u where
- type Var = V
- data Lam e = Lam V e
- data App e1 e2 = e1 :@ e2
- vy :: Var
- vr :: Var
- vf :: Var
- vx :: Var
- inComp :: Comp -> Value
- prComp :: Value -> Maybe Comp
- class PN u where
- data IntC = IntC Int
- data Add1 = Add1
- newtype Loc = Loc Int
- class PL u where
- type Sto = (Int, Loc -> Value)
- inSto :: Sto -> Value
- prSto :: Value -> Maybe Sto
- init_sto :: Sto
- data Ref e = Ref e
- data Deref e = Deref e
- data Set e1 e2 = Set e1 e2
- data StoAdmin e = StoAdmin Sto e
- inControl :: (Value -> Comp) -> Value
- prControl :: Value -> Maybe (Value -> Comp)
- data Control e = Control e
- data ControlAdmin e = ControlAdmin e
Documentation
The universal domain Yes, it is untyped... But Denot semantics is like this anyway... Bottom is the implicit member of this domain.
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
class Interpretor exp whereSource
Note that inV is essentially the identity partial
continuation
The error raise
action and its tag
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'
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
Interpretor Add1 | |
Interpretor IntC | |
Interpretor BE_omega | |
Interpretor BE_err | |
Interpretor V | |
Interpretor e => Interpretor (ControlAdmin e) | |
Interpretor e => Interpretor (Control e) | |
Interpretor e => Interpretor (StoAdmin e) | |
Interpretor e => Interpretor (Deref e) | |
Interpretor e => Interpretor (Ref e) | Denotations of the new actions (injproj tofrom the Universal Domain) |
Interpretor e => Interpretor (Lam e) | |
(Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2) | |
(Interpretor e1, Interpretor e2) => Interpretor (App e1 e2) |
The base language has only two expressions: omega and error See Fig. 3 (p. 7) of EDLS
type Proc = Value -> CompSource
The meaning of a program
Extension: Call-by-Value: see a part Fig. 4 of EDLS (or, Fig. 8)
We add closures (procedures) to the Base
Denotations of the new actions (injproj tofrom the Universal Domain)
inject and project computations
Extension: Arithmetic: see a part Fig. 4 of EDLS
type Sto = (Int, Loc -> Value)Source
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
new expressions
Ref e |
Interpretor e => Interpretor (Ref e) | Denotations of the new actions (injproj tofrom the Universal Domain) |
Now we need a storage admin It is treated as an expression in the source language!
Interpretor e => Interpretor (StoAdmin e) |