liboleg-2010.1.6: An evolving collection of Oleg Kiselyov's Haskell modules



Extensible Denotational Semantics

This work is a generalization of /Extensible Denotational Language Specifications Robert Cartwright, Matthias Felleisen Theor. Aspects of Computer Software, 1994/

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 Source

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


VI Int 
VS String 
VP Value Value 
VF (Value -> Value) 
VT Tag Value 


Show Value 
PL Value 
PN Value

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

PV Value 

data Comp Source

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


InV !Value 
InFX (Value -> Comp) Action 


newtype V Source

Auxiliary functions


V String 


type Env v = V -> vSource

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


interpret :: exp -> Env Value -> CompSource


data BE_err Source

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




data BE_omega Source



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

class PV u whereSource


inP :: Proc -> uSource

prP :: u -> Maybe ProcSource


type Var = VSource

data Lam e Source


Lam V e 


data App e1 e2 Source


e1 :@ e2 


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

vy :: VarSource

Create a few variables for use in examples

inComp :: Comp -> ValueSource

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

inject and project computations

class PN u whereSource

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


inN :: Int -> uSource

prN :: u -> Maybe IntSource


PN Value

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

data IntC Source


IntC Int 


data Add1 Source




newtype Loc Source

Extension: State: see Fig. 5 of EDLS


Loc Int 


class PL u whereSource


inL :: Loc -> uSource

prL :: u -> Maybe LocSource


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

data Ref e Source

new expressions


Ref e 


Interpretor e => Interpretor (Ref e)

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

data Deref e Source


Deref e 


data Set e1 e2 Source


Set e1 e2 


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

data StoAdmin e Source

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


StoAdmin Sto e 


data Control e Source


Control e 


data ControlAdmin e Source


ControlAdmin e