|
Continuations
Continuations can also be used to implement objects with state.
A continuation is just a function, passed as a parameter, that represents a
computation to be completed (i.e. continued with) at some later time.
e.g.
- γ : Cmd
- σ : State
- θ : Cont = State->Ans
- Ans = List Reply
- C : Cmd->Cont->State->Ans
= Cmd->Cont->Cont
- C `γ1;γ2' θ σ
= C γ1 (C γ2 θ) σ
Note how the rule for `γ1;γ2',
can be read left-to-right as
"to do γ1;γ2, first
do γ1 and then do γ2", and
replaces what would otherwise be functional composition
(C' γ2)o(C' γ1).
(Continuations are used in
denotational semantics
to describe the semantics of jumps and other sequencers found in
imperative programming languages.)
let Obj = lambda cmds. { List Cmd -> Ans }
{ Cont = State -> Ans -- continuation }
let rec
{ C : Cmd->Cont->State->Ans = Cmd->Cont->Cont }
C = lambda cmd. lambda cont. lambda state.
let rec tag = fst cmd,
param = snd cmd
in if tag = set then { change State }
(pair ok nil) :: cont param
else if tag = get then
(pair st state) :: cont state
else (pair err nil) :: cont state,
Cs = lambda cmds. lambda state.
if null cmds then nil {finished}
else C hd cmds (Cs tl cmds) state
in Cs cmds state0
Note that we have two functions, C and Cs,
because (here) Cmd and Cmds = List Cmd are different types.
|
λ ...
:: | list cons |
nil | the [ ] list |
null | predicate |
hd | head (1st) |
tl | tail (rest) |
|
|
|