|
Ah! This idea is not new; it appears to be what [Cenciarelli and Moggi (1993), A syntactic approach to modularity in denotational semantics] is about. Unfortunately Moggi's writing is as dense as ever in this paper. --KenShan |
|
This idea may be what [Cenciarelli and Moggi (1993), A syntactic approach to modularity in denotational semantics] is about. Unfortunately Moggi's writing is as dense as ever in this paper, so I can't tell for sure. --KenShan 2001-06-17 |
Begin with some program written in a lambda-calculus-ish programming language (call this language the source language L1). Like ML, our source language may have "imperative" constructs such as I/O (print), state (:=), etc. To clarify the denotational semantics of the source language L1, we define a translation from L1 into Moggi's computational meta-language (CML). The translation makes evaluation order explicit; we can choose from a variety of call-by-value and call-by-name translations available.
CML makes reference to a primitive type constructor T1, a monad. Our translation from L1 into CML does not completely specify the semantics of L1 -- it only reduces specifying the semantics of L1 to specifying the semantics of CML. To specify the semantics of CML, we then need to write down definitions for the monad T1 (in terms of map, unit, and join, say).
What (programming) language we use to define T1? It would probably be some language that is syntactically similar -- even identical -- to L1. For example, to define T1 as the environment monad, we might write
-- Listing 1
type T1 a = Env -> a
unit = \a \r a
bind = \m \k \r k (m r) r
Let us call the language we use to define T the secondary language
L2. We have so far reduced specifying the semantics of L1 to
specifying the semantics of L2. How are we to specify the semantics
of L2? Well, why not do again what we just did? Namely, let us
specify a translation from L2 into CML. Again we can choose between a
variety of call-by-value and call-by-name translations. Whatever
translation we choose, though, because it is a translation into CML it
must make reference to a primitive type constructor T2, a monad
distinct from the monad T1 from the previous translation.
We can continue this process for as many times as we like, each time selecting a translation from L(i) to CML, then specifying the monad T(i) by defining it in L(i+1):
Eventually we reach the identity monad, say T(n) = Id. We specify (ground) the semantics of L(n+1) in terms of "usual lambda calculus". Because the evaluation order of L(n) is fully specified in our translation from L(n) to CML with monad T(n), it doesn't matter what evaluation order we use when specifying the semantics of L(n+1). We are finally done specifying the semantics of all these languages, including our original source language L1.
A monad transformer is simply the monad morphism taking T(j) to T(k), where j >= k. In other words, a monad transformer is a monad T(k) defined in terms of another monad T(j); one easy way to define a monad T(k) in terms of another monad T(j) is to first define T(k) in some lambda-calculus-ish language L(k+1), then translate it into CML with the monad T(j).
For example, the usual environment monad transformer
-- Listing 2
type Monad m => EnvT m a = Env -> m a
unit = ...
bind = ...
can be thought of as a call-by-value translation of the environment
monad in Listing 1.
There is probably also a "call-by-name environment monad transformer", i.e., a call-by-name translation of Listing 1:
-- Listing 3
type Monad m => EnvT' m a = m Env -> m a
unit = ...
bind = ...
Connection to natural language semantics: The de-re/de-dicto ambiguity in the sentence
can probably be modeled by a call-by-name continuation monad transformer applied to the intensionality (aka environment) monad.
--KenShan
This idea may be what [Cenciarelli and Moggi (1993), A syntactic approach to modularity in denotational semantics] is about. Unfortunately Moggi's writing is as dense as ever in this paper, so I can't tell for sure. --KenShan 2001-06-17