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/Charlow2014.lean and Studies/Barker2002.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

eval c runs c at the trivial continuation 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

reset c evaluates c and lifts the result again, reset c = monadLift (eval c), which is [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, so effects escape islands where scope-takers do not.

@[simp]

theorem ContT.eval_reset {r : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (c : ContT r m r) : c.reset.eval = c.eval

Evaluating a reset computation is evaluating the computation.

@[simp]

theorem ContT.reset_pure {r : Type u} {m : Type u → Type v} {r' : Type u} [Monad m] [LawfulMonad m] (a : r) : (pure a).reset = pure a

A pure value passes through reset.

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 combining in m, so scopal combination subsumes applicative combination.

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

Evaluating a lifted computation under a value-level map is mapping in m.

theorem ContT.reset_map_monadLift {r α : Type u} {m : Type u → Type v} {r' : Type u} [Monad m] [LawfulMonad m] (f : α → r) (x : m α) : (f <$> monadLift x).reset = monadLift (f <$> x)

Resetting a lifted computation changes nothing, whatever sits on the bottom level, since evaluation leaves the side effects of the underlying monad intact ([Cha14b]'s Fact 4.1).

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

Resetting a combination of lifted computations is lifting their combination in m.