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