Control.ExtensibleDS

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.

Documentation

data Value

The universal domain Yes, it is untyped... But Denot semantics is like this anyway... Bottom is the implicit member of this domain.

Constructors

VI Int

VS String

VP Value Value

VF (Value -> Value)

VT Tag Value

Instances

Show Value

PL Value

PN Value

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

PV Value

type Tag = String

type Action = Value

data Comp

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

Constructors

InV !Value

InFX (Value -> Comp) Action

Instances

Show Comp

newtype V

Auxiliary functions

Constructors

V String

Instances

Eq V

Show V

Interpretor V

type Env v = V -> v

class Interpretor exp where

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

Methods

interpret :: exp -> Env Value -> Comp

Instances

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)

data BE_err

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

Constructors

BE_err

Instances

Interpretor BE_err

data BE_omega

Constructors

BE_omega

Instances

Interpretor BE_omega

type Proc = Value -> Comp

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

class PV u where

Methods

inP :: Proc -> u

prP :: u -> Maybe Proc

Instances

PV Value

type Var = V

data Lam e

Constructors

Lam V e

Instances

Interpretor e => Interpretor (Lam e)

data App e1 e2

Constructors

e1 :@ e2

Instances

(Interpretor e1, Interpretor e2) => Interpretor (App e1 e2)

vy :: Var

Create a few variables for use in examples

vr :: Var

vf :: Var

vx :: Var

inComp :: Comp -> Value

Denotations of the new actions (injproj tofrom the Universal Domain)

inject and project computations

prComp :: Value -> Maybe Comp

class PN u where

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

Methods

inN :: Int -> u

prN :: u -> Maybe Int

Instances

PN Value

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

data IntC

Constructors

IntC Int

Instances

Interpretor IntC

data Add1

Constructors

Add1

Instances

Interpretor Add1

newtype Loc

Extension: State: see Fig. 5 of EDLS

Constructors

Loc Int

Instances

Eq Loc

Show Loc

class PL u where

Methods

inL :: Loc -> u

prL :: u -> Maybe Loc

Instances

PL Value

type Sto = (Int, Loc -> Value)

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

inSto :: Sto -> Value

prSto :: Value -> Maybe Sto

init_sto :: Sto

data Ref e

new expressions

Constructors

Ref e

Instances

Interpretor e => Interpretor (Ref e)

Denotations of the new actions (injproj tofrom the Universal Domain)

data Deref e

Constructors

Deref e

Instances

Interpretor e => Interpretor (Deref e)

data Set e1 e2

Constructors

Set e1 e2

Instances

(Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2)

data StoAdmin e

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

Constructors

StoAdmin Sto e

Instances

Interpretor e => Interpretor (StoAdmin e)

inControl :: (Value -> Comp) -> Value

prControl :: Value -> Maybe (Value -> Comp)

data Control e

Constructors

Control e

Instances

Interpretor e => Interpretor (Control e)

data ControlAdmin e

Constructors

ControlAdmin e

Instances

Interpretor e => Interpretor (ControlAdmin e)