[Haskell-cafe] Implementing an embedded language that threads a global structure.

[Ian Bloom]

Hi,

I've been working on this problem for some time and I was hoping for some
feedback. I'm trying to implement an embedded language that can thread a
global structure through the evaluation of a term.

A mini version of this language only includes three functions, lam, app and
ext (lambda, apply and extension respectively). The only difference between
this and other embedded languages is that terms embedded in an extension
have access to a global variable that is invisible to the terms themselves.

The writer of a term in this language can only access the global variable
by applying an extension. The writer extensions insures that the effect of
evaluation on the global variable is commutative and insures that the
effect of the global variable on terms is constant regardless of the order
of evaluation.

For example the global variable could be a map with some sort of lazy
processing. An extension that queries the map for an element might cause a
change in the state of the map and return some information about an
element, but as long as the change in state are commutative and the same
information is returned about elements regardless of the order of
evaluation then the concept is safe.

My motivation for experimenting with such a language comes from a belief
that certain complicated programs would be easier to express in such a
language and that there might be very useful code transformations that
could eventually be applied to such a language that would be possible
because of the constraints on the behavior of extensions.

However I have yet to properly implement a language in Haskell and so I
decided to post what I have and look for comments.

Basically the language takes a common form of embedded languages; a lambda
expression such as

\x y->x y

would have the form:

lam (\x -> lam (\y -> app x y))

however in order to evaluate an expression the need to also apply it to a
global term:

lam (\x -> lam (\y -> app x y)) global

Ideally the result of evaluating this would be a (global', \x y-> x y), a
modified version of global paired with the term. So the type of the term:

lam (\x -> lam (\y -> app x y)) is something like g -> (g, (a -> b) -> a ->
b) where g is the type of global.