Lambda the Ultimate

inactiveTopic 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  blueArrow
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  blueArrow
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."