Information Technology Reference
In-Depth Information
For an example of both an environment monad and a side-effect monad,
take T ( D )= Env
S
D
×
S with Return ( d )= λρ.λσ.
d, σ
and e>> = f =
e ( ρ ). Then define GetEnv = P and UseEnv ( ρ )( e )=
λρ.e ( ρ ). Notice that T ( V ) is the domain of expression denotations in direct
semantics, and T () is isomorphic to the domain of statement denotations.
However, Scott and Strachey did not introduce combinators in connection
with environments, preferring to exhibit the propagation of environments.
Oxford style, continuation semantics: A further example of both an envi-
ronment monad and a side-effect monad is provided by T ( D )= Env
λρ. ( λ
a, σ
.f ( a )( ρ )( σ ))
S )with Return ( d )= λρ.λκ.κ ( d )and
e>> = f = λρ.λκ.e ( ρ )( λa.f ( a )( ρ )( κ )). (It could presumably be made into an
exception monad by adding continuations corresponding to handlers to the
environment.)
VDMstyle,normaltermination: Let T ( D )be =>D , which, in the absence
of abnormal termination, is STATE ˜
( D
C )
C (where C = S
STATE × D .Let Return be the VDM
combinator return ,andlet e>> = f be defined as def x: e; f(x) .This
provides a monad. Assuming that the store component of the state is selected
by STR , Update ( l, v ) can be defined to be STR := (c STR )+ [ l v ] ,and
Inspect ( l )tobe return((c STR )(l)) . This gives a side-effect monad, which
has been used in VDM since the early 1970s. It would be straightforward
to make Env=>D into an environment monad as well, but VDM does not
provide combinators corresponding to GetEnv and UseEnv .
VDM style, abnormal termination: The redefinition of =>D to allow abrupt
termination given in the PL/I semantics [17] is:
(res V | abn ABNORMAL)
where values are tagged with res or abn to distinguish between normal and
abrupt termination. The redefined combinators return and def still provide
a monad: this is essentially an instance of applying a monad transformer,
and all the original combinators are 'lifted' to the new domains. Moreover,
the resulting monad is easily made into an exception monad: define Raise ( a )
to be exit a ,and Handle ( a, b, c )as trap a with binc .Itisremarkable
that VDM was already using these monads more than 15 years before the
monadic style of denotational semantics was explicitly introduced.
However, it appears that the alternative redefinition of =>D in Meta-IV [18]
=>V = STATE ˜
=>V = STATE ˜
STATE
×
STATE × [ ABNORMAL ] × V
does not allow the combinators return and def to be redefined as a monad. 4
The problem is that e>> = f needs to be defined for all e in =>A and f in A=>B ,
where A and B are generally different domains; in the case corresponding to
abrupt termination of e , the third component of the resulting tuple needs to
be mapped from A to B . Simply mapping all elements of A to the bottom
element of B would violate one of the laws for monads (equation 17 above).
4 Thanks to Eugenio Moggi for drawing attention to this point.
 
Search WWH ::




Custom Search