Continuation Monad

@cite{barker-shan-2014} @cite{charlow-2021}

General-purpose continuation monad, following @cite{barker-shan-2014}. The type Cont R A := (A → R) → R underlies lifted question types (LiftedTypes.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 Core.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

• Core.Continuation.Cont R A = ((A → R) → R)

def Core.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

• Core.Continuation.Cont.pure a κ = κ a

def Core.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 Core.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

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

def Core.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 Core.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

• Core.Continuation.Tower C B A = ((A → B) → C)

theorem Core.Continuation.Cont.bind_left_id {R : Type u} {A : Type v} {B : Type w} (a : A) (f : A → Cont R B) : (pure a).bind f = f a

Left identity: pure a >>= f = f a

theorem Core.Continuation.Cont.bind_right_id {R : Type u} {A : Type v} (m : Cont R A) : m.bind pure = m

Right identity: m >>= pure = m

theorem Core.Continuation.Cont.bind_assoc {R : Type u} {A : Type v} {B : Type w} {C : Type u_1} (m : Cont R A) (f : A → Cont R B) (g : B → Cont R C) : (m.bind f).bind g = m.bind fun (a : A) => (f a).bind g

Associativity: (m >>= f) >>= g = m >>= (λa. f a >>= g)

theorem Core.Continuation.Cont.map_via_bind {R : Type u} {A : Type v} {B : Type w} (f : A → B) (m : Cont R A) : map f m = m.bind fun (a : A) => pure (f a)

Map can be defined via bind and pure.

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

Lower of pure is identity.