Continuation Monad

[BS14] [Cha21]

General-purpose continuation monad, following [BS14]. The type Cont R A := (A → R) → R underlies lifted question types (Lifted.lean), higher-order dynamic GQs, and scope-taking expressions generally.

Key definitions

• Cont R A: the continuation monad
• Cont.pure, Cont.bind, Cont.map: monad operations
• Cont.lower: Barker & Shan's LOWER (evaluate with identity continuation)
• Tower C B A: Barker & Shan's tower abbreviation (A → B) → C

def Semantics.Composition.Continuation.Cont (R : Type u) (A : Type v) : Type (max u v)

The continuation monad: (A → R) → R. An expression of type Cont R A takes a continuation A → R and produces a result of type R.

Equations

• Semantics.Composition.Continuation.Cont R A = ((A → R) → R)

def Semantics.Composition.Continuation.Cont.pure {R : Type u} {A : Type v} (a : A) : Cont R A

Monadic unit: wrap a value for any continuation. pure a = λκ. κ(a)

Equations

• Semantics.Composition.Continuation.Cont.pure a κ = κ a

def Semantics.Composition.Continuation.Cont.bind {R : Type u} {A : Type v} {B : Type w} (m : Cont R A) (f : A → Cont R B) : Cont R B

Monadic bind: sequence two continuized computations. m >>= f = λκ. m(λa. f(a)(κ))

Equations

• m.bind f κ = m fun (a : A) => f a κ

def Semantics.Composition.Continuation.Cont.map {R : Type u} {A : Type v} {B : Type w} (f : A → B) (m : Cont R A) : Cont R B

Functorial map: apply a function under the continuation. map f m = λκ. m(λa. κ(f(a)))

Equations

• Semantics.Composition.Continuation.Cont.map f m κ = m fun (a : A) => κ (f a)

def Semantics.Composition.Continuation.Cont.lower {A : Type v} (m : Cont A A) : A

LOWER: evaluate a Cont A A with the identity continuation. Barker & Shan's key operation for "scope-taking is done."

Equations

• m.lower = m id

@[reducible, inline]

abbrev Semantics.Composition.Continuation.Tower (C : Type u) (B : Type v) (A : Type w) : Type (max (max u v) w)

Tower type abbreviation: (A → B) → C. In Barker & Shan's notation, this is the flat reading of

  C | B
  ─────
    A

Equations

• Semantics.Composition.Continuation.Tower C B A = ((A → B) → C)

The continuation monad's laws (left/right identity, associativity, and the functor laws) are exactly those of LawfulMonad, so we register Cont R as a lawful monad rather than restating them as standalone rfl theorems. R is fixed to Type (not universe-polymorphic) for Lean's Monad class.

@[implicit_reducible]

instance Semantics.Composition.Continuation.instFunctorCont {R : Type} : Functor (Cont R)

Equations

• Semantics.Composition.Continuation.instFunctorCont = { map := fun {α β : Type ?u.1} => Semantics.Composition.Continuation.Cont.map }

@[implicit_reducible]

instance Semantics.Composition.Continuation.instPureCont {R : Type} : Pure (Cont R)

Equations

• Semantics.Composition.Continuation.instPureCont = { pure := fun {α : Type ?u.1} => Semantics.Composition.Continuation.Cont.pure }

@[implicit_reducible]

instance Semantics.Composition.Continuation.instBindCont {R : Type} : Bind (Cont R)

Equations

• Semantics.Composition.Continuation.instBindCont = { bind := fun {α β : Type ?u.1} => Semantics.Composition.Continuation.Cont.bind }

@[implicit_reducible]

instance Semantics.Composition.Continuation.instSeqCont {R : Type} : Seq (Cont R)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Composition.Continuation.instMonadCont {R : Type} : Monad (Cont R)

Equations

• One or more equations did not get rendered due to their size.

instance Semantics.Composition.Continuation.instLawfulMonadCont {R : Type} : LawfulMonad (Cont R)

theorem Semantics.Composition.Continuation.Cont.lower_pure {A : Type v} (a : A) : (pure a).lower = a

Lower of pure is identity. (Not a monad law — a fact about Cont.lower.)

Scope as bind order

Scope ambiguity in the continuation framework is the order of monadic bind — surface scope binds the subject first, inverse scope the object first — and lower is generalized-quantifier application ([BS14]). These hold for any quantifier and predicate.

theorem Semantics.Composition.Continuation.cont_scope_reduce {E S : Type} (q : Cont S E) (scope : E → S) : (q.bind fun (x : E) => Cont.pure (scope x)).lower = q scope

Lowering a Cont-wrapped quantifier with a pure scope predicate is plain GQ application: lower (Q >>= λx. pure (P x)) = Q P.

theorem Semantics.Composition.Continuation.cont_scope_double {E S : Type} (q₁ q₂ : Cont S E) (rel : E → E → S) : (q₁.bind fun (x : E) => q₂.bind fun (y : E) => Cont.pure (rel x y)).lower = q₁ fun (x : E) => q₂ fun (y : E) => rel x y

Nested Cont binds compute nested GQ application; the bind nesting determines scope order.

theorem Semantics.Composition.Continuation.scope_ambiguity_is_bind_order {E S : Type} (q₁ q₂ : Cont S E) (rel : E → E → S) : ((q₁.bind fun (x : E) => q₂.bind fun (y : E) => Cont.pure (rel x y)).lower = q₁ fun (x : E) => q₂ fun (y : E) => rel x y) ∧ (q₂.bind fun (y : E) => q₁.bind fun (x : E) => Cont.pure (rel x y)).lower = q₂ fun (y : E) => q₁ fun (x : E) => rel x y

Scope ambiguity = bind order: the two readings of Q₁ R Q₂ are Q₁ nested outside Q₂ vs Q₂ outside Q₁, each reducing to GQ application in the corresponding order.

theorem Semantics.Composition.Continuation.cont_scope_triple {E S : Type} (q₁ q₂ q₃ : Cont S E) (rel : E → E → E → S) : (q₁.bind fun (x : E) => q₂.bind fun (y : E) => q₃.bind fun (z : E) => Cont.pure (rel x y z)).lower = q₁ fun (x : E) => q₂ fun (y : E) => q₃ fun (z : E) => rel x y z

The bind-order pattern extends to arbitrary depth.

theorem Semantics.Composition.Continuation.cont_pure_is_fa {S A : Type} (f : A → S) (x : A) : ((Cont.pure f).bind fun (g : A → S) => (Cont.pure x).bind fun (y : A) => Cont.pure (g y)).lower = f x

When all meanings are Cont.pure-wrapped, Cont composition reduces to function application — the non-scope-taking (Reader) fragment embeds into Cont ([Cha18]).