 A Modular Monadic Action Semantics
started 8/30/2002; 1:26:39 AM - last post 8/30/2002; 2:41:06 AM
|
|
jon fernquest - A Modular Monadic Action Semantics 
8/30/2002; 1:26:39 AM (reads: 2703, responses: 1)
|
|
| A Modular Monadic Action Semantics |
|
This down to earth
246 page master's thesis
fuses the readability of
action semantics
with
the formal manipulability and provability of
modular monadic semantics
[Scheme Semantic Lego,
Liang and Hudak, 1996]
into a more useful whole:
Modular Monadic Action Semantics (MMAS).
"Modular monadic action semantics replaces the structural operational semantics
that formalises action semantics with a modular monadic semantics.
This replacement provides the flexibility to modify or delete existing facets of action
semantics or to add entirely new ones and will allow the use of the theories
of modular monadic semantics and of denotational semantics to theorise about
actions...
The integrated semantics adds a continuational facet to represent call-current-continuation.
The thesis includes a clear non-theoretical explanation of the two semantics that are integrated:
action semantics and modular monadic semantics.
A toy functional language EL is built in modular monadic semantics with Haskell.
The 1200 line Haskell implementation of the integrated system
is provided as a "literate Gofer script" in appendix e.
The whole thesis is written in a literate programming fashion and never strays far from source code.
Although neither a compiler nor an interpreter is built with the integrated system,
in appendix a two programming problems are solved.
(A Modular Monadic Action Semantics,
Keith Wansbrough, 1997)
Posted to functional by jon fernquest on 8/30/02; 1:31:55 AM
|
|
|
|
jon fernquest - Re: A Modular Monadic Action Semantics
8/30/2002; 2:41:06 AM (reads: 996, responses: 0)
|
|
|
Found this inspiring
old diary entry of
Graydon Hoare
(9 Jan 2001)
Been playing with modular monadic interpreters and compilers
recently. The monad keeners are really clever: the idea is to
separate out "facets" of a language processor (a la action
semantics) into separate monads, such that (if you get the
liftings right) you can do a modular proof of your rewrite
semantics for that facet irrespective of the other facets
you may have enabled. This is cool: you can develop a
working call/cc system or lambda abstraction or calling
convention in isolation, test it out, then just sorta graft
it into an existing compiler / interpreter. The math gets
a little ghastly but it's miles better than plain denotational semantics.
Monads are one of those things like pointers or closures.
You bang your head against them for a year or two, then one
day your brain's resistance to the concept just breaks,
and in its new broken state they make perfect sense.
Keith Wansbrough's
master's thesis advisor
John Hamer
has some interesting information on this line of research
on his
thesis/research topics page:
"Modularity in semantic specification languages
Recent work in semantic specification languages has focussed on the
issue of modularity. Modularity in denotational semantics has been
addressed by a number of frameworks, most notably action
semantics, modular monadic semantics, and the hybrid
modular monadic action semantics. A structuring mechanism
known as "monad transformers" is used in the latter two frameworks to
automatically connect the "plumbing" of the various building blocks
(environments, stores, exceptions, etc.).
The success of these monad transformers has prompted a search for
similar structuring mechanisms for operational semantics.
Peter Mosses of the University of Aarhus has recently proposed an
extension to SOS that appears to achieve this aim. This proposal bears
certain similarities to the DCG rules of Prolog, of which a number of
recent extensions have been made (e.g., van Roy's EDCG and Kagedal's
Logical State Threads packages). The comparative study proposed for
this project may well advance one or both of these two independently
conceived research initiatives."
|
|
|
|