Modify the syntax to include a new construct [Do] and restrict [Eff] to values
Following @fpottier's suggestion, we include a new language construct Do
that takes an arbitrary expression e
as its only argument. The meaning of Do e
is to launch the raising of an effect once the evaluation of e
is complete. This is captured by the following new reduction rule:
(Do (Val v)); σ → (Eff v EmptyCtx); σ
There are two advantages in doing this: (1) the syntax of evaluation contexts become simpler because we no longer need to consider the context Eff [] k
and (2) the users of the language can ignore the existence of Eff
which is now only a detail of the operational semantics.