State II

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.

Note how the rule for `γ₁;γ₂', can be read left-to-right as "to do γ₁;γ₂, first do γ₁ and then do γ₂", and replaces what would otherwise be functional composition (C' γ₂)o(C' γ₁). (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.