Evaluating continuation computations

ContT.eval finishes a continuation computation by handing it the trivial continuation pure — [Cha14b]'s Lowering, Haskell's evalCont, the LOWER of [BS14]. The eval_* simp lemmas mirror ContT's run_* set: a chain of binds evaluates in bind order and the applicative combination left-to-right, which is what lets bind order model quantifier scope. ContT.reset evaluates and re-lifts, delimiting scope the way scope islands do. For the linguistic applications see Studies/BumfordCharlow2024.lean and Studies/Charlow2020.lean.

References

• https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html#v:evalCont

def ContT.eval {r : Type u} {m : Type u → Type v} [Pure m] (c : ContT r m r) : m r

Evaluation at the trivial continuation: eval c = c.run pure.

Equations

• c.eval = c.run pure

Interaction with the monad operations

@[simp]

theorem ContT.eval_pure {r : Type u} {m : Type u → Type v} [Pure m] (a : r) : (pure a).eval = pure a

@[simp]

theorem ContT.eval_bind {r α : Type u} {m : Type u → Type v} [Pure m] (c : ContT r m α) (f : α → ContT r m r) : (c >>= f).eval = c.run fun (x : α) => (f x).eval

@[simp]

theorem ContT.eval_map {r α : Type u} {m : Type u → Type v} [Pure m] (f : α → r) (c : ContT r m α) : (f <$> c).eval = c.run fun (x : α) => pure (f x)

@[simp]

theorem ContT.eval_seq {r α : Type u} {m : Type u → Type v} [Pure m] (mf : ContT r m (α → r)) (mx : ContT r m α) : (mf <*> mx).eval = mf.run fun (f : α → r) => mx.run fun (x : α) => pure (f x)

Evaluating lifted computations

@[simp]

theorem ContT.eval_monadLift {r : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : m r) : (monadLift x).eval = x

def ContT.reset {r : Type u} {m : Type u → Type v} {r' : Type u} [Monad m] (c : ContT r m r) : ContT r' m r

Evaluate, then re-lift: reset c = monadLift (eval c) — [Cha14b]'s Reset, after [DF90]; [Bar02a]'s scope-island rule is an instance.

Equations

• c.reset = monadLift c.eval

theorem ContT.reset_monadLift {r : Type u} {m : Type u → Type v} {r' : Type u} [Monad m] [LawfulMonad m] (x : m r) : (monadLift x).reset = monadLift x

reset is transparent to lifted effects: effects escape islands, scope-takers do not.

theorem ContT.eval_seq_monadLift {r α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (f : α → β → r) (x : m α) (y : m β) : (f <$> monadLift x <*> monadLift y).eval = f <$> x <*> y

Lifting, combining, and evaluating is just combining in m: scopal combination subsumes applicative combination.