SatisfiesM with Cps monad

Stream: lean4

[Chris Bailey]

Is it possible to write one of the SatisfiesM_M_eq style lemmas for the continuation monad, or is this one of the cases where the continuation monad doesn't behave nicely? E.g.:

example (p : α → Prop) (x : CpsM α) : SatisfiesM p x → SatisfiesM p (x.run) := sorry

It seems like with a lawful definition of the monad instance, the subtype pulls you into a tug of war with the goal x (k := fun a => a.val)) = (x (k := id)).val that the lawful definitions just don't allow you to solve, but I wanted to check whether I'm crazy. The full definition of CpsM I'm using is:

def CpsT (m : Type u → Type v) (α : Type u) := (δ : Type u) → (α → m δ) → m δ

namespace CpsT

def runK {α β : Type u} {m : Type u → Type v}  (x : CpsT m α) (k : α  → m β) : m β :=
  x β k

def run {α : Type u} {m : Type u → Type v} [Monad m] (x : CpsT m α) : m α :=
  runK x (fun a => pure a)

instance : Monad (CpsT m) where
  map  f x := fun δ k => x δ fun a => k (f a)
  pure a   := fun _ k => k a
  bind x f := (fun δ k => x δ fun a => f a δ k)

instance : LawfulMonad  (CpsT m) := by
  refine' { .. } <;> intros <;> rfl

@[reducible]
def CpsM := CpsT Id

[Eric Wieser]

I don't have an answer to your question about docs#SatisfiesM, but... Does Cps exist anywhere in core/std4 already?

[Kyle Miller]

I ended up implementing a CPS monad transformer independently, though it's a bit different (δ is fixed). Pasting it here: (Edit: I guess I was bad at searching before writing this, since it's already in mathlib docs#ContT)

import Lean

structure ContT (α : Type u) (m : Type u → Type v) (β : Type w) where
  run : (β → m α) → m α

section
variable {m : Type u → Type v} {α : Type u}

/-- Variant of `run`. -/
def ContT.delimit [Monad m] (x : ContT α m α) : m α := x.run pure

/-- Early exit. -/
def ContT.leave [Monad m] (a : α) : ContT α m β := .mk fun _ => pure a

/-- To lift one-argument functions into `ContT`. Synonym for `ContT.mk`. -/
def ContT.ofFn (f : (β → m α) → m α) : ContT α m β := .mk f

/-- To lift two-argument functions into `ContT`. -/
def ContT.ofFn₂ {β' : β → Sort _} (f : ((b : β) → β' b → m α) → m α) :
    ContT α m ((b : β) × β' b) := .mk <| fun g => f fun b b' => g ⟨b, b'⟩

instance [Monad m] : MonadLift m (ContT α m) where
  monadLift x := .mk fun f => do f (← x)

@[always_inline]
instance [Monad m] (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ContT α m) where
  throw e  := liftM (m := m) (throw e)
  tryCatch := fun x f => .mk fun g => tryCatchThe ε (x.run g) (fun e => (f e).run g)

def ContT.pure (b : β) : ContT α m β := .mk (fun f => f b)

def ContT.bind (x : ContT α m β) (f : β → ContT α m γ) : ContT α m γ :=
  .mk (fun g => x.run (fun b => (f b).run g))

instance : Monad (ContT α m) where
  pure := ContT.pure
  bind := ContT.bind

-- From Chris
instance : LawfulMonad (ContT α m) := by
  refine' { .. } <;> intros <;> rfl

end

[Kyle Miller]

One application is using it to make it so local declaration functions in MetaM can put their new variables on the LHS and save on some nesting:

open Lean Meta

def mkIndic (x : Expr) : MetaM Expr := ContT.delimit do
  let arg ← .ofFn <| withLocalDeclD `a (← inferType x)
  let eq ← mkEq x arg
  mkForallFVars #[arg] eq

def arity (f : Expr) : MetaM Nat := ContT.delimit do
  let ⟨args, _⟩ ← .ofFn₂ <| forallTelescope (← inferType f)
  return args.size

I'm not sure if this is a great idea (I don't like how it gives you less control over how long local declarations are still around), but it's interesting

[Kyle Miller]

@Chris Bailey In case you still care, that example isn't true:

axiom bad (α : Type) (p : α → Prop) (x : CpsM α) : SatisfiesM p x → SatisfiesM p (x.run)

example : False := by
  have h := bad Bool (· = true)
  simp [SatisfiesM] at h
  have := Classical.propDecidable
  let x : CpsM {a // a = true} := fun δ f =>
    if h1 : δ = Bool then
      h1.mpr false
    else
      f ⟨_, rfl⟩
  obtain ⟨⟨_, rfl⟩, h'⟩ := h x
  simp [run, runK, Functor.map] at h'

(this is using import Mathlib)

[Eric Wieser]

What's ContT.delimit in the mathlib spelling?

[Kyle Miller]

I don't see it, at least not in that module.

When you combine it with monad lifting, it's sort of implementing delimited continuations (which is why I called it ContT.delimit), in particular the reset operator; the ContT constructor is shift.

[Eric Wieser]

I was able to work out what I needed in #5863

[Eric Wieser]

I think ofFun would probably be handy, as right now I have to use a show

[Eric Wieser]

The other stumbling block is that I can't seem to throw an exception from within ContT; I haven't yet worked out if this is to be expected, or just a trivial missing instance.

[Eric Wieser]

Ah, fixed in #5897

[Chris Bailey]

Kyle Miller said:

Chris Bailey In case you still care, that example isn't true

Thank you, mystery solved.